Documentation

Mathlib.RingTheory.LocalRing.ResidueField.Basic

Residue Field of local rings #

We prove basic properties of the residue field of a local ring.

source
theorem IsLocalRing.ker_residue {R : Type u_1} [CommRing R] [IsLocalRing R] :
RingHom.ker (residue R) = maximalIdeal R
source
@[simp]
theorem IsLocalRing.residue_eq_zero_iff {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) :
(residue R) x = 0 ↔ x ∈ maximalIdeal R
source
theorem IsLocalRing.residue_ne_zero_iff_isUnit {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) :
(residue R) x ≠ 0 ↔ IsUnit x
source
theorem IsLocalRing.residue_surjective {R : Type u_1} [CommRing R] [IsLocalRing R] :
Function.Surjective ⇑(residue R)
source
instance IsLocalRing.ResidueField.algebra (R : Type u_1) [CommRing R] [IsLocalRing R] {R₀ : Type u_4} [CommRing R₀] [Algebra R₀ R] :
Algebra R₀ (ResidueField R)
Equations
source
instance IsLocalRing.instIsScalarTowerResidueField (R : Type u_1) [CommRing R] [IsLocalRing R] {R₁ : Type u_4} {R₂ : Type u_5} [CommRing R₁] [CommRing R₂] [Algebra R₁ R₂] [Algebra R₁ R] [Algebra R₂ R] [IsScalarTower R₁ R₂ R] :
IsScalarTower R₁ R₂ (ResidueField R)
source
@[simp]
theorem IsLocalRing.ResidueField.algebraMap_eq (R : Type u_1) [CommRing R] [IsLocalRing R] :
algebraMap R (ResidueField R) = residue R
source
instance IsLocalRing.instIsLocalHomResidueFieldRingHomResidue (R : Type u_1) [CommRing R] [IsLocalRing R] :
IsLocalHom (residue R)
source
def IsLocalRing.ResidueField.lift {R : Type u_4} {S : Type u_5} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] :
ResidueField R →+* S

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

Equations
source
theorem IsLocalRing.ResidueField.lift_comp_residue {R : Type u_4} {S : Type u_5} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] :
(lift f).comp (residue R) = f
source
@[simp]
theorem IsLocalRing.ResidueField.lift_residue_apply {R : Type u_4} {S : Type u_5} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] (x : R) :
(lift f) ((residue R) x) = f x
source
def IsLocalRing.ResidueField.map {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
ResidueField R →+* ResidueField S

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

Equations
source
@[simp]
theorem IsLocalRing.ResidueField.map_id {R : Type u_1} [CommRing R] [IsLocalRing R] :
map (RingHom.id R) = RingHom.id (ResidueField R)

Applying IsLocalRing.ResidueField.map to the identity ring homomorphism gives the identity ring homomorphism.

source
theorem IsLocalRing.ResidueField.map_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] (f : T →+* R) (g : R →+* S) [IsLocalHom f] [IsLocalHom g] :
map (g.comp f) = (map g).comp (map f)

The composite of two IsLocalRing.ResidueField.maps is the IsLocalRing.ResidueField.map of the composite.

source
theorem IsLocalRing.ResidueField.map_comp_residue {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
(map f).comp (residue R) = (residue S).comp f
source
theorem IsLocalRing.ResidueField.map_residue {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] (r : R) :
(map f) ((residue R) r) = (residue S) (f r)
source
theorem IsLocalRing.ResidueField.map_id_apply {R : Type u_1} [CommRing R] [IsLocalRing R] (x : ResidueField R) :
(map (RingHom.id R)) x = x
source
@[simp]
theorem IsLocalRing.ResidueField.map_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] (f : R →+* S) (g : S →+* T) (x : ResidueField R) [IsLocalHom f] [IsLocalHom g] :
(map g) ((map f) x) = (map (g.comp f)) x
source
def IsLocalRing.ResidueField.mapEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R ≃+* S) :
ResidueField R ≃+* ResidueField S

A ring isomorphism defines an isomorphism of residue fields.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem IsLocalRing.ResidueField.mapEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R ≃+* S) (a : ResidueField R) :
(mapEquiv f) a = (map ↑f) a
source
@[simp]
theorem IsLocalRing.ResidueField.mapEquiv.symm {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R ≃+* S) :
(mapEquiv f).symm = mapEquiv f.symm
source
@[simp]
theorem IsLocalRing.ResidueField.mapEquiv_trans {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] (e₁ : R ≃+* S) (e₂ : S ≃+* T) :
mapEquiv (e₁.trans e₂) = (mapEquiv e₁).trans (mapEquiv e₂)
source
@[simp]
theorem IsLocalRing.ResidueField.mapEquiv_refl {R : Type u_1} [CommRing R] [IsLocalRing R] :
mapEquiv (RingEquiv.refl R) = RingEquiv.refl (ResidueField R)
source
def IsLocalRing.ResidueField.mapAut {R : Type u_1} [CommRing R] [IsLocalRing R] :
RingAut R →* RingAut (ResidueField R)

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

Equations
source
@[simp]
theorem IsLocalRing.ResidueField.mapAut_apply {R : Type u_1} [CommRing R] [IsLocalRing R] (f : R ≃+* R) :
mapAut f = mapEquiv f
source
instance IsLocalRing.ResidueField.instMulSemiringAction {R : Type u_1} [CommRing R] [IsLocalRing R] (G : Type u_4) [Group G] [MulSemiringAction G R] :
MulSemiringAction G (ResidueField R)

If G acts on R as a MulSemiringAction, then it also acts on IsLocalRing.ResidueField R.

Equations
source
@[simp]
theorem IsLocalRing.ResidueField.residue_smul {R : Type u_1} [CommRing R] [IsLocalRing R] (G : Type u_4) [Group G] [MulSemiringAction G R] (g : G) (r : R) :
(residue R) (g • r) = g • (residue R) r
source
noncomputable instance IsLocalRing.ResidueField.instAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] :
Algebra (ResidueField R) (ResidueField S)
Equations
source
instance IsLocalRing.ResidueField.instIsScalarTower {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] :
IsScalarTower R (ResidueField R) (ResidueField S)
source
instance IsLocalRing.ResidueField.finiteDimensional_of_noetherian {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherian R S] :
FiniteDimensional (ResidueField R) (ResidueField S)
source
theorem IsLocalRing.ResidueField.finite_of_finite {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherian R S] (hfin : Finite (ResidueField R)) :
Finite (ResidueField S)
source
theorem IsLocalRing.isLocalHom_residue {R : Type u_1} [CommRing R] [IsLocalRing R] :
IsLocalHom (residue R)
source
@[deprecated IsLocalRing.isLocalHom_residue (since := "2024-10-10")]
theorem IsLocalRing.isLocalRingHom_residue {R : Type u_1} [CommRing R] [IsLocalRing R] :
IsLocalHom (residue R)

Alias of IsLocalRing.isLocalHom_residue.

source
@[deprecated IsLocalRing.ker_residue (since := "2024-11-11")]
theorem LocalRing.ker_residue {R : Type u_1} [CommRing R] [IsLocalRing R] :
RingHom.ker (IsLocalRing.residue R) = IsLocalRing.maximalIdeal R

Alias of IsLocalRing.ker_residue.

source
@[deprecated IsLocalRing.residue_eq_zero_iff (since := "2024-11-11")]
theorem LocalRing.residue_eq_zero_iff {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) :
(IsLocalRing.residue R) x = 0 ↔ x ∈ IsLocalRing.maximalIdeal R

Alias of IsLocalRing.residue_eq_zero_iff.

source
@[deprecated IsLocalRing.residue_ne_zero_iff_isUnit (since := "2024-11-11")]
theorem LocalRing.residue_ne_zero_iff_isUnit {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) :
(IsLocalRing.residue R) x ≠ 0 ↔ IsUnit x

Alias of IsLocalRing.residue_ne_zero_iff_isUnit.

source
@[deprecated IsLocalRing.residue_surjective (since := "2024-11-11")]
theorem LocalRing.residue_surjective {R : Type u_1} [CommRing R] [IsLocalRing R] :
Function.Surjective ⇑(IsLocalRing.residue R)

Alias of IsLocalRing.residue_surjective.

source
@[deprecated IsLocalRing.ResidueField.algebraMap_eq (since := "2024-11-11")]
theorem LocalRing.ResidueField.algebraMap_eq (R : Type u_1) [CommRing R] [IsLocalRing R] :
algebraMap R (IsLocalRing.ResidueField R) = IsLocalRing.residue R

Alias of IsLocalRing.ResidueField.algebraMap_eq.

source
@[deprecated IsLocalRing.ResidueField.lift (since := "2024-11-11")]
def LocalRing.ResidueField.lift {R : Type u_4} {S : Type u_5} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] :
IsLocalRing.ResidueField R →+* S

Alias of IsLocalRing.ResidueField.lift.

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

Equations
source
@[deprecated IsLocalRing.ResidueField.lift_comp_residue (since := "2024-11-11")]
theorem LocalRing.ResidueField.lift_comp_residue {R : Type u_4} {S : Type u_5} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] :
(IsLocalRing.ResidueField.lift f).comp (IsLocalRing.residue R) = f

Alias of IsLocalRing.ResidueField.lift_comp_residue.

source
@[deprecated IsLocalRing.ResidueField.lift_residue_apply (since := "2024-11-11")]
theorem LocalRing.ResidueField.lift_residue_apply {R : Type u_4} {S : Type u_5} [CommRing R] [IsLocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] (x : R) :
(IsLocalRing.ResidueField.lift f) ((IsLocalRing.residue R) x) = f x

Alias of IsLocalRing.ResidueField.lift_residue_apply.

source
@[deprecated IsLocalRing.ResidueField.map (since := "2024-11-11")]
def LocalRing.ResidueField.map {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
IsLocalRing.ResidueField R →+* IsLocalRing.ResidueField S

Alias of IsLocalRing.ResidueField.map.

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

Equations
source
@[deprecated IsLocalRing.ResidueField.map_id (since := "2024-11-11")]
theorem LocalRing.ResidueField.map_id {R : Type u_1} [CommRing R] [IsLocalRing R] :
IsLocalRing.ResidueField.map (RingHom.id R) = RingHom.id (IsLocalRing.ResidueField R)

Alias of IsLocalRing.ResidueField.map_id.

Applying IsLocalRing.ResidueField.map to the identity ring homomorphism gives the identity ring homomorphism.

source
@[deprecated IsLocalRing.ResidueField.map_comp (since := "2024-11-11")]
theorem LocalRing.ResidueField.map_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] (f : T →+* R) (g : R →+* S) [IsLocalHom f] [IsLocalHom g] :
IsLocalRing.ResidueField.map (g.comp f) = (IsLocalRing.ResidueField.map g).comp (IsLocalRing.ResidueField.map f)

Alias of IsLocalRing.ResidueField.map_comp.

The composite of two IsLocalRing.ResidueField.maps is the IsLocalRing.ResidueField.map of the composite.

source
@[deprecated IsLocalRing.ResidueField.map_comp_residue (since := "2024-11-11")]
theorem LocalRing.ResidueField.map_comp_residue {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
(IsLocalRing.ResidueField.map f).comp (IsLocalRing.residue R) = (IsLocalRing.residue S).comp f

Alias of IsLocalRing.ResidueField.map_comp_residue.

source
@[deprecated IsLocalRing.ResidueField.map_residue (since := "2024-11-11")]
theorem LocalRing.ResidueField.map_residue {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] (r : R) :
(IsLocalRing.ResidueField.map f) ((IsLocalRing.residue R) r) = (IsLocalRing.residue S) (f r)

Alias of IsLocalRing.ResidueField.map_residue.

source
@[deprecated IsLocalRing.ResidueField.map_id_apply (since := "2024-11-11")]
theorem LocalRing.ResidueField.map_id_apply {R : Type u_1} [CommRing R] [IsLocalRing R] (x : IsLocalRing.ResidueField R) :
(IsLocalRing.ResidueField.map (RingHom.id R)) x = x

Alias of IsLocalRing.ResidueField.map_id_apply.

source
@[deprecated IsLocalRing.ResidueField.map_map (since := "2024-11-11")]
theorem LocalRing.ResidueField.map_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] (f : R →+* S) (g : S →+* T) (x : IsLocalRing.ResidueField R) [IsLocalHom f] [IsLocalHom g] :
(IsLocalRing.ResidueField.map g) ((IsLocalRing.ResidueField.map f) x) = (IsLocalRing.ResidueField.map (g.comp f)) x

Alias of IsLocalRing.ResidueField.map_map.

source
@[deprecated IsLocalRing.ResidueField.mapEquiv (since := "2024-11-11")]
def LocalRing.ResidueField.mapEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R ≃+* S) :
IsLocalRing.ResidueField R ≃+* IsLocalRing.ResidueField S

Alias of IsLocalRing.ResidueField.mapEquiv.

A ring isomorphism defines an isomorphism of residue fields.

Equations
source
@[deprecated IsLocalRing.ResidueField.mapEquiv.symm (since := "2024-11-11")]
theorem LocalRing.ResidueField.mapEquiv.symm {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] (f : R ≃+* S) :
(IsLocalRing.ResidueField.mapEquiv f).symm = IsLocalRing.ResidueField.mapEquiv f.symm

Alias of IsLocalRing.ResidueField.mapEquiv.symm.

source
@[deprecated IsLocalRing.ResidueField.mapEquiv_trans (since := "2024-11-11")]
theorem LocalRing.ResidueField.mapEquiv_trans {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] (e₁ : R ≃+* S) (e₂ : S ≃+* T) :
IsLocalRing.ResidueField.mapEquiv (e₁.trans e₂) = (IsLocalRing.ResidueField.mapEquiv e₁).trans (IsLocalRing.ResidueField.mapEquiv e₂)

Alias of IsLocalRing.ResidueField.mapEquiv_trans.

source
@[deprecated IsLocalRing.ResidueField.mapEquiv_refl (since := "2024-11-11")]
theorem LocalRing.ResidueField.mapEquiv_refl {R : Type u_1} [CommRing R] [IsLocalRing R] :
IsLocalRing.ResidueField.mapEquiv (RingEquiv.refl R) = RingEquiv.refl (IsLocalRing.ResidueField R)

Alias of IsLocalRing.ResidueField.mapEquiv_refl.

source
@[deprecated IsLocalRing.ResidueField.mapAut (since := "2024-11-11")]
def LocalRing.ResidueField.mapAut {R : Type u_1} [CommRing R] [IsLocalRing R] :
RingAut R →* RingAut (IsLocalRing.ResidueField R)

Alias of IsLocalRing.ResidueField.mapAut.

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

Equations
source
@[deprecated IsLocalRing.ResidueField.residue_smul (since := "2024-11-11")]
theorem LocalRing.ResidueField.residue_smul {R : Type u_1} [CommRing R] [IsLocalRing R] (G : Type u_4) [Group G] [MulSemiringAction G R] (g : G) (r : R) :
(IsLocalRing.residue R) (g • r) = g • (IsLocalRing.residue R) r

Alias of IsLocalRing.ResidueField.residue_smul.

source
@[deprecated IsLocalRing.ResidueField.finite_of_finite (since := "2024-11-11")]
theorem LocalRing.ResidueField.finite_of_finite {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherian R S] (hfin : Finite (IsLocalRing.ResidueField R)) :
Finite (IsLocalRing.ResidueField S)

Alias of IsLocalRing.ResidueField.finite_of_finite.