Residue Field of local rings #

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

source

theorem LocalRing.ker_residue {R : Type u_1} [CommRing R] [LocalRing R] :

RingHom.ker (LocalRing.residue R) = LocalRing.maximalIdeal R

source

@[simp]

theorem LocalRing.residue_eq_zero_iff {R : Type u_1} [CommRing R] [LocalRing R] (x : R) :

(LocalRing.residue R) x = 0 ↔ x ∈ LocalRing.maximalIdeal R

source

theorem LocalRing.residue_ne_zero_iff_isUnit {R : Type u_1} [CommRing R] [LocalRing R] (x : R) :

(LocalRing.residue R) x ≠ 0 ↔ IsUnit x

source

instance LocalRing.ResidueField.algebra (R : Type u_1) [CommRing R] [LocalRing R] :

Algebra R (LocalRing.ResidueField R)

Equations

LocalRing.ResidueField.algebra R = Ideal.Quotient.algebra R

source

theorem LocalRing.ResidueField.algebraMap_eq (R : Type u_1) [CommRing R] [LocalRing R] :

algebraMap R (LocalRing.ResidueField R) = LocalRing.residue R

source

instance LocalRing.instIsLocalHomResidueFieldRingHomResidue (R : Type u_1) [CommRing R] [LocalRing R] :

IsLocalHom (LocalRing.residue R)

Equations

⋯ = ⋯

source

def LocalRing.ResidueField.lift {R : Type u_4} {S : Type u_5} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] :

LocalRing.ResidueField R →+* S

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

Equations

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

Instances For

source

theorem LocalRing.ResidueField.lift_comp_residue {R : Type u_4} {S : Type u_5} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] :

(LocalRing.ResidueField.lift f).comp (LocalRing.residue R) = f

source

@[simp]

theorem LocalRing.ResidueField.lift_residue_apply {R : Type u_4} {S : Type u_5} [CommRing R] [LocalRing R] [Field S] (f : R →+* S) [IsLocalHom f] (x : R) :

(LocalRing.ResidueField.lift f) ((LocalRing.residue R) x) = f x

source

def LocalRing.ResidueField.map {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalHom f] :

LocalRing.ResidueField R →+* LocalRing.ResidueField S

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

Equations

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

Instances For

source

@[simp]

theorem LocalRing.ResidueField.map_id {R : Type u_1} [CommRing R] [LocalRing R] :

LocalRing.ResidueField.map (RingHom.id R) = RingHom.id (LocalRing.ResidueField R)

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

source

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

LocalRing.ResidueField.map (g.comp f) = (LocalRing.ResidueField.map g).comp (LocalRing.ResidueField.map f)

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

source

theorem LocalRing.ResidueField.map_comp_residue {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalHom f] :

(LocalRing.ResidueField.map f).comp (LocalRing.residue R) = (LocalRing.residue S).comp f

source

theorem LocalRing.ResidueField.map_residue {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R →+* S) [IsLocalHom f] (r : R) :

(LocalRing.ResidueField.map f) ((LocalRing.residue R) r) = (LocalRing.residue S) (f r)

source

theorem LocalRing.ResidueField.map_id_apply {R : Type u_1} [CommRing R] [LocalRing R] (x : LocalRing.ResidueField R) :

(LocalRing.ResidueField.map (RingHom.id R)) x = x

source

@[simp]

theorem LocalRing.ResidueField.map_map {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing T] [LocalRing T] (f : R →+* S) (g : S →+* T) (x : LocalRing.ResidueField R) [IsLocalHom f] [IsLocalHom g] :

(LocalRing.ResidueField.map g) ((LocalRing.ResidueField.map f) x) = (LocalRing.ResidueField.map (g.comp f)) x

source

def LocalRing.ResidueField.mapEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R ≃+* S) :

LocalRing.ResidueField R ≃+* LocalRing.ResidueField S

A ring isomorphism defines an isomorphism of residue fields.

Equations

LocalRing.ResidueField.mapEquiv f = { toFun := ⇑(LocalRing.ResidueField.map ↑f), invFun := ⇑(LocalRing.ResidueField.map ↑f.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem LocalRing.ResidueField.mapEquiv_apply {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R ≃+* S) (a : LocalRing.ResidueField R) :

(LocalRing.ResidueField.mapEquiv f) a = (LocalRing.ResidueField.map ↑f) a

source

@[simp]

theorem LocalRing.ResidueField.mapEquiv.symm {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] (f : R ≃+* S) :

(LocalRing.ResidueField.mapEquiv f).symm = LocalRing.ResidueField.mapEquiv f.symm

source

@[simp]

theorem LocalRing.ResidueField.mapEquiv_trans {R : Type u_1} {S : Type u_2} {T : Type u_3} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [CommRing T] [LocalRing T] (e₁ : R ≃+* S) (e₂ : S ≃+* T) :

LocalRing.ResidueField.mapEquiv (e₁.trans e₂) = (LocalRing.ResidueField.mapEquiv e₁).trans (LocalRing.ResidueField.mapEquiv e₂)

source

@[simp]

theorem LocalRing.ResidueField.mapEquiv_refl {R : Type u_1} [CommRing R] [LocalRing R] :

LocalRing.ResidueField.mapEquiv (RingEquiv.refl R) = RingEquiv.refl (LocalRing.ResidueField R)

source

def LocalRing.ResidueField.mapAut {R : Type u_1} [CommRing R] [LocalRing R] :

RingAut R →* RingAut (LocalRing.ResidueField R)

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

Equations

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

Instances For

source

@[simp]

theorem LocalRing.ResidueField.mapAut_apply {R : Type u_1} [CommRing R] [LocalRing R] (f : R ≃+* R) :

LocalRing.ResidueField.mapAut f = LocalRing.ResidueField.mapEquiv f

source

instance LocalRing.ResidueField.instMulSemiringAction {R : Type u_1} [CommRing R] [LocalRing R] (G : Type u_4) [Group G] [MulSemiringAction G R] :

MulSemiringAction G (LocalRing.ResidueField R)

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

Equations

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

source

@[simp]

theorem LocalRing.ResidueField.residue_smul {R : Type u_1} [CommRing R] [LocalRing R] (G : Type u_4) [Group G] [MulSemiringAction G R] (g : G) (r : R) :

(LocalRing.residue R) (g • r) = g • (LocalRing.residue R) r

source

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

Algebra (LocalRing.ResidueField R) (LocalRing.ResidueField S)

Equations

LocalRing.ResidueField.instAlgebra = (LocalRing.ResidueField.map (algebraMap R S)).toAlgebra

source

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

Algebra R (LocalRing.ResidueField S)

Equations

LocalRing.ResidueField.instAlgebra_1 = ((LocalRing.ResidueField.map (algebraMap R S)).comp (LocalRing.residue R)).toAlgebra

source

instance LocalRing.ResidueField.instIsScalarTower {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] :

IsScalarTower R (LocalRing.ResidueField R) (LocalRing.ResidueField S)

Equations

⋯ = ⋯

source

instance LocalRing.ResidueField.finiteDimensional_of_noetherian {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherian R S] :

FiniteDimensional (LocalRing.ResidueField R) (LocalRing.ResidueField S)

Equations

⋯ = ⋯

source

theorem LocalRing.ResidueField.finite_of_finite {R : Type u_1} {S : Type u_2} [CommRing R] [LocalRing R] [CommRing S] [LocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] [IsNoetherian R S] (hfin : Finite (LocalRing.ResidueField R)) :

Finite (LocalRing.ResidueField S)

source

theorem LocalRing.isLocalHom_residue {R : Type u_1} [CommRing R] [LocalRing R] :

IsLocalHom (LocalRing.residue R)

source

@[deprecated LocalRing.isLocalHom_residue]

theorem LocalRing.isLocalRingHom_residue {R : Type u_1} [CommRing R] [LocalRing R] :

IsLocalHom (LocalRing.residue R)

Alias of LocalRing.isLocalHom_residue.

Documentation

Mathlib.RingTheory.LocalRing.ResidueField.Basic

Residue Field of local rings #