Residue Field of local rings

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

theorem IsLocalRing.residue_def {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) : (residue R) x = (Ideal.Quotient.mk (maximalIdeal R)) x

theorem IsLocalRing.ker_residue {R : Type u_1} [CommRing R] [IsLocalRing R] : RingHom.ker (residue R) = maximalIdeal R

@[simp]

theorem IsLocalRing.residue_eq_zero_iff {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) : (residue R) x = 0 ↔ x ∈ maximalIdeal R

theorem IsLocalRing.residue_ne_zero_iff_isUnit {R : Type u_1} [CommRing R] [IsLocalRing R] (x : R) : (residue R) x ≠ 0 ↔ IsUnit x

theorem IsLocalRing.residue_surjective {R : Type u_1} [CommRing R] [IsLocalRing R] : Function.Surjective ⇑(residue R)

@[implicit_reducible]

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

• IsLocalRing.ResidueField.algebra R = { smul := IsLocalRing.ResidueField.algebra._aux_1 R, algebraMap := IsLocalRing.ResidueField.algebra._aux_3 R, commutes' := ⋯, smul_def' := ⋯ }

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)

@[simp]

theorem IsLocalRing.ResidueField.algebraMap_eq (R : Type u_1) [CommRing R] [IsLocalRing R] : algebraMap R (ResidueField R) = residue R

instance IsLocalRing.instIsLocalHomResidueFieldRingHomResidue (R : Type u_1) [CommRing R] [IsLocalRing R] : IsLocalHom (residue R)

@[implicit_reducible]

noncomputable instance IsLocalRing.instModuleResidueFieldOfAlgebra (R : Type u_1) [CommRing R] [IsLocalRing R] {R₀ : Type u_4} [CommRing R₀] [Algebra R₀ R] : Module R₀ (ResidueField R)

Equations

• IsLocalRing.instModuleResidueFieldOfAlgebra R = { toDistribMulAction := Algebra.toModule.toDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance IsLocalRing.instFiniteResidueField (R : Type u_1) [CommRing R] [IsLocalRing R] {R₀ : Type u_4} [CommRing R₀] [Algebra R₀ R] [Module.Finite R₀ R] : Module.Finite R₀ (ResidueField R)

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

• IsLocalRing.ResidueField.lift f = Ideal.Quotient.lift (IsLocalRing.maximalIdeal R) f ⋯

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

@[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

noncomputable 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

• IsLocalRing.ResidueField.map f = Ideal.Quotient.lift (IsLocalRing.maximalIdeal R) ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal S)).comp f) ⋯

@[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.

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.

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

@[simp]

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)

theorem IsLocalRing.ResidueField.map_id_apply {R : Type u_1} [CommRing R] [IsLocalRing R] (x : ResidueField R) : (map (RingHom.id R)) x = x

@[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

noncomputable 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.

@[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

@[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

@[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₂)

@[simp]

theorem IsLocalRing.ResidueField.mapEquiv_refl {R : Type u_1} [CommRing R] [IsLocalRing R] : mapEquiv (RingEquiv.refl R) = RingEquiv.refl (ResidueField R)

noncomputable 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

• IsLocalRing.ResidueField.mapAut = { toFun := IsLocalRing.ResidueField.mapEquiv, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem IsLocalRing.ResidueField.mapAut_apply {R : Type u_1} [CommRing R] [IsLocalRing R] (f : R ≃+* R) : mapAut f = mapEquiv f

@[implicit_reducible]

noncomputable 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

• IsLocalRing.ResidueField.instMulSemiringAction G = MulSemiringAction.compHom (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField.mapAut.comp (MulSemiringAction.toRingAut G R))

@[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

instance IsLocalRing.ResidueField.instLiesOverMaximalIdeal {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] : (maximalIdeal S).LiesOver (maximalIdeal R)

@[implicit_reducible]

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

• IsLocalRing.ResidueField.instAlgebra = Ideal.Quotient.algebraOfLiesOver (IsLocalRing.maximalIdeal S) (IsLocalRing.maximalIdeal R)

@[simp]

theorem IsLocalRing.ResidueField.algebraMap_residue {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] (x : R) : (algebraMap (ResidueField R) (ResidueField S)) ((residue R) x) = (residue S) ((algebraMap R S) x)

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)] {R₀ : Type u_4} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] : IsScalarTower R₀ (ResidueField R) (ResidueField S)

instance IsLocalRing.ResidueField.instIsScalarTower_1 {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] {R₀ : Type u_4} [CommRing R₀] [Algebra R₀ R] [Algebra R₀ S] [IsScalarTower R₀ R S] [IsLocalRing R₀] [IsLocalHom (algebraMap R₀ R)] [IsLocalHom (algebraMap R₀ S)] : IsScalarTower (ResidueField R₀) (ResidueField R) (ResidueField S)

@[implicit_reducible]

noncomputable instance IsLocalRing.ResidueField.instModule {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] : Module (ResidueField R) (ResidueField S)

Equations

• IsLocalRing.ResidueField.instModule = { toDistribMulAction := Algebra.toModule.toDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance IsLocalRing.ResidueField.finite_of_module_finite {R : Type u_1} {S : Type u_2} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Finite R S] : Module.Finite (ResidueField R) (ResidueField S)

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)] [Module.Finite R S] (hfin : Finite (ResidueField R)) : Finite (ResidueField S)

noncomputable def IsLocalRing.ResidueField.mapAlgHom {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] (e : S →ₐ[R] T) [IsLocalHom e] : ResidueField S →ₐ[R] ResidueField T

A local algebra homomorphism induces an algebra homomorphism on the residue fields.

See mapAlgHom' for a variant where the base ring R is also quotiented.

Equations

• IsLocalRing.ResidueField.mapAlgHom e = { toRingHom := IsLocalRing.ResidueField.map ↑e, commutes' := ⋯ }

@[simp]

theorem IsLocalRing.ResidueField.mapAlgHom_residue {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : (mapAlgHom e) ((residue S) x) = (residue T) (e x)

noncomputable def IsLocalRing.ResidueField.mapAlgEquiv {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] (e : S ≃ₐ[R] T) : ResidueField S ≃ₐ[R] ResidueField T

A local algebra isomorphism induces an algebra isomorphism on the residue fields.

See mapAlgEquiv' for a variant where the base ring R is also quotiented.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsLocalRing.ResidueField.mapAlgEquiv_residue {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] (e : S ≃ₐ[R] T) (x : S) : (mapAlgEquiv e) ((residue S) x) = (residue T) (e x)

noncomputable def IsLocalRing.ResidueField.mapAlgHom' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] (e : S →ₐ[R] T) [IsLocalHom e] : ResidueField S →ₐ[ResidueField R] ResidueField T

A local algebra homomorphism induces an algebra homomorphism on the residue fields.

See mapAlgHom for a variant where the base ring R is not quotiented.

Equations

• IsLocalRing.ResidueField.mapAlgHom' e = AlgHom.extendScalarsOfSurjective ⋯ (IsLocalRing.ResidueField.mapAlgHom e)

@[simp]

theorem IsLocalRing.ResidueField.mapAlgHom'_residue {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] [IsLocalRing R] (e : S →ₐ[R] T) [IsLocalHom e] (x : S) : (mapAlgHom' e) ((residue S) x) = (residue T) (e x)

noncomputable def IsLocalRing.ResidueField.mapAlgEquiv' {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] (e : S ≃ₐ[R] T) : ResidueField S ≃ₐ[ResidueField R] ResidueField T

A local algebra isomorphism induces an algebra isomorphism on the residue fields.

See mapAlgEquiv for a variant where the base ring R is not quotiented.

Equations

• IsLocalRing.ResidueField.mapAlgEquiv' e = AlgEquiv.extendScalarsOfSurjective ⋯ (IsLocalRing.ResidueField.mapAlgEquiv e)

@[simp]

theorem IsLocalRing.ResidueField.mapAlgEquiv'_residue {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [CommRing S] [IsLocalRing S] [CommRing T] [IsLocalRing T] [Algebra R S] [Algebra R T] [IsLocalHom (algebraMap R S)] [IsLocalHom (algebraMap R T)] [IsLocalRing R] (e : S ≃ₐ[R] T) (x : S) : (mapAlgEquiv' e) ((residue S) x) = (residue T) (e x)