Documentation

LeanPool.CompositionAlgebrasOverRings.LGRing.Products

Products of LG-rings #

The product half of GPR 11.21 (GN 2.1(a)): R₁ × R₂ is an LG-ring iff R₁ and R₂ both are. The Jacobson-quotient half is in LGRing/Jacobson.lean; the two combine in LGRing/Semilocal.lean to give GPR 11.22.

A second, unrelated result closes the file: an arbitrary product of fields is an LG-ring. That is not a corollary of the binary statement — induction on isLGRing_prod_iff reaches only finite products — and its proof runs through the value-ideal criterion instead.

Main results #

Proof idea #

The maximal ideals of R₁ × R₂ are exactly Ideal.prod 𝔪 ⊤ and Ideal.prod ⊤ 𝔪 for 𝔪 maximal in R₁ resp. R₂ — Ideal.ideal_prod_prime classifies the primes, and maximality transfers both ways along Ideal.comap_isMaximal_of_surjective and Ideal.map_fst_prod — with the corresponding residue fields those of the factors.

For ⇐, given p over R₁ × R₂ representing a unit at every residue field, its images MvPolynomial.map (RingHom.fst _ _) p and map (RingHom.snd _ _) p represent units at every residue field of R₁ resp. R₂; the LG hypotheses give witnesses s₁, s₂, and fun i ↦ (s₁ i, s₂ i) is a witness over R₁ × R₂, because IsUnit in a product is componentwise (Prod.isUnit_iff).

For ⟹, the point is that a polynomial over R₁ must be promoted to one over R₁ × R₂ that carries no information about R₂. There is no ring homomorphism R₁ → R₁ × R₂ to push it through — r ↦ (r, 1) is not additive and r ↦ (r, 0) is not unital — but MvPolynomial.map (RingHom.fst _ _) is surjective, so p₁ has some preimage q, and the orthogonal idempotents of R₁ × R₂ assemble it into

p := C (1, 0) * q + C (0, 1),

for which map fst p = p₁ while map snd p = 1. Then p represents a unit at every residue field of R₁ × R₂: on the R₁ side because p₁ does, and on the R₂ side for free, the constant 1 representing a unit anywhere. The LG hypothesis for R₁ × R₂ yields a witness, whose first components witness p₁ over R₁.

References #

Transport of RepresentsUnit along a square of ring homomorphisms #

source
theorem MvPolynomial.RepresentsUnit.mapOfComm {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 : ℕ} {p : MvPolynomial (Fin n) R} (h : p.RepresentsUnit S) :
((map φ) p).RepresentsUnit S'

Pushing a RepresentsUnit witness forward along a commuting square.

source
theorem MvPolynomial.RepresentsUnit.ofMapOfComm {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'] (e : S ≃+* S') (hcomm : e.toRingHom.comp (algebraMap R S) = (algebraMap R' S').comp φ) {n : ℕ} {p : MvPolynomial (Fin n) R} (h : ((map φ) p).RepresentsUnit S') :
p.RepresentsUnit S

Pulling a RepresentsUnit witness back along a commuting square whose vertical map is an isomorphism. This is the direction that needs ψ invertible: the witness is transported by e.symm and the resulting unit is recognised by applying e.

Maximal ideals and residue fields of a product #

source
theorem Ideal.comap_fst_eq_prod_top {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₁) :
comap (RingHom.fst R₁ R₂) 𝔪 = 𝔪.prod ⊤
source
theorem Ideal.comap_snd_eq_top_prod {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₂) :
comap (RingHom.snd R₁ R₂) 𝔪 = ⊤.prod 𝔪
source
theorem Ideal.prod_top_isMaximal {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₁) [𝔪.IsMaximal] :
(𝔪.prod ⊤).IsMaximal
source
theorem Ideal.top_prod_isMaximal {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₂) [𝔪.IsMaximal] :
(⊤.prod 𝔪).IsMaximal
source
theorem Ideal.isMaximal_of_prod_top_isMaximal {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] {𝔭 : Ideal R₁} (h : (𝔭.prod ⊤).IsMaximal) :
𝔭.IsMaximal
source
theorem Ideal.isMaximal_of_top_prod_isMaximal {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] {𝔭 : Ideal R₂} (h : (⊤.prod 𝔭).IsMaximal) :
𝔭.IsMaximal
source
noncomputable def Ideal.prodQuotientFstEquiv {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₁) :
(R₁ × R₂) ⧸ 𝔪.prod ⊤ ≃+* R₁ ⧸ 𝔪

The residue field of R₁ × R₂ at Ideal.prod 𝔪 ⊤ is the residue field of R₁ at 𝔪: apply the first isomorphism theorem to R₁ × R₂ → R₁ → R₁ ⧸ 𝔪, whose kernel is Ideal.prod 𝔪 ⊤ by Ideal.comap_fst_eq_prod_top.

Equations
Instances For
    source
    @[simp]
    theorem Ideal.prodQuotientFstEquiv_apply {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₁) (x : R₁ × R₂) :
    𝔪.prodQuotientFstEquiv ((Quotient.mk (𝔪.prod ⊤)) x) = (Quotient.mk 𝔪) x.1
    source
    noncomputable def Ideal.prodQuotientSndEquiv {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₂) :
    (R₁ × R₂) ⧸ ⊤.prod 𝔪 ≃+* R₂ ⧸ 𝔪

    The residue field of R₁ × R₂ at Ideal.prod ⊤ 𝔪 is the residue field of R₂ at 𝔪.

    Equations
    Instances For
      source
      @[simp]
      theorem Ideal.prodQuotientSndEquiv_apply {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₂) (x : R₁ × R₂) :
      𝔪.prodQuotientSndEquiv ((Quotient.mk (⊤.prod 𝔪)) x) = (Quotient.mk 𝔪) x.2
      source
      theorem Ideal.prodQuotientFstEquiv_comm {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₁) :
      𝔪.prodQuotientFstEquiv.toRingHom.comp (algebraMap (R₁ × R₂) ((R₁ × R₂) ⧸ 𝔪.prod ⊤)) = (algebraMap R₁ (R₁ ⧸ 𝔪)).comp (RingHom.fst R₁ R₂)
      source
      theorem Ideal.prodQuotientSndEquiv_comm {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] (𝔪 : Ideal R₂) :
      𝔪.prodQuotientSndEquiv.toRingHom.comp (algebraMap (R₁ × R₂) ((R₁ × R₂) ⧸ ⊤.prod 𝔪)) = (algebraMap R₂ (R₂ ⧸ 𝔪)).comp (RingHom.snd R₁ R₂)

      GPR 11.21(ii) #

      source
      theorem isLGRing_prod_iff {R₁ : Type u} [CommRing R₁] {R₂ : Type u} [CommRing R₂] :
      IsLGRing (R₁ × R₂) ↔ IsLGRing R₁ ∧ IsLGRing R₂

      GPR 11.21(ii): a binary product of rings is an LG-ring iff both factors are.

      Arbitrary products of fields #

      source
      theorem isLGRing_pi_of_forall_field {ι : Type v} (K : ι → Type u) [(i : ι) → Field (K i)] :
      IsLGRing ((i : ι) → K i)

      An arbitrary product of fields is an LG-ring (GN 2.2, from EG).

      By the value-ideal criterion it suffices to turn an equation 1 = Σⱼ cⱼ · p(tⱼ) — finitely many points tⱼ of (∏ᵢ Kᵢ)ⁿ whose values at p generate the unit ideal — into a single point where p is a unit. Read that equation off at one index i: the i-th components sum to 1 ≠ 0 in the field Kᵢ, so some j has p(tⱼ)ᵢ ≠ 0. Choosing such a j = j(i) for every i and splicing, s x i := t (j i) x i, gives a point whose value has p(s)ᵢ = p(t (j i))ᵢ ≠ 0 in every coordinate — and a unit in a product is exactly a coordinatewise unit.

      A product of fields is von Neumann regular, so this also follows from IsVonNeumannRegular.isLGRing in LGRing/ZeroDimensional.lean; the direct argument is kept because it is elementary — no idempotents, no value ideal beyond its unwinding — and because it is what makes the shape of the general statement visible.

      The splicing step is legitimate because evaluation commutes with each projection ∏ᵢ Kᵢ → Kᵢ (MvPolynomial.aeval_map_comm): the i-th coordinate of a value depends on the i-th coordinates of the point and on nothing else. This is the whole reason the argument needs the factors to be fields only coordinatewise, with no compatibility between them.

      source
      theorem isLGRing_pi_field (F : Type u) [Field F] (I : Type v) :
      IsLGRing (I → F)

      F^I is an LG-ring for a field F and an arbitrary index set I (GN 2.2, from EG); the constant-family case of isLGRing_pi_of_forall_field.