The value ideal, and a finitary criterion for IsLGRing

The defining biconditional of IsLGRing quantifies over all residue fields. This file replaces that quantifier by a single ideal-theoretic condition on R itself: p represents a unit over every residue field iff the ideal generated by all the values p(s), s : Fin n → R, is the unit ideal.

The point is that the resulting criterion is finitary: 1 ∈ Ideal.span {p(s) : s} unwinds to a single equation 1 = Σᵢ cᵢ · p(sᵢ) involving finitely many elements of R. Every example in LGRing/DirectLimit.lean and LGRing/ZeroDimensional.lean is proved by starting from that equation, and the direct-limit example is exactly the observation that a finitary condition passes to filtered colimits.

Main definitions

• MvPolynomial.valueIdeal p : the ideal of R generated by the set of values of p.

Main results

• MvPolynomial.representsUnit_quotient_iff : p represents a unit over the residue field R ⧸ 𝔪 iff some value p(s), with s taken in R itself, escapes 𝔪.
• MvPolynomial.valueIdeal_eq_top_iff : p.valueIdeal = ⊤ iff p represents a unit over every residue field.
• isLGRing_iff_forall_valueIdeal_eq_top : R is LG iff every p with p.valueIdeal = ⊤ represents a unit over R.

Implementation notes

MvPolynomial.representsUnit_quotient_iff is what makes the whole file work, and it is where the maximality of 𝔪 is used: over a field a nonzero element is a unit, so the existence of a witness in (R ⧸ 𝔪)ⁿ can be traded for the existence of a witness in Rⁿ — the reduction map Rⁿ → (R ⧸ 𝔪)ⁿ is surjective, so nothing is lost by lifting. As in LGRing/Defs.lean we use the Prop-valued IsField (R ⧸ 𝔪) rather than Ideal.Quotient.field, to avoid introducing a second Field structure on the quotient.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.20.
• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, §2.1.

def MvPolynomial.valueIdeal {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) : Ideal R

The value ideal of p : R[X₁,…,Xₙ]: the ideal of R generated by the values p(s) as s ranges over Rⁿ. It is the unit ideal exactly when p represents a unit over every residue field (MvPolynomial.valueIdeal_eq_top_iff), which is the hypothesis side of the LG axiom.

Equations

• p.valueIdeal = Ideal.span (Set.range fun (s : Fin n → R) => (MvPolynomial.aeval s) p)

theorem MvPolynomial.aeval_mem_valueIdeal {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (s : Fin n → R) : (aeval s) p ∈ p.valueIdeal

theorem MvPolynomial.valueIdeal_le_iff {R : Type u} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} {I : Ideal R} : p.valueIdeal ≤ I ↔ ∀ (s : Fin n → R), (aeval s) p ∈ I

theorem MvPolynomial.quotient_mk_aeval {R : Type u} [CommRing R] {n : ℕ} (I : Ideal R) (p : MvPolynomial (Fin n) R) (s : Fin n → R) : (Ideal.Quotient.mk I) ((aeval s) p) = (aeval fun (i : Fin n) => (Ideal.Quotient.mk I) (s i)) p

Evaluating over R and reducing mod 𝔪 is evaluating over R ⧸ 𝔪 at the reduced point.

theorem MvPolynomial.representsUnit_quotient_iff {R : Type u} [CommRing R] {n : ℕ} (𝔪 : Ideal R) [h𝔪 : 𝔪.IsMaximal] (p : MvPolynomial (Fin n) R) : p.RepresentsUnit (R ⧸ 𝔪) ↔ ∃ (s : Fin n → R), (aeval s) p ∉ 𝔪

p represents a unit over the residue field R ⧸ 𝔪 exactly when some value of p at a point of R escapes 𝔪.

Both directions use that R ⧸ 𝔪 is a field: forwards, a unit is nonzero; backwards, a nonzero element is a unit. The passage between witnesses over R ⧸ 𝔪 and witnesses over R is the surjectivity of Ideal.Quotient.mk.

theorem MvPolynomial.valueIdeal_eq_top_iff {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) : p.valueIdeal = ⊤ ↔ ∀ (𝔪 : Ideal R) [𝔪.IsMaximal], p.RepresentsUnit (R ⧸ 𝔪)

The value ideal is the unit ideal exactly when p represents a unit over every residue field: "p.valueIdeal ≠ ⊤" and "p misses a residue field" are both the statement that some maximal ideal swallows every value of p.

The finitary unwinding

p.valueIdeal = ⊤ says 1 lies in the span of the values of p, which is a statement about a single equation in finitely many elements of R. These two lemmas are that translation, and they are the only interface the examples use.

theorem MvPolynomial.exists_sum_mul_aeval_eq_one {R : Type u} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} (h : p.valueIdeal = ⊤) : ∃ (k : ℕ) (c : Fin k → R) (t : Fin k → Fin n → R), ∑ j : Fin k, c j * (aeval (t j)) p = 1

Unwinding p.valueIdeal = ⊤: finitely many points t j of Rⁿ whose values at p combine to 1.

theorem MvPolynomial.valueIdeal_eq_top_of_sum_mul_aeval_eq_one {R : Type u} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} {k : ℕ} (c : Fin k → R) (t : Fin k → Fin n → R) (h : ∑ j : Fin k, c j * (aeval (t j)) p = 1) : p.valueIdeal = ⊤

Conversely, one such equation forces p.valueIdeal = ⊤.

theorem isLGRing_iff_forall_valueIdeal_eq_top (R : Type u) [CommRing R] : IsLGRing R ↔ ∀ (n : ℕ) (p : MvPolynomial (Fin n) R), p.valueIdeal = ⊤ → p.RepresentsUnit R

A finitary criterion for IsLGRing. R is an LG-ring iff, whenever the values of a polynomial p generate the unit ideal, p already takes a unit value.

This is the form of the LG axiom used throughout LGRing/DirectLimit.lean and LGRing/ZeroDimensional.lean: unlike the definition, its hypothesis unwinds to a single equation 1 = Σᵢ cᵢ · p(sᵢ) in finitely many elements of R.