Von Neumann regular and zero-dimensional rings are LG

GN 2.2 (from EG): von Neumann regular rings are LG-rings, and more generally so are zero-dimensional rings.

Main definitions

• IsVonNeumannRegular R : every a : R satisfies a * x * a = a for some x. mathlib has no such predicate, so we introduce one; see the implementation notes.
• MvPolynomial.RepresentsUnitOn p e : local scaffolding — p takes a value that is invertible "on the idempotent e", i.e. invertible in the ring eR, without leaving R.

Main results

• isLGRing_of_forall_exists_idempotent : the shared criterion. If every a : R admits an idempotent f such that a is invertible on f and some power of a lies in (f), then R is an LG-ring.
• IsVonNeumannRegular.isLGRing : GN 2.2, von Neumann regular implies LG.
• isLGRing_of_isVonNeumannRegular_quotient_jacobson : the same with R ⧸ Jac(R) von Neumann regular, which is how GN states it.
• Ring.exists_pow_eq_pow_succ_mul : in a zero-dimensional ring every a satisfies aᵐ = aᵐ⁺¹ x for some m and x.
• isLGRing_of_krullDimLE_zero : GN 2.2, Ring.KrullDimLE 0 implies LG.

Proof idea

By the value-ideal criterion (LGRing/ValueIdeal.lean), being LG amounts to: from 1 = Σⱼ cⱼ · p(tⱼ) produce a single point where p is a unit. The tⱼ each work somewhere but nowhere in particular; the idempotents are what let their witnesses be spliced together.

Write aⱼ := p(tⱼ) and let fⱼ be the idempotent supplied by the hypothesis, so that aⱼ is invertible on fⱼ. Since a power of aⱼ lies in (fⱼ), a maximal ideal containing every fⱼ would contain every aⱼ and hence 1; so the fⱼ generate the unit ideal and ∏ⱼ (1 - fⱼ) = 0. Orthogonalising, 1 = Σⱼ eⱼ with eⱼ ≤ fⱼ, and the point s := Σⱼ eⱼ tⱼ restricts to tⱼ on the j-th block: eⱼ · s = eⱼ · tⱼ, hence eⱼ · p(s) = eⱼ · p(tⱼ) — the key step MvPolynomial.mul_aeval_eq_of_mul_eq, proved by induction on p, using only that multiplication by an idempotent is "the projection onto eR". So p(s) is invertible on every block, and the blocks exhaust R.

The two examples differ only in producing the idempotent. Von Neumann regularity gives it at once (f = ax, with a invertible on f and a ∈ (f)). For a zero-dimensional ring one first shows aᵐ = aᵐ⁺¹ x, which produces f = aᵐ xᵐ with aᵐ ∈ (f) — the power is genuinely needed here, which is why the criterion is stated with a ^ m ∈ (f) rather than a ∈ (f).

Implementation notes

IsVonNeumannRegular is a new definition, which overview §0 asks us to justify: mathlib (as pinned in lake-manifest.json) has no von Neumann regular ring predicate — its only VonNeumann namespace is Analysis.VonNeumannAlgebra, an unrelated notion. The definition is stated for CommRing because that is all this file needs and all the LG theory ever uses; the usual definition makes sense for any ring.

MvPolynomial.RepresentsUnitOn is deliberately phrased inside R, as ∃ s c, e * p(s) * c = e, rather than as MvPolynomial.RepresentsUnit over the ring eR or R ⧸ (1 - e). Every proof here is an identity between elements of R, and routing through a quotient or a subtype would force transporting polynomials back and forth for no gain.

References

• [GN] Gille, Neher, Group schemes over LG-rings and applications to cancellation theorems and Azumaya algebras, European Journal of Mathematics 11 (2025), article 42, Example 2.2.
• [EG] Estes, Guralnick, Module equivalences: local to global when primitive polynomials represent units, Journal of Algebra 77 (1982), 138–157.

Evaluation only sees a point through an idempotent

theorem MvPolynomial.mul_aeval_eq_of_mul_eq {R : Type u} [CommRing R] {n : ℕ} {e : R} (he : IsIdempotentElem e) {s t : Fin n → R} (h : ∀ (i : Fin n), e * s i = e * t i) (p : MvPolynomial (Fin n) R) : e * (aeval s) p = e * (aeval t) p

Multiplication by an idempotent is a ring map onto eR, so it cannot tell two points apart that agree after multiplication by e. This is the splicing lemma: it is what allows a witness assembled block by block to be evaluated block by block.

The proof is a direct induction on p; the multiplicative step is e·(AB) = (e·e)·(AB) = (e·A)(e·B).

def MvPolynomial.RepresentsUnitOn {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (e : R) : Prop

p represents a unit on the idempotent e: some value p(s) is invertible in the ring eR, expressed without leaving R. For e = 1 this is MvPolynomial.RepresentsUnit (MvPolynomial.RepresentsUnitOn.representsUnit), and for e = 0 it is vacuous.

Equations

• p.RepresentsUnitOn e = ∃ (s : Fin n → R) (c : R), e * (MvPolynomial.aeval s) p * c = e

theorem MvPolynomial.representsUnitOn_zero {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) : p.RepresentsUnitOn 0

theorem MvPolynomial.RepresentsUnitOn.mono {R : Type u} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} {e e' : R} (h : p.RepresentsUnitOn e) (hle : e' * e = e') : p.RepresentsUnitOn e'

Representing a unit on e is inherited by any e' below e (e' * e = e'): the same witness works, since e' factors through e.

theorem MvPolynomial.RepresentsUnitOn.add {R : Type u} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} {e₁ e₂ : R} (h₁ : IsIdempotentElem e₁) (h₂ : IsIdempotentElem e₂) (horth : e₁ * e₂ = 0) (hr₁ : p.RepresentsUnitOn e₁) (hr₂ : p.RepresentsUnitOn e₂) : p.RepresentsUnitOn (e₁ + e₂)

Gluing over orthogonal idempotents. Witnesses on e₁ and on e₂ splice into a witness on e₁ + e₂: take s := e₁ s₁ + e₂ s₂, which agrees with sₖ after multiplication by eₖ, so that eₖ · p(s) = eₖ · p(sₖ) by MvPolynomial.mul_aeval_eq_of_mul_eq; the inverses glue as e₁ c₁ + e₂ c₂, all cross terms being killed by orthogonality.

theorem MvPolynomial.RepresentsUnitOn.representsUnit {R : Type u} [CommRing R] {n : ℕ} {p : MvPolynomial (Fin n) R} (h : p.RepresentsUnitOn 1) : p.RepresentsUnit R

theorem MvPolynomial.representsUnitOn_one_sub_prod {R : Type u} [CommRing R] {n : ℕ} {ι : Type u_1} {p : MvPolynomial (Fin n) R} (f : ι → R) (hf : ∀ (i : ι), IsIdempotentElem (f i)) (hrep : ∀ (i : ι), p.RepresentsUnitOn (f i)) (T : Finset ι) : IsIdempotentElem (1 - ∏ i ∈ T, (1 - f i)) ∧ p.RepresentsUnitOn (1 - ∏ i ∈ T, (1 - f i))

Orthogonalisation, in the form the induction needs: for a family of idempotents f each of which supports a witness for p, the idempotent 1 - ∏_{i ∈ T} (1 - fᵢ) — the "union" of the blocks indexed by T — again supports one.

The step from T to insert j T writes 1 - ∏_{insert j T}(1 - fᵢ) = e + fⱼ(1 - e) with e := 1 - ∏_T (1 - fᵢ), a sum of orthogonal idempotents to which MvPolynomial.RepresentsUnitOn.add applies; the second summand lies below fⱼ, so it inherits a witness by MvPolynomial.RepresentsUnitOn.mono.

The shared criterion

theorem isLGRing_of_forall_exists_idempotent {R : Type u} [CommRing R] (h : ∀ (a : R), ∃ (f : R) (c : R), IsIdempotentElem f ∧ a * c * f = f ∧ ∃ (m : ℕ), a ^ m ∈ Ideal.span {f}) : IsLGRing R

The idempotent criterion for IsLGRing. Suppose every a : R admits an idempotent f together with a c making a invertible on f (a·c·f = f), and some power aᵐ lying in the ideal (f). Then R is an LG-ring.

The two hypotheses on f play complementary roles: a·c·f = f supplies the witness on the block f, and aᵐ ∈ (f) forces the blocks to cover Spec R, since a maximal ideal containing all the fⱼ would contain all the aⱼ and hence 1 = Σⱼ cⱼ aⱼ.

Von Neumann regular rings

def IsVonNeumannRegular (R : Type u) [CommRing R] : Prop

A commutative ring is von Neumann regular if every element a satisfies a * x * a = a for some x — equivalently, if every principal ideal is generated by an idempotent.

⚠ mathlib has no von Neumann regular ring predicate at the pinned revision (its only VonNeumann namespace is the unrelated Analysis.VonNeumannAlgebra), which is why this is defined here rather than imported. If one is added upstream, this definition should be replaced by it.

Equations

• IsVonNeumannRegular R = ∀ (a : R), ∃ (x : R), a * x * a = a

theorem IsVonNeumannRegular.isLGRing {R : Type u} [CommRing R] (h : IsVonNeumannRegular R) : IsLGRing R

GN 2.2: a von Neumann regular ring is an LG-ring.

The support idempotent of a is f = a·x: it is idempotent because axax = (axa)x = ax, the element a is invertible on it with c = x for the same reason, and a = a·(ax) lies in (f) outright — no power is needed.

theorem isLGRing_of_isVonNeumannRegular_quotient_jacobson {R : Type u} [CommRing R] (h : IsVonNeumannRegular (R ⧸ Ring.jacobson R)) : IsLGRing R

GN 2.2, in the form the source states it: it is enough that R ⧸ Jac(R) be von Neumann regular. Combine IsVonNeumannRegular.isLGRing with GPR 11.21(i) (isLGRing_iff_isLGRing_quotient_jacobson).

Zero-dimensional rings

theorem Ring.exists_pow_eq_pow_succ_mul {R : Type u} [CommRing R] [KrullDimLE 0 R] (a : R) : ∃ (m : ℕ) (x : R), a ^ m = a ^ (m + 1) * x

In a zero-dimensional ring every element satisfies aᵐ = aᵐ⁺¹ x for some m and x.

The ideal J = ⋃ₘ Ann(aᵐ) together with (a) generates everything: were both inside a maximal ideal 𝔪, then — 𝔪 being minimal prime, R having dimension zero — the multiplicative set {aⁱ s : s ∉ 𝔪} would miss 0, and a prime disjoint from it would be a prime strictly inside 𝔪 (it omits a ∈ 𝔪) yet still maximal, which is absurd. So 0 = aⁱ s for some s ∉ 𝔪, putting s in J ⊆ 𝔪. Writing 1 = c·a + z with z·aᵐ = 0 and multiplying by aᵐ gives the claim.

theorem isLGRing_of_krullDimLE_zero (R : Type u) [CommRing R] [Ring.KrullDimLE 0 R] : IsLGRing R

GN 2.2: a zero-dimensional ring is an LG-ring.

From aᵐ = aᵐ⁺¹ x (Ring.exists_pow_eq_pow_succ_mul) one gets, by iterating, aᵐ = aᵐ⁺ᵏ xᵏ for every k; taking k = m shows f := aᵐ xᵐ is idempotent, that a·x·f = f, and that aᵐ = aᵐ · f ∈ (f). This is the case the criterion's a ^ m ∈ (f) clause was written for: unlike the von Neumann regular case, a itself need not lie in (f).