Documentation

Mathlib.RingTheory.LocalRing.NonLocalRing

Non-local rings #

This file gathers some results about non-local rings.

Main results #

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

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.