Non-local rings

This file gathers some results about non-local rings.

Main results

• not_isLocalRing_of_nontrivial_pi: for an index type ι with at least two elements and an indexed family of (semi)rings R : ι → Type*, the indexed product (semi)ring Π i, R i is not local.
• not_isLocalRing_of_prod_of_nontrivial: the product of two nontrivial (semi)rings is not local.
• not_isLocalRing_tfae: the following conditions are equivalent for a commutative (semi)ring R:
  • R is not local,
  • the maximal spectrum of R is nontrivial,
  • R has two distinct maximal ideals.
• exists_surjective_of_not_isLocalRing: there exists a surjective ring homomorphism from a non-local commutative ring onto a product of two fields.

theorem IsLocalRing.not_isLocalRing_def {R : Type u_1} [Semiring R] {a b : R} (ha : ¬IsUnit a) (hb : ¬IsUnit b) (hab : a + b = 1) : ¬IsLocalRing R

If two non-units sum to 1 in a (semi)ring R then R is not local.

theorem IsLocalRing.not_isLocalRing_of_nontrivial_pi {ι : Type u_1} [Nontrivial ι] (R : ι → Type u_2) [(i : ι) → Semiring (R i)] [∀ (i : ι), Nontrivial (R i)] : ¬IsLocalRing ((i : ι) → R i)

For an index type ι with at least two elements and an indexed family of (semi)rings R : ι → Type*, the indexed product (semi)ring Π i, R i is not local.

theorem IsLocalRing.not_isLocalRing_of_prod_of_nontrivial (R₁ : Type u_1) (R₂ : Type u_2) [Semiring R₁] [Semiring R₂] [Nontrivial R₁] [Nontrivial R₂] : ¬IsLocalRing (R₁ × R₂)

The product of two nontrivial (semi)rings is not local.

theorem IsLocalRing.not_isLocalRing_tfae {R : Type u_1} [CommSemiring R] [Nontrivial R] : [¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE

The following conditions are equivalent for a commutative (semi)ring R:

• R is not local,
• the maximal spectrum of R is nontrivial,
• R has two distinct maximal ideals.

theorem IsLocalRing.exists_surjective_of_not_isLocalRing {R : Type u} [CommRing R] [Nontrivial R] (h : ¬IsLocalRing R) : ∃ (K₁ : Type u) (K₂ : Type u) (x : Field K₁) (x_1 : Field K₂) (f : R →+* K₁ × K₂), Function.Surjective ⇑f

There exists a surjective ring homomorphism from a non-local commutative ring onto a product of two fields.