mathlib documentation


Local rings #

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

Main definitions #

theorem local_ring.is_unit_or_is_unit_one_sub_self {R : Type u} [comm_ring R] [local_ring R] (a : R) :
theorem local_ring.is_unit_of_mem_nonunits_one_sub_self {R : Type u} [comm_ring R] [local_ring R] (a : R) (h : 1 - a nonunits R) :
theorem local_ring.is_unit_one_sub_self_of_mem_nonunits {R : Type u} [comm_ring R] [local_ring R] (a : R) (h : a nonunits R) :
is_unit (1 - a)
theorem local_ring.nonunits_add {R : Type u} [comm_ring R] [local_ring R] {x y : R} (hx : x nonunits R) (hy : y nonunits R) :
x + y nonunits R
def local_ring.maximal_ideal (R : Type u) [comm_ring R] [local_ring R] :

The ideal of elements that are not units.

theorem local_ring.maximal_ideal_unique (R : Type u) [comm_ring R] [local_ring R] :
∃! (I : ideal R), I.is_maximal
theorem local_ring.eq_maximal_ideal {R : Type u} [comm_ring R] [local_ring R] {I : ideal R} (hI : I.is_maximal) :
theorem local_ring.le_maximal_ideal {R : Type u} [comm_ring R] [local_ring R] {J : ideal R} (hJ : J ) :
theorem local_of_nonunits_ideal {R : Type u} [comm_ring R] (hnze : 0 1) (h : ∀ (x y : R), x nonunits Ry nonunits Rx + y nonunits R) :
theorem local_of_unique_max_ideal {R : Type u} [comm_ring R] (h : ∃! (I : ideal R), I.is_maximal) :
theorem local_of_unique_nonzero_prime (R : Type u) [comm_ring R] (h : ∃! (P : ideal R), P P.is_prime) :
theorem local_of_surjective {R : Type u} {S : Type v} [comm_ring R] [local_ring R] [comm_ring S] [nontrivial S] (f : R →+* S) (hf : function.surjective f) :
structure is_local_ring_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :

A local ring homomorphism is a homomorphism between local rings such that the image of the maximal ideal of the source is contained within the maximal ideal of the target.

theorem is_unit_map_iff {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) [is_local_ring_hom f] (a : R) :
def is_local_ring_hom_comp {R : Type u} {S : Type v} {T : Type w} [semiring R] [semiring S] [semiring T] (g : S →+* T) (f : R →+* S) [is_local_ring_hom g] [is_local_ring_hom f] :
def is_local_ring_hom_equiv {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R ≃+* S) :
theorem is_unit_of_map_unit {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) [is_local_ring_hom f] (a : R) (h : is_unit (f a)) :
theorem of_irreducible_map {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) [h : is_local_ring_hom f] {x : R} (hfx : irreducible (f x)) :
theorem map_nonunit {R : Type u} {S : Type v} [comm_ring R] [local_ring R] [comm_ring S] [local_ring S] (f : R →+* S) [is_local_ring_hom f] (a : R) (h : a local_ring.maximal_ideal R) :
def local_ring.residue_field (R : Type u) [comm_ring R] [local_ring R] :
Type u

The residue field of a local ring is the quotient of the ring by its maximal ideal.


The quotient map from a local ring to its residue field.


The map on residue fields induced by a local homomorphism between local rings

theorem local_ring.ker_eq_maximal_ideal {R : Type u} [comm_ring R] [local_ring R] {K : Type u_1} [field K] (φ : R →+* K) (hφ : function.surjective φ) :
def field.local_ring {R : Type u} [field R] :