mathlibdocumentation

ring_theory.ideal.local_ring

Local rings #

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

Main definitions #

• local_ring: A predicate on commutative rings, stating that every element a is either a unit or 1 - a is a unit. This is shown to be equivalent to the condition that there exists a unique maximal ideal.
• local_ring.maximal_ideal: The unique maximal ideal for a local rings. Its carrier set is the set of non units.
• is_local_ring_hom: A predicate on semiring homomorphisms, requiring that it maps nonunits to nonunits. For local rings, this means that the image of the unique maximal ideal is again contained in the unique maximal ideal.
• local_ring.residue_field: The quotient of a local ring by its maximal ideal.
@[class]
structure local_ring (R : Type u) [comm_ring R] :
Prop
• to_nontrivial :
• is_local : ∀ (a : R), is_unit (1 - a)

A commutative ring is local if it has a unique maximal ideal. Note that local_ring is a predicate.

Instances
theorem local_ring.is_unit_or_is_unit_one_sub_self {R : Type u} [comm_ring R] [local_ring R] (a : R) :
is_unit (1 - a)
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 ) :
theorem local_ring.is_unit_one_sub_self_of_mem_nonunits {R : Type u} [comm_ring R] [local_ring R] (a : R) (h : a ) :
is_unit (1 - a)
theorem local_ring.nonunits_add {R : Type u} [comm_ring R] [local_ring R] {x y : R} (hx : x ) (hy : y ) :
x + y
def local_ring.maximal_ideal (R : Type u) [comm_ring R] [local_ring R] :

The ideal of elements that are not units.

Equations
@[protected, instance]
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 ) :
@[simp]
theorem local_ring.mem_maximal_ideal {R : Type u} [comm_ring R] [local_ring R] (x : R) :
x
theorem local_of_nonunits_ideal {R : Type u} [comm_ring R] (hnze : 0 1) (h : ∀ (x : R), x ∀ (y : R), y x + y ) :
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) :
@[class]
structure is_local_ring_hom {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) :
Prop

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.

Instances
@[protected, instance]
def is_local_ring_hom_id (R : Type u_1) [semiring R] :
@[simp]
theorem is_unit_map_iff {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (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)  :
@[protected, instance]
def CommRing.is_local_ring_hom_comp {R S T : CommRing} (f : R S) (g : S T)  :
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)  :

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) :
@[simp]
theorem is_unit_of_map_unit {R : Type u} {S : Type v} [semiring R] [semiring S] (f : R →+* S) (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_iso {R S : CommRing} (f : R S) :
@[protected, instance]
def is_local_ring_hom_of_is_iso {R S : CommRing} (f : R S)  :
theorem map_nonunit {R : Type u} {S : Type v} [comm_ring R] [local_ring R] [comm_ring S] [local_ring S] (f : R →+* S) (a : R) (h : a ) :
theorem local_ring.local_hom_tfae {R : Type u} {S : Type v} [comm_ring R] [local_ring R] [comm_ring S] [local_ring S] (f : R →+* S) :

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. https://stacks.math.columbia.edu/tag/07BJ

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
@[protected, instance]
noncomputable def local_ring.residue_field.field (R : Type u) [comm_ring R] [local_ring R] :
Equations
@[protected, instance]
noncomputable def local_ring.residue_field.inhabited (R : Type u) [comm_ring R] [local_ring R] :
Equations
def local_ring.residue (R : Type u) [comm_ring R] [local_ring R] :

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

Equations
@[protected, instance]
noncomputable def local_ring.residue_field.algebra (R : Type u) [comm_ring R] [local_ring R] :
Equations
noncomputable def local_ring.residue_field.map {R : Type u} {S : Type v} [comm_ring R] [local_ring R] [comm_ring S] [local_ring S] (f : R →+* S)  :

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

Equations
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] :