mathlib3 documentation

ring_theory.ideal.local_ring

Local rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definitions #

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

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

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

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.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)] :
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.

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

If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.

@[protected, instance]

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

Equations
Instances for local_ring.residue

A local ring homomorphism into a field can be descended onto the residue field.

Equations

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

Equations
@[simp]

Applying residue_field.map to the identity ring homomorphism gives the identity ring homomorphism.

The composite of two residue_field.maps is the residue_field.map of the composite.

The group homomorphism from ring_aut R to ring_aut k where k is the residue field of R.

Equations
@[simp]
theorem local_ring.residue_field.residue_smul {R : Type u} [comm_ring R] [local_ring R] (G : Type u_1) [group G] [mul_semiring_action G R] (g : G) (r : R) :
@[protected, instance]
def field.local_ring (K : Type u') [field K] :
@[protected, reducible]
theorem ring_equiv.local_ring {A : Type u_1} {B : Type u_2} [comm_semiring A] [local_ring A] [comm_semiring B] (e : A ≃+* B) :