R is LG iff R ⧸ Jac(R) is LG

The Jacobson-quotient half of GPR 11.21 (GN 2.1(b)): R is an LG-ring iff R ⧸ Jac(R) is. The other half of GPR 11.21 (finite products of LG-rings are LG) is not covered here — see LGRing/Products.lean.

Main results

• isLGRing_iff_isLGRing_quotient_jacobson : IsLGRing R ↔ IsLGRing (R ⧸ Ring.jacobson R).

Proof idea

Every maximal ideal 𝔪 of R contains Jac(R) (it is the intersection of all of them), so maximal ideals of R correspond exactly to maximal ideals of R ⧸ Jac(R), via 𝔪 ↦ 𝔪.map π and back via comap π, where π : R → R ⧸ Jac(R) is the quotient map — and the residue fields agree on the nose: R ⧸ 𝔪 ≅ (R ⧸ Jac(R)) ⧸ 𝔪.map π (residueFieldQuotientJacobsonEquiv, which is mathlib's third isomorphism theorem DoubleQuot.quotQuotEquivQuotOfLE, applicable because Jac(R) ≤ 𝔪). Transporting a witness for p.RepresentsUnit back and forth along this isomorphism and along MvPolynomial.map π (aeval_comp_residueFieldQuotientJacobsonEquiv, aeval_map_quotient) turns "p represents a unit at every residue field of R" into "p's image represents a unit at every residue field of R ⧸ Jac(R)" and back (represents_unit_quotient_jacobson_of_forall, represents_unit_of_forall_quotient_jacobson).

The one place this needs more than bookkeeping: going from "p's image represents a unit over R ⧸ Jac(R)" back to "p represents a unit over R" needs that a witness whose image is a unit modulo Jac(R) was already a unit in R (isUnit_of_isUnit_image_jacobson) — this is specific to the Jacobson radical (it is false for a general quotient) and is where 1 - j being a unit for j ∈ Jac(R) actually gets used.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.21(i).
• [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(b).

theorem isUnit_of_isUnit_image_jacobson {R : Type u} [CommRing R] (x : R) (h : IsUnit ((Ideal.Quotient.mk (Ring.jacobson R)) x)) : IsUnit x

If the image of x under R → R ⧸ Jac(R) is a unit, so is x itself. This is specific to the Jacobson radical: xz ≡ 1 mod Jac(R) gives xz - 1 ∈ Jac(R), hence xz is a unit (elements of 1 + Jac(R) are always units), hence (commutativity) x is a unit.

noncomputable def residueFieldQuotientJacobsonEquiv {R : Type u} [CommRing R] (𝔪 : Ideal R) [h𝔪 : 𝔪.IsMaximal] : R ⧸ 𝔪 ≃+* (R ⧸ Ring.jacobson R) ⧸ Ideal.map (Ideal.Quotient.mk (Ring.jacobson R)) 𝔪

The residue field of R at a maximal ideal 𝔪 agrees with the residue field of R ⧸ Jac(R) at the corresponding maximal ideal 𝔪.map π (π the quotient-by-Jac(R) map). This is mathlib's third isomorphism theorem DoubleQuot.quotQuotEquivQuotOfLE, which applies because Jac(R) ≤ 𝔪.

Equations

• residueFieldQuotientJacobsonEquiv 𝔪 = (DoubleQuot.quotQuotEquivQuotOfLE ⋯).symm

@[simp]

theorem residueFieldQuotientJacobsonEquiv_apply {R : Type u} [CommRing R] (𝔪 : Ideal R) [𝔪.IsMaximal] (r : R) : (residueFieldQuotientJacobsonEquiv 𝔪) ((Ideal.Quotient.mk 𝔪) r) = (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ring.jacobson R)) 𝔪)) ((Ideal.Quotient.mk (Ring.jacobson R)) r)

theorem aeval_comp_residueFieldQuotientJacobsonEquiv {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (𝔪 : Ideal R) [𝔪.IsMaximal] (s : Fin n → R ⧸ 𝔪) : (residueFieldQuotientJacobsonEquiv 𝔪) ((MvPolynomial.aeval s) p) = (MvPolynomial.aeval fun (i : Fin n) => (residueFieldQuotientJacobsonEquiv 𝔪) (s i)) ((MvPolynomial.map (Ideal.Quotient.mk (Ring.jacobson R))) p)

aeval commutes with residueFieldQuotientJacobsonEquiv: evaluating p at a point of R ⧸ 𝔪 and transporting the result along the equivalence agrees with reducing p's coefficients mod Jac(R) first and evaluating at the transported point.

theorem aeval_map_quotient {R : Type u} [CommRing R] (J : Ideal R) {n : ℕ} (p : MvPolynomial (Fin n) R) (t : Fin n → R) : (Ideal.Quotient.mk J) ((MvPolynomial.aeval t) p) = (MvPolynomial.aeval fun (i : Fin n) => (Ideal.Quotient.mk J) (t i)) ((MvPolynomial.map (Ideal.Quotient.mk J)) p)

aeval commutes with reduction mod any ideal J: evaluating p at a point of R and then reducing mod J agrees with reducing p's coefficients mod J first and evaluating at the reduced point.

theorem represents_unit_quotient_jacobson_of_forall {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (hwit : ∀ (𝔪 : Ideal R) [𝔪.IsMaximal], p.RepresentsUnit (R ⧸ 𝔪)) (𝔐 : Ideal (R ⧸ Ring.jacobson R)) [𝔐.IsMaximal] : ((MvPolynomial.map (Ideal.Quotient.mk (Ring.jacobson R))) p).RepresentsUnit ((R ⧸ Ring.jacobson R) ⧸ 𝔐)

If p represents a unit at every residue field of R, its image under R → R ⧸ Jac(R) represents a unit at every residue field of R ⧸ Jac(R): every maximal ideal 𝔐 of R ⧸ Jac(R) is 𝔪.map π for 𝔪 := comap π 𝔐 maximal in R, and the residue fields agree via residueFieldQuotientJacobsonEquiv.

theorem represents_unit_of_forall_quotient_jacobson {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (hwit : ∀ (𝔐 : Ideal (R ⧸ Ring.jacobson R)) [𝔐.IsMaximal], ((MvPolynomial.map (Ideal.Quotient.mk (Ring.jacobson R))) p).RepresentsUnit ((R ⧸ Ring.jacobson R) ⧸ 𝔐)) (𝔪 : Ideal R) [𝔪.IsMaximal] : p.RepresentsUnit (R ⧸ 𝔪)

Conversely, if the image of p under R → R ⧸ Jac(R) represents a unit at every residue field of R ⧸ Jac(R), then p itself represents a unit at every residue field of R: for 𝔪 maximal in R, 𝔪.map π is maximal in R ⧸ Jac(R) (Jac(R) ≤ 𝔪 supplies the kernel hypothesis), and the residue fields agree via residueFieldQuotientJacobsonEquiv.

theorem isLGRing_iff_isLGRing_quotient_jacobson {R : Type u} [CommRing R] : IsLGRing R ↔ IsLGRing (R ⧸ Ring.jacobson R)

GPR 11.21(i): R is an LG-ring iff R ⧸ Jac(R) is.