Documentation

LeanPool.CompositionAlgebrasOverRings.LGRing.Defs

LG rings #

Defines IsLGRing R (GPR 11.20, GN 2.1): a commutative ring R is an LG-ring ("local–global ring") if, for every n and every f ∈ R[X₁,…,Xₙ], f represents a unit over R iff f represents a unit over every residue field R/𝔪, 𝔪 maximal. LG rings are the class of commutative rings where most results of undergraduate linear algebra for vector spaces also hold for finitely generated projective modules — see the overview's "Why LG rings" section.

Main definitions #

Main results #

Implementation notes #

GPR 11.20 states the defining biconditional using residue fields, and remarks that it is equivalent to use the localization R_𝔪 instead. GN 2.1 adds a third equivalent formulation, "represents a unit over every field F ∈ R-alg" — but this project does not reprove that three-way equivalence, and an earlier version of this file took that third formulation as the definition, which turned out to make GPR 11.21 (R LG iff R ⧸ Jac(R) LG) genuinely harder to prove: a field receiving R through a non-maximal prime need not have any relationship to a residue field of R, so the bridge between the two rings' field-algebras breaks down. Residue fields of R and of R ⧸ Jac(R) correspond exactly (every maximal ideal contains the Jacobson radical), which is what makes LGRing/Jacobson.lean go through. So this file uses GPR's own formulation (residue fields), matching the primary source, not the alternative from GN.

Constructing the Field (R ⧸ 𝔪) instance from 𝔪.IsMaximal (via Ideal.Quotient.field) is a well-known mathlib performance/diamond hazard when combined with other instances derived from the same quotient in the same context. We avoid it entirely by working with the Prop-valued IsField (R ⧸ 𝔪) (via Ideal.Quotient.maximal_ideal_iff_isField_quotient) instead of the bundled Field structure wherever we need "nonzero ⇒ invertible" — IsField carries no data, so there is nothing for two different derivations of it to disagree about.

The forward direction of the biconditional (RepresentsUnit p R → ∀ 𝔪, RepresentsUnit p (R ⧸ 𝔪)) holds for any commutative ring R, LG or not: IsUnit is preserved by every ring homomorphism, so a witness over R pushes forward to a witness over any quotient. The entire content of the LG axiom is in the converse.

References #

source
def MvPolynomial.RepresentsUnit {R : Type u} [CommRing R] {n : ℕ} (p : MvPolynomial (Fin n) R) (S : Type v) [CommRing S] [Algebra R S] :
Prop

p, viewed as a polynomial over the R-algebra S, represents a unit: it evaluates to a unit at some point of S.

Equations
Instances For
    source
    def IsLGRing (R : Type u) [CommRing R] :
    Prop

    R is an LG-ring (GPR 11.20, "local–global ring"): a polynomial in finitely many variables over R represents a unit over R iff it represents a unit over every residue field R ⧸ 𝔪, 𝔪 maximal. See the implementation notes for why this formulation (rather than GN's "every field F ∈ R-alg" alternative) is taken as the definition.

    Equations
    Instances For
      source
      theorem MvPolynomial.aeval_map_comm {R : Type u_1} [CommRing R] {R' : Type u_2} [CommRing R'] (φ : R →+* R') {S : Type u_3} [CommRing S] [Algebra R S] {S' : Type u_4} [CommRing S'] [Algebra R' S'] (ψ : S →+* S') (hcomm : ψ.comp (algebraMap R S) = (algebraMap R' S').comp φ) {n : ℕ} (s : Fin n → S) (p : MvPolynomial (Fin n) R) :
      (aeval fun (i : Fin n) => ψ (s i)) ((map φ) p) = ψ ((aeval s) p)

      If ψ : S → S' sits over φ : R → R' — that is, the square of structure maps commutes — then evaluating p over S and transporting agrees with reducing p's coefficients along φ and evaluating over S'. Compare aeval_map_quotient in LGRing/Jacobson.lean, which is the special case of reduction modulo an ideal.

      Every transport of MvPolynomial.RepresentsUnit in this directory is an instance of this square: see MvPolynomial.RepresentsUnit.mapOfComm and MvPolynomial.RepresentsUnit.ofMapOfComm in LGRing/Products.lean.

      Units lift along quotients by a principal ideal #

      The test polynomial is u + b·T (one variable): linear, not quadratic, and the argument routes entirely through the LG axiom rather than through any explicit field-case computation.

      source
      noncomputable def linUC {R : Type u} [CommRing R] (u b : R) :
      MvPolynomial (Fin 1) R

      The affine polynomial u + b·T, in one variable.

      Equations
      Instances For
        source
        @[simp]
        theorem aeval_linUC {R : Type u} [CommRing R] {S : Type v} [CommRing S] [Algebra R S] (s : Fin 1 → S) (u b : R) :
        (MvPolynomial.aeval s) (linUC u b) = (algebraMap R S) u + (algebraMap R S) b * s 0
        source
        theorem exists_isUnit_of_isUnit_quotient {R : Type u} [CommRing R] (hLG : IsLGRing R) (b : R) (ū : (R ⧸ Ideal.span {b})ˣ) :
        ∃ (u' : Rˣ), (Ideal.Quotient.mk (Ideal.span {b})) ↑u' = ↑ū

        If R is LG, every unit of R ⧸ (b) lifts to a unit of R.

        Given ū ∈ (R ⧸ (b))ˣ, lift it (non-canonically) to u, v : R with u ≡ ū, v ≡ ū⁻¹, so that uv = 1 + bw for some w. The polynomial u + b·T represents a unit over every residue field R ⧸ 𝔪: if b ↦ 0, then u ↦ a unit already (from uv = 1 + bw reducing to uv = 1), so T = 0 works; if b ↦ something nonzero, T = (1 - u)/b gives u + bT ↦ 1. By the LG axiom this descends to R itself: some u + bt₀ ∈ Rˣ, and it is ≡ u ≡ ū mod (b).