Local rings

Define local rings as commutative rings having a unique maximal ideal.

Main definitions

• LocalRing: A predicate on semirings, stating that for any pair of elements that adds up to 1, one of them is a unit. In the commutative case this is shown to be equivalent to the condition that there exists a unique maximal ideal, see LocalRing.of_unique_max_ideal and LocalRing.maximal_ideal_unique.

class LocalRing (R : Type u_1) [Semiring R] extends Nontrivial : Prop

A semiring is local if it is nontrivial and a or b is a unit whenever a + b = 1. Note that LocalRing is a predicate.

• of_is_unit_or_is_unit_of_add_one :: (
• exists_pair_ne : ∃ (x : R), ∃ (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one : ∀ {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b

  in a local ring R, if a + b = 1, then either a is a unit or b is a unit. In another word, for every a : R, either a is a unit or 1 - a is a unit.

• )

theorem LocalRing.isUnit_or_isUnit_of_add_one {R : Type u_1} : ∀ {inst : Semiring R} [self : LocalRing R] {a b : R}, a + b = 1 → IsUnit a ∨ IsUnit b

in a local ring R, if a + b = 1, then either a is a unit or b is a unit. In another word, for every a : R, either a is a unit or 1 - a is a unit.