Integral elements over… to Fraction-ring renaming is…

TheoremIntegral elements over coefficient rings#

For any commutative ring R and arbitrary variable type σ, MvPolynomial.isIntegral_iff_coeff_isNilpotent characterizes IsIntegral R p by nilpotence of every nonconstant coefficient. For reduced R, MvPolynomial.isIntegral_iff_eq_C_coeff_zero specializes this to p = C (p.coeff 0). The coefficient and variable universes are independent; trivial coefficient rings and empty or infinite variable types are allowed. Over ZMod 4, C 2 * X () is a nonconstant square-zero integral polynomial.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.isIntegral_iff_coeff_isNilpotent

InstanceIntegral closure in arbitrarily many variables#

For every integrally closed commutative domain R and arbitrary variable type ι, MvPolynomial.isIntegrallyClosed makes the ordinary polynomial ring MvPolynomial ι R integrally closed. The coefficient and variable universes are independent, and the variables may be empty or infinite. No Noetherian or unique-factorization hypothesis is imposed on R.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.isIntegrallyClosed

TheoremFlatness of commutative-ring variable renaming#

For every commutative ring R and arbitrary f : σ → τ, with coefficient and variable types in independent universes, MvPolynomial.rename_flat_iff characterizes flatness of the full ring homomorphism MvPolynomial.rename (R := R) f by injectivity of f or subsingleton coefficients. The scalar action is induced by this original polynomial-ring map, not just by R or by its image. Injective maps give free polynomial extensions after complementary variables are separated; a collision kills the regular difference of two distinct variables. The regularity API works over every commutative ring, including the zero ring. The independent models and criterion applications include a proper inclusion over the integers, a collision over the nonreduced ring ZMod 4, and the same collision over ZMod 1. The same module also gives MvPolynomial.comap_rename_surjective_iff for commutative semirings and MvPolynomial.rename_faithfullyFlat_iff for commutative rings: each uses the same injectivity-or-subsingleton condition for the original full polynomial map. Their criterion applications include the strict inclusion over ℤ, prime-spectrum surjectivity over the non-ring semiring ℕ, an empty source, and a collision over the zero ring.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.rename_flat_iff

TheoremCanonical unique-variable degree#

For any commutative semiring R, unique variable type σ ([Unique σ]), and p : MvPolynomial σ R, MvPolynomial.natDegree_uniqueAlgEquiv identifies Polynomial.natDegree (MvPolynomial.uniqueAlgEquiv R σ p) with p.totalDegree. The coefficient and variable universes are independent. No nonzero-polynomial or nontrivial-coefficient premise is needed: both natural-number degrees assign zero to the zero polynomial.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.natDegree_uniqueAlgEquiv

TheoremInjectivity and surjectivity of variable renaming#

For any commutative semiring R and any map f : σ → τ, with the coefficient, source-variable and target-variable types in independent universes, the canonical renaming map from the full polynomial semiring MvPolynomial σ R to the full polynomial semiring MvPolynomial τ R is injective exactly when f is injective or R is subsingleton (MvPolynomial.injective_rename_iff), and is surjective exactly when f is surjective or R is subsingleton (MvPolynomial.surjective_rename_iff).

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.injective_rename_iff

TheoremFormal smoothness of variable renaming#

Over any commutative ring R, MvPolynomial.rename_formallySmooth_iff_injective characterizes formal smoothness of the full source polynomial-ring homomorphism by injectivity of that homomorphism. Equivalently, MvPolynomial.rename_formallySmooth_iff says that the variable map is injective or the coefficients are subsingleton. The scalar action is induced by the original renaming, not just by R. The coefficient and variable types have independent universes, with no finiteness or nontriviality hypotheses. Complementary variables give the polynomial-extension direction; a square-zero lifting obstruction detects collisions over nontrivial coefficients.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.rename_formallySmooth_iff_injective

TheoremSmoothness of variable renaming#

Over any commutative ring R, MvPolynomial.rename_smooth_iff says that the canonical homomorphism on full polynomial rings is smooth exactly when the variable map is injective with finite complement, or R is subsingleton. This is stock RingHom.Smooth, including finite presentation, for the source-polynomial action induced by renaming. Coefficients and both variable types have independent universes; no finiteness or nontriviality hypothesis is imposed on them. MvPolynomial.rename_smooth_iff_flat_and_finiteType compares smoothness with flatness and finite type for these renamings. Five concrete settings in the same file distinguish the collision/flatness obstruction from the infinite-complement/finite-type obstruction and exhibit the zero-ring exception. A derived application uses the comparison to extract flatness and finite type from an independent one-variable extension over ℤ.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.rename_smooth_iff

TheoremFormal unramifiedness of variable renaming#

Over any commutative ring R, MvPolynomial.formallyUnramified_rename_iff_surjective says that MvPolynomial.rename f, as a homomorphism from the full source polynomial ring, is formally unramified exactly when it is surjective: equivalently, when f is surjective or R is subsingleton. The coefficient and variable types may lie in independent universes, and neither variable type must be finite or inhabited. The private boundary models include a collision of variables over the integers, an omitted variable over the integers, and an omitted variable over ZMod 1. The collision uses MvPolynomial.formallyUnramified_rename_iff_moduleFinite, with the full source polynomial ring acting by multiplication by the renamed polynomial.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.formallyUnramified_rename_iff_surjective

TheoremIntegrality of polynomial variable renaming#

Over any commutative ring R, MvPolynomial.isIntegral_rename_iff states that renaming between the full polynomial rings is integral exactly when the variable map is surjective or the coefficient ring is subsingleton. See the integrality section for the precise map, generality and applications.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.isIntegral_rename_iff

TheoremAlgebraicity of polynomial variable renaming#

Over any commutative ring R, MvPolynomial.isAlgebraic_rename_iff states that the full target polynomial ring is algebraic over the full source via the specified renaming exactly when the coefficients are nontrivial and the variable map is surjective or noninjective. A collision gives a nonzero constant annihilator, even when a target variable is missed; zero coefficients give no such polynomial, even for identity renaming. This is weak algebraicity, not integrality or module finiteness. The coefficient and both variable types have independent universes, with no additional ring or finiteness hypotheses. Criterion applications are colocated with the public result. The independent positive models and negative models use stock Mathlib directly for algebraicity. The shifted-projection models over the integers and ZMod 4 use the existing integrality criterion for their missing-variable nonintegrality proofs: MvPolynomial.isIntegral_X_rename_iff.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.isAlgebraic_rename_iff

TheoremFinite presentation of commutative-ring variable renaming#

MvPolynomial.finitePresentation_rename_iff states the relative finite-presentation criterion: subsingleton coefficients, or finitely many missed target variables together with finitely many source collision participants. Both collision endpoints are counted. See the finite-presentation section for the coefficient-ring boundary and infinite-variable examples.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.finitePresentation_rename_iff

TheoremZero-variable presentations and semiring renaming#

Algebra.FinitePresentation.of_surjective_algebraMap gives a zero-variable presentation for a surjective scalar map from a commutative semiring to any semiring, with finitely generated ideal kernel. For commutative-semiring coefficients with subsingleton additive units, renaming reflects zero and every surjective variable map is finitely presented over its full source polynomial semiring. No cancellation, order, or finiteness assumption is needed. This is Mathlib's ideal-kernel convention, not congruence-based semiring finite presentation; a bottom ideal kernel need not imply injectivity.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanAlgebra.FinitePresentation.of_surjective_algebraMap

TheoremVariable renaming has an exact relative finite-type criterion#

MvPolynomial.finiteType_rename_iff characterizes finite generation of the target polynomial algebra over the source polynomial semiring: the coefficients are subsingleton or the set of missed target variables is finite. See the relative finite-type section for the algebra structure, generality and infinite-variable applications.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.finiteType_rename_iff

TheoremVariable renaming has an exact relative essentially finite-type criterion#

MvPolynomial.essFiniteType_rename_iff characterizes RingHom.EssFiniteType of renaming for arbitrary f : σ → τ over a commutative ring R, with independent coefficient and variable universes: R is subsingleton or Set.Finite ((Set.range f)ᶜ). Scalars are MvPolynomial σ R, acting on MvPolynomial τ R by p • q = rename f p * q. Essential finite type is distinct from finite type, but their criteria coincide for these maps. The worked applications contrast successor renaming over ℤ (only 0 is missed), Empty → ℕ with subsingleton coefficients (infinitely many missed variables), and even-index renaming over ℤ, which is not essentially of finite type.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.essFiniteType_rename_iff

TheoremModule finiteness of variable renaming has a sharper criterion#

For any commutative semiring R and any map f : σ → τ, with all three types in independent universes, MvPolynomial.moduleFinite_rename_iff states that the full target polynomial semiring is a finite module over the full source polynomial semiring under p • q = MvPolynomial.rename f p * q exactly when f is surjective or R is subsingleton. This is stronger than finite type: over nontrivial coefficients, Nat.succ : ℕ → ℕ misses only 0, so its renaming is of finite type but is not module-finite. These are source-polynomial scalars, not coefficient-R scalars. See the applications beside the criterion, including nonreduced and noncancellative coefficients and independent universe lifts.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.moduleFinite_rename_iff

TheoremQuasi-finiteness of commutative-ring variable renaming#

For any commutative ring R and arbitrary f : σ → τ, with all three types in independent universes, MvPolynomial.rename_quasiFinite_iff states that the original full polynomial-ring map is quasi-finite exactly when f is surjective or R is subsingleton. It uses Mathlib's residue-field-fiber convention, without a FiniteType hypothesis, and the full source-polynomial action. Module finiteness supplies the positive direction; an omitted target variable gives a surjective evaluation onto R[X], reducing the converse to Mathlib's polynomial local obstruction. The comparison MvPolynomial.rename_quasiFinite_iff_finite identifies quasi-finiteness with finiteness of that same ring homomorphism. The boundary applications contrast an omitted variable and a noninjective surjection over ℤ, and include the same omitted-variable map over ZMod 1. In the collision case, a nonzero source polynomial annihilates every target polynomial under the full renaming-induced action.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.rename_quasiFinite_iff

TheoremFinite coefficient aggregation has an exact injectivity criterion#

For types α, β and M in independent universes, an additive commutative monoid M, and any index map f : α → β, Finsupp.mapDomain_injective_iff characterizes injectivity of Finsupp.mapDomain f : (α →₀ M) → (β →₀ M): it holds exactly when f is injective or M is subsingleton. The map adds coefficients whose indices have the same image; cancellation, a ring structure and nontrivial coefficients are not required. The applications contrast the identity and a constant index map with natural-number coefficients.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanFinsupp.mapDomain_injective_iff

TheoremJoint degree-and-support profiles recover bivariate coefficients only for trivial coefficients#

For any additive commutative monoid M in an arbitrary universe, Finsupp.mapDomain_degree_support_hasLeftInverse_iff proves that pushing coefficients along d ↦ (d.degree, d.support.card), for d : Fin 2 →₀ ℕ, admits a total left inverse exactly when M is subsingleton. The profile groups coefficients jointly by total degree and the number of variables with positive exponent. The decoder may be any total function: no additive, multiplicative or linear structure is required. The applications exclude every decoder over ℕ and obtain recovery over the zero ring ZMod 1.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanFinsupp.mapDomain_degree_support_hasLeftInverse_iff

TheoremVariable-renaming kernels have an exact presentation and finite-generation criterion#

For any commutative ring R and any map f : σ → τ, with all three types in independent universes, MvPolynomial.ker_rename_eq_span_X_sub_X identifies the kernel of MvPolynomial.rename (R := R) f with the ideal generated by X i - X j for pairs satisfying f i = f j. Moreover, MvPolynomial.ker_rename_fg_iff says that this ideal is finitely generated exactly when R is subsingleton or the set {i : σ | ∃ j : σ, i ≠ j ∧ f i = f j} is finite. This counts both endpoints of every collision, not just chosen representatives; finiteness of individual fibres is not enough. Finite generation is as an ideal of the source polynomial ring MvPolynomial σ R, not as an R-module. No surjectivity or finite-variable hypothesis is required. See the applications.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.ker_rename_eq_span_X_sub_X

TheoremFraction-ring renaming is surjective, equivalently integral, exactly when it covers all variables#

For any integral domain R ([CommRing R] [IsDomain R]) and injective ρ : τ → σ, MvPolynomial.surjective_fractionRing_map_rename_iff characterizes surjectivity of the induced fraction-ring map by Function.Surjective ρ. Its source L and target K may be any commutative-ring fraction-ring realizations with their Algebra and IsFractionRing instances, without Field instances. The five universes of R, τ, σ, L and K are independent. For this same map, MvPolynomial.isIntegral_fractionRing_map_rename_iff characterizes integrality by the same condition Function.Surjective ρ. MvPolynomial.surjective_fractionRing_map_finset_iff and MvPolynomial.isIntegral_fractionRing_map_finset_iff specialize these criteria to a finite-variable stage S : Finset σ: the stage map is surjective, equivalently integral, exactly when ∀ i : σ, i ∈ S, with no finiteness hypothesis on the ambient variable type. The variable-image criterion identifies the image of X i in the range exactly when i ∈ Set.range ρ. When i ∉ Set.range ρ, MvPolynomial.not_isIntegralElem_fractionRing_map_rename_X shows that the localized variable X i in K is not integral over the image of the fraction-ring map. Thus every finite stage in infinitely many variables is neither surjective nor integral, although each finite family of fractions has a common finite stage. See the API guide.

Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

Lean

Read from the source at commit 724d9804, without running Lean.

Sources
LeanMvPolynomial.surjective_fractionRing_map_rename_iff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.