← all areas

Namespace MvPolynomial 99 theorems

— 62 · CrossingQuotient 36 · IsHomogeneous 1

directly in MvPolynomial 62

• Low coefficients agree under polynomial and power-series substitution MvPolynomial.coeff_aeval_optionElim_C_add_X_sum_monomial_eq 12 below · cited by 2 · depth 15
• Truncated implicit functions for a triangular pair of relations MvPolynomial.exists_coeff_aeval_optionElim_eq_zero_of_isUnit_eval_pderiv 1 below · cited by 2 · depth 16
• Kernel of (Q,R)-evaluation is generated by A-1 MvPolynomial.ker_aeval_eq_span_sub_one_of_squarefree_of_isWeightedHomogeneous 0 below · cited by 1 · depth 17
• Divisibility by a prime over 𝔽ₚ descends along Xᵢ ↦ Xᵢ^{p^n} MvPolynomial.mem_span_map_of_aeval_X_pow_mem_span_map 0 below · cited by 1 · depth 17
• Squarefreeness of the isobaric relation A(Q,R)=1 MvPolynomial.squarefree_of_isWeightedHomogeneous_of_aeval_eq_one 0 below · cited by 1 · depth 17
• Non-archimedean Lipschitz bound for polynomials on the unit polydisc MvPolynomial.abv_eval_sub_eval_le_mul_iSup 0 below · cited by 1 · depth 20
• Non-zero polynomials vanish almost nowhere on the torus MvPolynomial.ae_restrict_torusBox_eval_circleMap_ne_zero 0 below · cited by 4 · depth 20
• Integrability of log‖P‖ on the torus MvPolynomial.integrableOn_log_norm_eval_circleMap 2 below · cited by 4 · depth 20
• Mahler's bound: coefficients versus logarithmic Mahler measure MvPolynomial.log_norm_coeff_le_logMahlerMeasure_add 4 below · cited by 2 · depth 20
• Non-archimedean Lipschitz bound for a rational function near a point MvPolynomial.abv_eval_div_sub_eval_div_le 0 below · cited by 2 · depth 21
• Polynomial identity on S × {N^u} holds identically MvPolynomial.eq_of_forall_eval_rpow_eq 0 below · cited by 1 · depth 21
• Two-variable polynomial identity along real powers of N MvPolynomial.eq_of_forall_rpow_infinite_setOf_eval_eq 0 below · cited by 1 · depth 21
• Mahler measure by integrating out one variable MvPolynomial.logMahlerMeasure_eq_mul_integral_logMahlerMeasure_map_finSuccEquiv 3 below · cited by 1 · depth 21
• Symmetric homogeneous 2-cocycles are coboundaries (Lazard) MvPolynomial.exists_isHomogeneous_eq_sub_sub_of_cocycle_of_symmetric 0 below · cited by 1 · depth 22
• Uniform clearing of denominators in a deformation parameter MvPolynomial.exists_pair_clearDenominator_deformation 0 below · cited by 1 · depth 22
• Rank of a truncated polynomial algebra over a finite index set MvPolynomial.finrank_quotient_span_range_X_pow_eq_prod 0 below · cited by 1 · depth 22
• Polynomial inverse mod p of X + C X⁽ᵖ⁾ MvPolynomial.exists_subst_X_add_sum_mul_X_pow_sub_X_coeff_mem_span_of_isNilpotent 0 below · cited by 1 · depth 23
• Row-wise continuation of a two-variable series with separated denominators MvPolynomial.exists_polynomial_forall_tsum_row_mul_eval_eq_and_tsum_mul_eval_eq_of_tsum_mul_eval_eq 0 below · cited by 2 · depth 24
• From generators to all of ℤ[Xₙ]: additive intertwining MvPolynomial.forall_apply_eq_apply_smul_of_forall_X_of_eq_act 0 below · cited by 1 · depth 24
• Integral scaling P(nc)=nᵈP(c) forces homogeneity of degree d MvPolynomial.isHomogeneous_of_forall_eval_intCast_mul_eq_pow_mul 0 below · cited by 1 · depth 25
• Dimension of k[Xᵢ]/(f(Xᵢ)) for monic f MvPolynomial.finite_and_finrank_quotient_span_aeval_X_eq_pow_of_monic 0 below · cited by 1 · depth 27
• Finiteness of a truncated Dieudonné ring, with bound pⁿᵇ MvPolynomial.finite_and_natCard_quotient_truncatedDieudonneRelations_le_pow 0 below · cited by 1 · depth 27
• Faithfully flat lift family from Artinian lifting property MvPolynomial.exists_faithfullyFlat_algHom_lift_family_of_forall_isArtinianRing_exists_algHom_lift 9 below · cited by 1 · depth 29
• expandₚ makes R[X_σ] finite flat of rank p^{|σ|} MvPolynomial.finite_and_flat_and_finrank_expand_eq_pow 0 below · cited by 1 · depth 29
• Jacobian criterion for formal smoothness of a localised quotient MvPolynomial.formallySmooth_localization_atPrime_quotient_of_forall_pderiv_mem 4 below · cited by 2 · depth 29
• Multiplicative homogeneous quartic on ℤ[X,Y]/(X²-D,Y²-c) forces a square MvPolynomial.isSquare_or_isSquare_of_isHomogeneous_of_forall_eval_mul_eq 0 below · cited by 1 · depth 29
• Zero sets of non-zero polynomials are Haar-null MvPolynomial.measure_setOf_eval_eq_zero_of_ne_zero 0 below · cited by 5 · depth 29
• Jacobian criterion step: dv=0 forces v ∈ J I MvPolynomial.mem_mul_of_forall_pderiv_mem_of_forall_exists_algHom_lift 0 below · cited by 2 · depth 29
• Differentials of a localised polynomial ring after base change MvPolynomial.exists_tensor_kaehlerDifferential_linearEquiv_pi_of_isLocalization 0 below · cited by 1 · depth 30
• Localisations of polynomial rings are formally smooth over the base MvPolynomial.formallySmooth_and_free_and_finite_kaehlerDifferential_of_isLocalization 0 below · cited by 1 · depth 30
• Polynomial rings are standard smooth of relative dimension #ι MvPolynomial.isStandardSmoothOfRelativeDimension_natCard 0 below · cited by 3 · depth 30
• Scaling rigidity forcing P = c (X₀+X₁)^g MvPolynomial.exists_eq_C_mul_X_add_X_pow_of_totalDegree_le_of_forall_eval_eq_pow_mul_eval 0 below · cited by 1 · depth 31
• Existence of a Gotzmann bound for a Hilbert polynomial MvPolynomial.exists_forall_finrank_piece_succ_le_eval_and_exists_eq_eval 4 below · cited by 5 · depth 31
• Bertini–Noether: absolute irreducibility spreads out MvPolynomial.exists_ne_zero_and_forall_irreducible_map_of_irreducible_map_algebraicClosure 0 below · cited by 1 · depth 32
• Macaulay's bound is attained by a homogeneous ideal MvPolynomial.exists_span_monomial_finrank_piece_eq_and_finrank_piece_succ_eq_macaulayPow 0 below · cited by 4 · depth 32
• Macaulay's bound on Hilbert functions of graded quotients MvPolynomial.finrank_piece_succ_le_macaulayPow 1 below · cited by 13 · depth 32
• Homogeneous elements of an ideal generated by forms MvPolynomial.exists_finset_sum_mul_eq_of_isHomogeneous_of_mem_span 0 below · cited by 2 · depth 33
• Standard smooth quotient inverting a Jacobian minor MvPolynomial.exists_isStandardSmooth_algHom_isUnit_det_pderiv_basis_kaehlerDifferential 0 below · cited by 1 · depth 33
• Gotzmann persistence for ideals of maximal Hilbert growth MvPolynomial.finrank_piece_eq_of_maximal_growth 13 below · cited by 2 · depth 33
• Maximal Hilbert growth forces relations in degrees ≤ 1 MvPolynomial.relation_mem_span_of_forall_finrank_piece_succ_le 12 below · cited by 1 · depth 33
• Faithfully flat Artin-local lift families over a Noetherian base MvPolynomial.exists_faithfullyFlat_algHom_lift_family_of_forall_isArtinianRing_exists_algHom_lift_of_isNoetherianRing 4 below · cited by 1 · depth 34
• Green's hyperplane restriction theorem for a general linear form MvPolynomial.exists_forall_eval_ne_zero_macaulayPow_finrank_piece_sup_add_le 1 below · cited by 3 · depth 34
• Gotzmann maximal growth: general linear form regular in degrees ≥ m MvPolynomial.exists_forall_eval_ne_zero_mem_of_mul_mem_of_finrank_piece_succ_eq_macaulayPow 9 below · cited by 5 · depth 34
• A linear form that is a non-zero-divisor modulo a saturated homogeneous ideal MvPolynomial.exists_forall_sum_C_mul_X_mul_mem_imp_of_forall_exists_X_pow_mul_mem 16 below · cited by 1 · depth 34
• Killing an idempotent costs one variable and one relation MvPolynomial.exists_quotient_span_quotient_span_singleton_algEquiv_of_isIdempotentElem 0 below · cited by 1 · depth 34
• One step of Gotzmann's persistence theorem MvPolynomial.finrank_piece_add_two_eq_macaulayPow_of_finrank_piece_succ_eq_macaulayPow 11 below · cited by 1 · depth 34
• Hilbert function drop along a nonzerodivisor linear form MvPolynomial.finrank_piece_sup_span_singleton_succ_add_finrank_piece_eq_of_forall_mul_mem_imp 0 below · cited by 1 · depth 34
• Macaulay lower bound for Hilbert functions of maximal growth MvPolynomial.le_finrank_piece_of_forall_succ_eq_macaulayPow_of_eventually_eq 3 below · cited by 1 · depth 34
• Maximal growth persists under a general hyperplane section MvPolynomial.exists_forall_eval_ne_zero_mem_of_mul_mem_and_finrank_piece_sup_eq_macaulayPow 4 below · cited by 2 · depth 35
• g⊗1-1⊗ g lies in the diagonal ideal MvPolynomial.exists_tmul_one_sub_one_tmul_eq_sum_mul 0 below · cited by 1 · depth 35
• Maximal growth passes to the degree-m part of J+(ℓ) MvPolynomial.finrank_piece_span_sup_linearForm_eq_macaulayPow_and_lt 1 below · cited by 1 · depth 35
• Gotzmann persistence for maximal Macaulay growth MvPolynomial.forall_finrank_piece_succ_eq_macaulayPow_of_finrank_piece_succ_eq_macaulayPow 14 below · cited by 3 · depth 35
• Ideal membership in A[σ] is Zariski-local on Spec A MvPolynomial.mem_ideal_iff_forall_map_mem_map_localizationAway 0 below · cited by 1 · depth 35
• Bayer–Stillman inductive step for colon ideals in degrees ≥ m MvPolynomial.mem_span_of_linear_mul_mem_of_forall_relation_modulo_mem_span 0 below · cited by 1 · depth 35
• Relations among degree-m forms spanning S_m are generated in degrees ≤ 1 MvPolynomial.relation_mem_span_of_forall_isHomogeneous_mem_span 1 below · cited by 1 · depth 35
• Relations generated in degree ≤ 1 from a hyperplane section MvPolynomial.relation_mem_span_of_linear_of_forall_relation_modulo_mem_span 0 below · cited by 1 · depth 35
• Linear syzygies among the variables are skew-symmetric MvPolynomial.exists_skew_eq_sum_mul_X_of_sum_mul_X_eq_zero 0 below · cited by 1 · depth 36
• Bézout coefficients multiply down to partial derivatives MvPolynomial.lmul_eq_pderiv_of_tmul_one_sub_one_tmul_eq_sum_mul 0 below · cited by 1 · depth 36
• Maximal Macaulay growth at m forces saturation in degrees ≥ m MvPolynomial.mem_of_forall_exists_X_pow_mul_mem_of_finrank_piece_succ_eq_macaulayPow 15 below · cited by 1 · depth 36
• Endomorphism of a truncated polynomial ring onto mod t² is bijective MvPolynomial.bijective_algHom_truncated_of_forall_exists_sub_mem_sq 0 below · cited by 3 · depth 37
• Localization at a rational point as a power series quotient MvPolynomial.exists_algEquiv_localization_atPrime_mvPowerSeries_quotient_apply_mk 0 below · cited by 1 · depth 37
• Killing an element of tsetminust² in a truncated polynomial algebra MvPolynomial.nonempty_truncated_quotient_span_singleton_algEquiv_truncated_of_not_mem_sq 1 below · cited by 1 · depth 37

MvPolynomial.CrossingQuotient 36

• Glued quotient a_w/a = b_w/b on the crossing model uv = t MvPolynomial.CrossingQuotient.exists_section_basicOpen_sup_mul_eq_of_mul_eq 0 below · cited by 2 · depth 15
• Stalk maximal ideal at a crossing section point is principal MvPolynomial.CrossingQuotient.maximalIdeal_stalk_eq_span_germ_sub 0 below · cited by 2 · depth 16
• Base change of the crossing algebra B[u,v]/(uv-b) MvPolynomial.CrossingQuotient.exists_algEquiv_tensorProduct_apply_U_and_apply_V 0 below · cited by 4 · depth 17
• Normality of the crossing ring W[x,y]/(xy-t) MvPolynomial.CrossingQuotient.isDomain_and_isIntegrallyClosed 2 below · cited by 6 · depth 17
• Krull dimension of the crossing W[x,y]/(xy-t) MvPolynomial.CrossingQuotient.ringKrullDim_le 0 below · cited by 4 · depth 17
• Chart line generic points are maximal in the special fibre MvPolynomial.CrossingQuotient.Resolution.eq_iota_apply_of_specializes_of_notMem_preimage_basicOpen 1 below · cited by 5 · depth 18
• Existence of a chart table of ideal sheaves on Resolution(t,e) MvPolynomial.CrossingQuotient.Resolution.exists_idealSheafData_chartTable 2 below · cited by 10 · depth 18
• Exceptional multidegree zero implies local triviality on the uv=varpi^e resolution MvPolynomial.CrossingQuotient.Resolution.exists_open_pullback_twist_iso_tensorUnit_of_degree_eq_zero 53 below · cited by 2 · depth 18
• Crossing resolution is an isomorphism over D(u)∪ D(v) MvPolynomial.CrossingQuotient.Resolution.isIso_toCrossing_morphismRestrict_basicOpen_U_sup_basicOpen_V 0 below · cited by 6 · depth 18
• Properness of the resolution morphism over the crossing xy=t^e MvPolynomial.CrossingQuotient.Resolution.isProper_toCrossing 4 below · cited by 11 · depth 18
• Regularity of the local rings of the glued crossing resolution MvPolynomial.CrossingQuotient.Resolution.isRegularLocalRing_stalk 1 below · cited by 6 · depth 18
• Special-fibre package for the resolution of uv = varpi^e MvPolynomial.CrossingQuotient.Resolution.specialFibrePackage_of_chartTable 22 below · cited by 2 · depth 18
• Regularity of R[x,y]/(xy-varpi) over a discrete valuation ring MvPolynomial.CrossingQuotient.isRegularRing_of_irreducible 0 below · cited by 6 · depth 18
• Monomial basis of the crossing ring W[x,y]/(xy-t) MvPolynomial.CrossingQuotient.linearIndependent_monomial_and_span_eq_top 0 below · cited by 11 · depth 18
• Points of exceptional ideal sheaves map to the crossing vertex MvPolynomial.CrossingQuotient.Resolution.U_mem_and_V_mem_asIdeal_toCrossing_of_mem_support 0 below · cited by 1 · depth 19
• Chart pullbacks of the component ideal sheaves on the resolution MvPolynomial.CrossingQuotient.Resolution.comap_iota_vanishingIdeal_closure_lines 1 below · cited by 7 · depth 19
• Fibre-maximal points over the vertex are exceptional-line generic points MvPolynomial.CrossingQuotient.Resolution.exists_eq_lineUGen_of_toCrossing_eq_vertexPt_of_forall_specializes 0 below · cited by 2 · depth 19
• Supports of consecutive ideal sheaves on the resolution meet MvPolynomial.CrossingQuotient.Resolution.exists_mem_support_and_mem_support_succ 0 below · cited by 1 · depth 19
• Exceptional subschemes of the resolution covered by two affine lines MvPolynomial.CrossingQuotient.Resolution.exists_twoAffineLineCover_subscheme_of_chartTable 1 below · cited by 2 · depth 19
• Sections of the resolution of uv=varpi^e meeting one exceptional line MvPolynomial.CrossingQuotient.Resolution.isClosedImmersion_and_exists_eq_specMap_lift_comp_iota_of_comp_toSpec_eq_id 1 below · cited by 1 · depth 19
• Invertibility of the ideal of a section of the resolution MvPolynomial.CrossingQuotient.Resolution.isInvertible_ker_section 13 below · cited by 1 · depth 19
• Chart table implies invertibility of the ideal sheaves F_k MvPolynomial.CrossingQuotient.Resolution.isInvertible_of_chartTable 2 below · cited by 1 · depth 19
• Separatedness of the glued resolution of xy = t^e MvPolynomial.CrossingQuotient.Resolution.isSeparated 0 below · cited by 5 · depth 19
• Divisor of varpiᵈ-α U on the Aₑ₋₁ resolution MvPolynomial.CrossingQuotient.Resolution.ker_section_mul_prod_pow_min_eq_ofIdealTop 9 below · cited by 1 · depth 19
• The resolution morphism is locally of finite type and quasi-compact MvPolynomial.CrossingQuotient.Resolution.locallyOfFiniteType_and_quasiCompact_toCrossing 0 below · cited by 1 · depth 19
• Section sorting on the resolution of uv=varpi^e MvPolynomial.CrossingQuotient.Resolution.mem_support_iff_eq_addVal_of_comp_toCrossing_eq 0 below · cited by 2 · depth 19
• Divisor table on the resolution of uv=t^e MvPolynomial.CrossingQuotient.Resolution.prod_pow_eq_ofIdealTop_uSec_and_vSec_and_tSec 2 below · cited by 5 · depth 19
• Valuative existence for the resolution of uv=t^e MvPolynomial.CrossingQuotient.Resolution.valuativeCriterion_existence_toCrossing 1 below · cited by 1 · depth 19
• x and y are non-zero-divisors in W[x,y]/(xy-t) MvPolynomial.CrossingQuotient.U_mem_nonZeroDivisors_and_V_mem_nonZeroDivisors 1 below · cited by 2 · depth 19
• Quotients of a crossing chart by U and V are polynomial rings MvPolynomial.CrossingQuotient.exists_algEquiv_quotient_span_U_and_span_V_polynomial 0 below · cited by 5 · depth 19
• Minimal primes over t in the chart W[x,y]/(xy-t) MvPolynomial.CrossingQuotient.minimalPrimes_span_algebraMap_eq_pair 0 below · cited by 1 · depth 19
• Valuation-ring points of uv = t^e lift to a chart MvPolynomial.CrossingQuotient.exists_comp_resolutionChart_eq_of_valuationRing 0 below · cited by 1 · depth 20
• 1-wU and 1-wV are non-zero-divisors in the crossing quotient MvPolynomial.CrossingQuotient.one_sub_algebraMap_mul_U_mem_nonZeroDivisors_and_V 1 below · cited by 1 · depth 20
• Universal property of the crossing quotient W[X₀,X₁]/(X₀X₁-t) MvPolynomial.CrossingQuotient.existsUnique_ringHom_comp_algebraMap_eq_and_apply_U_eq_and_apply_V_eq 0 below · cited by 3 · depth 27
• Maximal ideal at a hyperbola point generated by v-y' MvPolynomial.CrossingQuotient.maximalIdeal_stalk_eq_span_germ_V_sub 0 below · cited by 1 · depth 28
• Residue field surjectivity at a crossing point of UV=a MvPolynomial.CrossingQuotient.surjective_residueFieldMap_specMap_algebraMap_of_U_mem_of_V_mem 0 below · cited by 2 · depth 28

MvPolynomial.IsHomogeneous 1

• Iterated partial derivatives of order >n annihilate degree-n forms MvPolynomial.IsHomogeneous.iterate_pderiv_eq_zero_of_lt 0 below · cited by 2 · depth 14