mathlib documentation

ring_theory.ideal.local_ring

Local rings #

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

Main definitions #

theorem local_ring.of_is_unit_or_is_unit_of_is_unit_add {R : Type u} [comm_semiring R] [nontrivial R] (h : ∀ (a b : R), is_unit (a + b)is_unit a is_unit b) :
theorem local_ring.of_nonunits_add {R : Type u} [comm_semiring R] [nontrivial R] (h : ∀ (a b : R), a nonunits Rb nonunits Ra + b nonunits R) :

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

theorem local_ring.of_unique_max_ideal {R : Type u} [comm_semiring R] (h : ∃! (I : ideal R), I.is_maximal) :

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

theorem local_ring.of_unique_nonzero_prime {R : Type u} [comm_semiring R] (h : ∃! (P : ideal R), P P.is_prime) :
theorem local_ring.is_unit_or_is_unit_of_is_unit_add {R : Type u} [comm_semiring R] [local_ring R] {a b : R} (h : is_unit (a + b)) :
theorem local_ring.nonunits_add {R : Type u} [comm_semiring R] [local_ring R] {a b : R} (ha : a nonunits R) (hb : b nonunits R) :
a + b nonunits R
theorem local_ring.maximal_ideal_unique (R : Type u) [comm_semiring R] [local_ring R] :
∃! (I : ideal R), I.is_maximal
theorem local_ring.le_maximal_ideal {R : Type u} [comm_semiring R] [local_ring R] {J : ideal R} (hJ : J ) :
@[simp]
theorem local_ring.of_is_unit_or_is_unit_one_sub_self {R : Type u} [comm_ring R] [nontrivial R] (h : ∀ (a : R), is_unit a is_unit (1 - a)) :
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.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]
@[simp]
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) :
@[simp]
theorem map_mem_nonunits_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]
def is_local_ring_hom_equiv {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R ≃+* S) :
@[simp]
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 is_local_ring_hom_of_comp {R : Type u} {S : Type v} {T : Type w} [semiring R] [semiring S] [semiring T] (f : R →+* S) (g : S →+* T) [is_local_ring_hom (g.comp f)] :
@[protected, instance]
theorem ring_hom.domain_local_ring {R : Type u_1} {S : Type u_2} [comm_semiring R] [comm_semiring 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.

@[protected, instance]
theorem map_nonunit {R : Type u} {S : Type v} [comm_semiring R] [local_ring R] [comm_semiring S] [local_ring S] (f : R →+* S) [is_local_ring_hom f] (a : R) (h : a local_ring.maximal_ideal R) :

The image of the maximal ideal of the source is contained within the maximal ideal of the target.

theorem local_ring.of_surjective {R : Type u} {S : Type v} [comm_semiring R] [local_ring R] [comm_semiring S] [nontrivial S] (f : R →+* S) [is_local_ring_hom f] (hf : function.surjective f) :
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.

Equations
Instances for local_ring.residue_field
@[protected, instance]
Equations

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

Equations

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

Equations
theorem local_ring.ker_eq_maximal_ideal {R : Type u} {K : Type u'} [comm_ring R] [local_ring R] [field K] (φ : R →+* K) (hφ : function.surjective φ) :
@[protected, instance]
def field.local_ring (K : Type u') [field K] :