Semilocal rings are LG-rings

GPR 11.22: a commutative ring with only finitely many maximal ideals is an LG-ring. This is the workhorse instance for the rest of the development — local rings, Artinian rings and fields are all semilocal.

Semilocality is expressed in mathlib's way, as [Finite (MaximalSpectrum R)].

Main results

• IsLGRing.of_ringEquiv : the LG property transfers along a ring isomorphism.
• IsLGRing.quotient_span_one_sub_of_isIdempotentElem : an idempotent factor of an LG ring is LG.
• isLGRing_of_finite_maximalSpectrum : GPR 11.22, semilocal implies LG.
• isLGRing_of_isLocalRing : every commutative local ring is LG.

Proof idea

Assemble the two halves of GPR 11.21. Writing 𝔪₁, …, 𝔪ₖ for the maximal ideals, Jac(R) = 𝔪₁ ⊓ ⋯ ⊓ 𝔪ₖ is a finite intersection, so the Chinese Remainder Theorem (Ideal.quotientInfEquivQuotientProd, applied k times) identifies R ⧸ Jac(R) with a finite product of the residue fields R ⧸ 𝔪ᵢ. Fields are LG (isLGRing_of_field), binary products of LG-rings are LG (isLGRing_prod_iff), so R ⧸ Jac(R) is LG, and R itself is LG by isLGRing_iff_isLGRing_quotient_jacobson.

The induction is on a Finset of maximal ideals rather than on a cardinality, which keeps everything inside R: isLGRing_quotient_biInf proves R ⧸ (⨅ 𝔪 ∈ s, 𝔪) is LG for every finite set s of maximal ideals, with the empty set giving the zero ring (isLGRing_of_subsingleton, in LGRing/Examples.lean).

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.22.
• [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.

theorem IsLGRing.of_ringEquiv {R : Type u} [CommRing R] {S : Type u} [CommRing S] (e : R ≃+* S) (hR : IsLGRing R) : IsLGRing S

The LG property transfers along a ring isomorphism: maximal ideals correspond (Ideal.map_isMaximal_of_equiv), the residue fields correspond (Ideal.quotientEquiv), and MvPolynomial.map transports polynomials both ways.

theorem IsLGRing.quotient_span_one_sub_of_isIdempotentElem {R : Type u} [CommRing R] (hLG : IsLGRing R) {e : R} (he : IsIdempotentElem e) : IsLGRing (R ⧸ Ideal.span {1 - e})

An idempotent factor of an LG ring is LG.

The complementary ideals (1 - e) and (e) have zero intersection, so the Chinese remainder theorem identifies the original ring with the product of the two quotient rings. The assertion then follows from GPR 11.21(ii).

theorem isLGRing_quotient_biInf {R : Type u} [CommRing R] (s : Finset (Ideal R)) (hs : ∀ 𝔪 ∈ s, 𝔪.IsMaximal) : IsLGRing (R ⧸ ⨅ 𝔪 ∈ s, 𝔪)

For any finite set s of maximal ideals of R, the quotient R ⧸ (⨅ 𝔪 ∈ s, 𝔪) is an LG-ring. Induction on s: the empty set gives the zero ring, and the induction step splits off one maximal ideal by the Chinese Remainder Theorem and applies isLGRing_prod_iff.

theorem isLGRing_of_finite_maximalSpectrum (R : Type u) [CommRing R] [Finite (MaximalSpectrum R)] : IsLGRing R

GPR 11.22: every semilocal ring is an LG-ring. Semilocality is mathlib's [Finite (MaximalSpectrum R)]: R has only finitely many maximal ideals.

theorem isLGRing_of_isLocalRing (R : Type u) [CommRing R] [IsLocalRing R] : IsLGRing R

Every commutative local ring is an LG ring, since it has a unique maximal ideal and hence is semilocal.