Local rings

We prove basic properties of local rings.

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

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

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

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

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

def IsLocalRing.nonunitsAddSubmonoid (R : Type u_1) [Semiring R] [IsLocalRing R] : AddSubmonoid R

The nonunits of a local semiring form an additive submonoid.

Equations

• IsLocalRing.nonunitsAddSubmonoid R = { carrier := nonunits R, add_mem' := ⋯, zero_mem' := ⋯ }

theorem IsLocalRing.exists_of_isUnit_sum {R : Type u_1} [Semiring R] [IsLocalRing R] {ι : Type u_3} {s : Finset ι} {f : ι → R} (h : IsUnit (∑ i ∈ s, f i)) : ∃ i ∈ s, IsUnit (f i)

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

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

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

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

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

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

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

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

@[instance 100]

instance Field.instIsLocalRing (K : Type u_3) [Field K] : IsLocalRing K