Local rings

We prove basic properties of local rings.

theorem LocalRing.of_isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), IsUnit (a + b) → IsUnit a ∨ IsUnit b) : LocalRing R

theorem LocalRing.of_nonunits_add {R : Type u_1} [CommSemiring R] [Nontrivial R] (h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) : LocalRing R

A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.

theorem LocalRing.of_unique_max_ideal {R : Type u_1} [CommSemiring R] (h : ∃! I : Ideal R, I.IsMaximal) : LocalRing R

A semiring is local if it has a unique maximal ideal.

theorem LocalRing.of_unique_nonzero_prime {R : Type u_1} [CommSemiring R] (h : ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime) : LocalRing R

theorem LocalRing.isUnit_or_isUnit_of_isUnit_add {R : Type u_1} [CommSemiring R] [LocalRing R] {a : R} {b : R} (h : IsUnit (a + b)) : IsUnit a ∨ IsUnit b

theorem LocalRing.nonunits_add {R : Type u_1} [CommSemiring R] [LocalRing R] {a : R} {b : R} (ha : a ∈ nonunits R) (hb : b ∈ nonunits R) : a + b ∈ nonunits R

theorem LocalRing.of_isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [Nontrivial R] (h : ∀ (a : R), IsUnit a ∨ IsUnit (1 - a)) : LocalRing R

theorem LocalRing.isUnit_or_isUnit_one_sub_self {R : Type u_1} [CommRing R] [LocalRing R] (a : R) : IsUnit a ∨ IsUnit (1 - a)

theorem LocalRing.isUnit_of_mem_nonunits_one_sub_self {R : Type u_1} [CommRing R] [LocalRing R] (a : R) (h : 1 - a ∈ nonunits R) : IsUnit a

theorem LocalRing.isUnit_one_sub_self_of_mem_nonunits {R : Type u_1} [CommRing R] [LocalRing R] (a : R) (h : a ∈ nonunits R) : IsUnit (1 - a)

theorem LocalRing.of_surjective' {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [Nontrivial S] (f : R →+* S) (hf : Function.Surjective ⇑f) : LocalRing S

@[instance 100]

instance Field.instLocalRing (K : Type u_3) [Field K] : LocalRing K

Equations

• ⋯ = ⋯