Heights of homogeneous… to Jacobson radicals of…
Headline results
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
TheoremHeights of homogeneous polynomial evaluations#
Over any field with
Height.AdmissibleAbsValues, a homogeneous polynomial family of common degree
d, with finite input and output coordinate types and no nonzero common zero
over an algebraic closure, has evaluation height uniformly comparable to the
input height raised to d. More precisely,
Height.exists_logHeight_eval_sub_mul_bound
bounds the difference between evaluation logarithmic height and d times input
logarithmic height, while
Height.exists_mulHeight_eval_bounds
bounds positive multiplicative height above and below by reciprocal constant
factors, with comparison constant at least one. The coordinate universes are
independent. Zero tuples, degree zero and empty coordinate types are included.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
Height.exists_logHeight_eval_sub_mul_bound(theorem), declared in MultivariatePolynomials/Height/Homogeneous.lean, line 40.
Read from the source at commit 724d9804, without running Lean.
Sources
DefinitionHomogeneous polynomial maps on projective coordinate spaces#
MvPolynomial.projectivize
sends a nonzero tuple's class to the class of its polynomial evaluation tuple.
The coefficients may lie in any commutative semiring equipped with a homomorphism
to the field of points. A common homogeneity degree and nonvanishing on nonzero
input tuples make this map well-defined; its values on these classes characterize
it uniquely. Coordinate variables induce the identity, and homogeneous
substitution induces composition. The coordinate types may be infinite or empty,
their universes are independent, and the degree may be zero. With coefficients
in the field of points, finite coordinates and admissible absolute values, the
projective height comparisons
descend the tuple bounds under the same algebraic-closure common-zero condition.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.projectivize(def), declared in MultivariatePolynomials/Projectivization.lean, line 74.
Read from the source at commit 724d9804, without running Lean.
Sources
Homogeneous coordinate-power certificates.
For an arbitrarily indexed homogeneous family p : J → MvPolynomial I R
of common degree d over any commutative semiring, with finitely many
variables, the
certificate module
states that radical membership of every variable gives finitely supported
coefficients q : I → (J →₀ MvPolynomial I R) and one common M, with
every q i j homogeneous of degree M and
(q i).sum (fun j r => r * p j) = X i ^ (M + d). Over a field, the second
statement replaces radical membership by absence of nonzero common zeros
over the algebraic closure. The finite-index function-sum corollaries
exists_homogeneous_sum_mul_eq_X_pow and
exists_homogeneous_sum_mul_eq_X_pow_of_forall_aeval_eq_zero convert these
conclusions to ∑ j, q (i, j) * p j = X i ^ (M + d) using
Finsupp.sum_fintype.
The variable, generator and coefficient universes are independent; empty
types, trivial semirings and degree zero are included. The
coordinate-power and constant-one examples
verify the hypotheses and explicit certificates independently of the core statements.
DefinitionPolynomial closed points and algebraic-closure orbits#
For independently
universed fields K and L with their given Algebra K L and
IsAlgClosure K L,
Polynomial.algAutOrbitEquivMaximalSpectrum
identifies the existing quotient of L by its K-algebra automorphism orbits
with MaximalSpectrum K[X]. The ideal of the orbit of a is the kernel of
aeval a, equivalently the ideal generated by minpoly K a. No perfectness
or separability is assumed. This is a set equivalence; over an imperfect
field, a singleton orbit need not be a rational point.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
Polynomial.algAutOrbitEquivMaximalSpectrum(def), declared in MultivariatePolynomials/PolynomialClosedPoints.lean, line 62.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremInfinitely many maximal ideals of polynomial rings#
Every nontrivial
commutative ring R has infinitely many maximal ideals in R[X], including
when R is a finite field, by
MaximalSpectrum.infinite_polynomial.
For any commutative ring R and arbitrary variable type σ, the maximal
spectrum of MvPolynomial σ R is infinite exactly when R is nontrivial
and either σ is nonempty or the maximal spectrum of R is infinite, by
MaximalSpectrum.infinite_mvPolynomial_iff.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MaximalSpectrum.infinite_polynomial(theorem), declared in MultivariatePolynomials/PrimeSpectrum.lean, line 190.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremFactorization uniqueness from a regular crossed resultant#
Over any commutative
ring, let G,G' have degree at most m and H,H' degree at most n, with
G.coeff m = G'.coeff m and H.coeff n = H'.coeff n. If G * H = G' * H'
and Polynomial.resultant G' H m n is regular, then G = G' and H = H', by
Polynomial.eq_and_eq_of_mul_eq_mul_of_isRegular_resultant.
Neither monicity nor positive nominal degrees are required, and the ring may have
zero divisors.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
Polynomial.eq_and_eq_of_mul_eq_mul_of_isRegular_resultant(theorem), declared in MultivariatePolynomials/ResultantFactorization.lean, line 62.
Read from the source at commit 724d9804, without running Lean.
Sources
Non-unital rings of additive units. For a non-unital, non-associative semiring
R, the existing AddUnits R inherits multiplication and forms a non-unital,
non-associative ring. Associativity and commutativity are inherited when present.
For every non-unital, non-associative ring S, value inclusion induces
(S →ₙ+* AddUnits R) ≃ (S →ₙ+* R), with a unique factorization through the
additive units. See AddUnits.
TheoremNonconstant coefficients of polynomial units#
Over any commutative semiring
R, every coefficient at a nonzero exponent of a unit in MvPolynomial σ R
is additively invertible, by
MvPolynomial.isAddUnit_coeff_of_isUnit.
The variable type is arbitrary, including empty and infinite types.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.isAddUnit_coeff_of_isUnit(theorem), declared in MultivariatePolynomials/UnitCoefficients.lean, line 28.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremPolynomial units over commutative semirings#
For any commutative semiring
R and arbitrary variable type σ, a polynomial in MvPolynomial σ R is a
unit if and only if its constant coefficient is a unit and its coefficient at
every nonzero exponent is both nilpotent and additively invertible, by
MvPolynomial.isUnit_iff_coeff_isNilpotent_isAddUnit.
The coefficient and variable types have independent universes; empty variable
types and the zero semiring are included. The lemma
MvPolynomial.isUnit_coeff_zero_and_isNilpotent_isAddUnit_iff
identifies the coefficient conditions over a commutative ring with those in
Mathlib's MvPolynomial.isUnit_iff. The sufficiency direction remains available as
MvPolynomial.isUnit_of_coeff_isNilpotent_isAddUnit.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.isUnit_iff_coeff_isNilpotent_isAddUnit(theorem), declared in MultivariatePolynomials/UnitCriterion.lean, line 40.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremPrime coefficient extensions over commutative semirings#
For a commutative
semiring R, any variable type σ and ideal I, primality of I together
with ∀ a b : R, a ∈ I → a + b ∈ I → b ∈ I implies primality of
I.map MvPolynomial.C,
by MvPolynomial.isPrime_map_C_of_subtractive.
For nonempty σ, these conditions are also necessary, by
MvPolynomial.isPrime_map_C_iff.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.isPrime_map_C_of_subtractive(theorem), declared in MultivariatePolynomials/CoefficientIdealPrime.lean, line 34.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremMaximal coefficient extensions over commutative semirings#
For a commutative
semiring R, any variable type σ and ideal I,
(I.map MvPolynomial.C).IsMaximal ↔ I.IsMaximal ∧ IsEmpty σ, by
MvPolynomial.isMaximal_map_C_iff.
With nonempty σ, no coefficient extension is maximal. For proper I,
the constant-coefficient preimage is a strict intermediate ideal.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.isMaximal_map_C_iff(theorem), declared in MultivariatePolynomials/CoefficientIdealMaximal.lean, line 61.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremFinite coefficient-product equations determine whole products#
For independent
commutative semirings C and R, an arbitrary homomorphism φ : C →+* R,
nominal sizes m,n, seeds g,h : Polynomial C and arbitrary target coefficient
point, MvPolynomial.eval₂Hom_coefficientProduct_eq_iff
identifies the finite evaluated equations with equality of the entire ordinary
perturbed product to T. It assumes target-side bounds
(g.map φ).natDegree ≤ m, (h.map φ).natDegree ≤ n, T.natDegree ≤ m + n, and
T.coeff (m + n) = (g.map φ).coeff m * (h.map φ).coeff n. Zero sizes, mapped
degree drops and trivial semirings are included; no source degree bound or
injectivity of φ is required.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.eval₂Hom_coefficientProduct_eq_iff(theorem), declared in MultivariatePolynomials/CoefficientProduct.lean, line 354.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremRadicals of coefficient-ideal extensions#
For any commutative ring R,
arbitrary variable type σ and ideal I : Ideal R,
MvPolynomial.radical_map_C
says that extending I along the constant-polynomial map commutes with radicals.
MvPolynomial.mem_radical_map_C_iff
characterizes radical membership coefficientwise: a polynomial lies in the
radical of the extended ideal exactly when every coefficient lies in I.radical.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.radical_map_C(theorem), declared in MultivariatePolynomials/IdealExtension.lean, line 37.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremScalar annihilators and non-zero-divisors#
For any commutative semiring
R and arbitrary variable type σ,
MvPolynomial.mem_nonZeroDivisors_iff
characterizes non-zero-divisors by the absence of a nonzero scalar in the
original coefficient semiring annihilating every coefficient. No individual
coefficient need be a non-zero-divisor.
MvPolynomial.eq_zero_of_mul_eq_zero_of_smul
shows that a polynomial with no nonzero scalar annihilator has no nonzero
polynomial annihilator. The results allow empty or infinite variable types,
independent universes and trivial coefficient semirings. The interpretation
in terms of IsRegular is asserted only over commutative rings.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.mem_nonZeroDivisors_iff(theorem), declared in MultivariatePolynomials/Regularity.lean, line 172.
Read from the source at commit 724d9804, without running Lean.
Sources
DefinitionThe degree-zero homogeneous component#
For any commutative semiring
R and arbitrary variable type σ,
MvPolynomial.gradeZeroAlgEquiv
identifies R as an R-algebra with Mathlib's original degree-zero homogeneous
component. Its forward map is the inherited coefficient algebra map, with
ambient polynomial C r; its inverse is constantCoeff. The construction uses
independent universes and commutes with coefficient homomorphisms in the
ambient polynomial algebras, without finiteness or nontriviality hypotheses.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.gradeZeroAlgEquiv(def), declared in MultivariatePolynomials/GradeZero.lean, line 40.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremCoefficient ideals over commutative semirings#
For any commutative
semiring R, ideal I and arbitrary variable type σ,
MvPolynomial.coeffsIn_eq_restrictScalars_map_C
identifies the extension Ideal.map C I, restricted to the canonical
coefficient action, with Mathlib's coefficient submodule coeffsIn σ I.
Polynomial membership is therefore coefficientwise membership, and
contraction along C recovers I.
MvPolynomial.ker_map_eq_map_C
identifies the kernel of a coefficient map with the extension of its kernel.
Coefficients, target coefficients and variables have independent universes;
no ring, finiteness or nontriviality hypothesis is needed. The
natural-number example
separates 2 * X from X for the proper extended ideal (2) and for
coefficient reduction modulo two.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.coeffsIn_eq_restrictScalars_map_C(theorem), declared in MultivariatePolynomials/CoefficientIdeal.lean, line 75.
Read from the source at commit 724d9804, without running Lean.
Sources
DefinitionSquare witnesses for failure of subtractivity#
Over any commutative
semiring R, for i : σ and a b : R,
MvPolynomial.subtractiveWitness
is C a + C b * X i + C (a + b) * X i ^ 2, with linear coefficient b.
Its square belongs to I.map C if a ∈ I and a + b ∈ I, while
b ∉ I excludes the witness itself. Thus a radical (in particular prime)
extension over nonempty variables forces subtractivity. Coefficient and
variable universes are independent; no finiteness or nontriviality is needed.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.subtractiveWitness(def), declared in MultivariatePolynomials/CoefficientIdealSubtractive.lean, line 79.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremPowers of augmented coefficient ideals#
For any commutative semiring
R, ideal I, natural number n, arbitrary variable type σ, and polynomial
p, MvPolynomial.mem_pow_comap_constantCoeff_iff_coeff_mem_pow
characterizes membership in (I.comap constantCoeff) ^ n: the coefficient
at each exponent d belongs to I ^ (n - d.sum (fun _ k => k)).
Subtraction is truncated in ℕ, so degrees at least n impose no
restriction, rather than vanishing. Coefficients and variables have
independent universes; empty or infinite variables and trivial coefficient
semirings are allowed. The bottom coefficient ideal recovers Mathlib's
variable-ideal power criterion. The
integer and boundary examples
apply the criterion to 2 * X ∈ (2, X)², contrast the constant 2, and
include the zeroth power and empty variables.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.mem_pow_comap_constantCoeff_iff_coeff_mem_pow(theorem), declared in MultivariatePolynomials/AugmentedIdealPowers.lean, line 150.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremPrimary coefficient ideals#
Over any commutative semiring R,
MvPolynomial.isPrimary_map_C_of_subtractive
extends a primary ideal I satisfying a ∈ I → a + b ∈ I → b ∈ I to a
primary coefficient ideal, for every variable type σ. When σ is nonempty,
MvPolynomial.isPrimary_map_C_iff_subtractive
proves that primaryness and this subtractivity condition are also necessary.
For a commutative ring, subtractivity is automatic, and
MvPolynomial.isPrimary_map_C_iff
gives the equivalence without any restriction on σ. Coefficients and
variables have independent universes; empty variable types and the unit ideal
are included, with no Noetherian or nontriviality hypothesis. The
integer example extends the
primary, nonradical ideal (4).
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.isPrimary_map_C_of_subtractive(theorem), declared in MultivariatePolynomials/Primary.lean, line 71.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremSupplied primary families and deletion irredundance#
Over a commutative
semiring R, for an ideal I and family Q : ι → Ideal R,
MvPolynomial.primary_family_map_C_iff_of_subtractive
assumes a ∈ Q i → a + b ∈ Q i → b ∈ Q i for each component. For every variable
type σ, it equates I.map C = ⨅ i, (Q i).map C with all mapped components
primary to I = ⨅ i, Q i with all original components primary. For nonempty
σ, MvPolynomial.primary_family_map_C_iff_subtractive
gives the exact equivalence with I = ⨅ i, Q i and componentwise primaryness
and subtractivity, recovering the latter from the mapped primary family.
The ring theorem
MvPolynomial.primary_family_map_C_iff
specializes the first equivalence using automatic subtractivity, for every σ.
The intersection itself need not be primary. Over any commutative semiring,
MvPolynomial.irredundant_iInf_map_C_iff
preserves and reflects the condition that each intersection of the other
components is not contained in the omitted component, without subtractivity.
Indices may form any sort; coefficient, variable and index universes are
independent. Empty or infinite families are allowed, with no finiteness or
Noetherian hypothesis. These statements give no existence, uniqueness or
associated-prime claim. The
integer model
uses the ring equivalence and deletion irredundance for (12) = (4) ∩ (3).
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.primary_family_map_C_iff_of_subtractive(theorem), declared in MultivariatePolynomials/PrimaryDecomposition.lean, line 46.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremNilpotent coefficients and irreducible polynomial spectra#
For any
commutative semiring R and arbitrary variable type σ,
MvPolynomial.isNilpotent_iff_coeff
characterizes nilpotent polynomials by nilpotence of every coefficient.
PrimeSpectrum.irreducibleSpace_mvPolynomial_iff
states that PrimeSpectrum (MvPolynomial σ R) is irreducible exactly when
PrimeSpectrum R is irreducible. Coefficients and variables have independent
universes; empty or infinite variables and trivial coefficients are allowed.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
MvPolynomial.isNilpotent_iff_coeff(theorem), declared in MultivariatePolynomials/Nilpotent.lean, line 131.
Read from the source at commit 724d9804, without running Lean.
Sources
TheoremJacobson radicals of coefficient ideals#
For any commutative ring R,
ideal I and nonempty variable type σ,
Ideal.jacobson_map_mvPolynomial_C
identifies Ideal.jacobson (I.map C) with I.radical.map C.
In particular, the Jacobson radical of zero in MvPolynomial σ R is its
nilradical. Coefficient and variable universes are independent; no
Jacobson-ring, Noetherian, properness or nontriviality hypothesis is needed.
The integer example separates
the extended ideal (4) from its proper Jacobson radical using 2 * X.
Quoted from the headline results in README.md of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.
Lean
Ideal.jacobson_map_mvPolynomial_C(theorem), declared in MultivariatePolynomials/Jacobson.lean, line 87.
Read from the source at commit 724d9804, without running Lean.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.