Documentation

Mathlib.RingTheory.LocalRing.ResidueField.Basic

Residue Field of local rings #

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

instance LocalRing.instIsScalarTowerResidueField (R : Type u_1) [CommRing R] [LocalRing 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] :
Equations
  • =

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

Equations
Instances For
    @[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) :

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

    Equations
    Instances For
      @[simp]

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

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

      A ring isomorphism defines an isomorphism of residue fields.

      Equations
      Instances For
        @[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) :

        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
          @[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
          @[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) :
          Equations
          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)] :
          Equations
          @[deprecated LocalRing.isLocalHom_residue]

          Alias of LocalRing.isLocalHom_residue.