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 : R), x nonunits R∀ (y : R), y 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) :
@[protected, instance]
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) :
@[protected, instance]
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] :
@[protected, instance]
theorem ring_hom.domain_local_ring {R : Type u_1} {S : Type u_2} [comm_ring R] [comm_ring S] [H : local_ring S] (f : R →+* S) [is_local_ring_hom f] :

If f : R →+* S is a local ring hom, then R is a local ring if S is.

theorem is_local_ring_hom_of_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [comm_ring R] [comm_ring S] [comm_ring T] (f : R →+* S) (g : S →+* T) [is_local_ring_hom (g.comp f)] :
@[protected, instance]
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)) :
@[protected, instance]
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) :

A ring homomorphism between local rings is a local ring hom iff it reflects units, i.e. any preimage of a unit is still a unit.

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.

@[protected, instance]

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 φ) :
@[protected, instance]
def field.local_ring {R : Type u} [field R] :