Documentation

Schlessinger.Categories.Terminal

The residue field of Λ is a terminal object of the category of local Λ-residuealgebras. (shown for ArtinResAlg here)

source
instance instIsLocalHomResidueFieldAlgHomRestrictScalarsOfId_schlessinger (Λ Y : Type u) [CommRing Λ] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] :
IsLocalHom (AlgHom.restrictScalars Λ (Algebra.ofId Y (IsLocalRing.ResidueField Y)))
source
instance instIsLocalHomResidueFieldRingHomAlgebraMap_schlessinger (Λ Y : Type u) [CommRing Λ] [CommRing Y] [Algebra Λ Y] [IsLocalRing Y] [IsLocalHom (algebraMap Λ Y)] :
IsLocalHom (algebraMap Λ (IsLocalRing.ResidueField Y))
source
noncomputable def residuehom_artin (Λ : Type u) [CommRing Λ] (Y : Deformation.ArtinResAlg Λ) :
Y ⟶ Deformation.ArtinResAlg.of Λ (IsLocalRing.ResidueField ↑Y)
Equations
Instances For
    source
    noncomputable def residuehom_proartin (Λ : Type u) [CommRing Λ] (Y : Deformation.ProArtinResAlg Λ) :
    Y ⟶ Deformation.ProArtinResAlg.of Λ (IsLocalRing.ResidueField ↑Y)
    Equations
    Instances For
      source
      noncomputable def residuefieldiso_artin (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ArtinResAlg Λ) :
      Deformation.ArtinResAlg.of Λ (IsLocalRing.ResidueField Λ) ≅ Deformation.ArtinResAlg.of Λ (IsLocalRing.ResidueField ↑Y)
      Equations
      Instances For
        source
        @[simp]
        theorem residuefieldiso_artin_inv_hom_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ArtinResAlg Λ) (a : IsLocalRing.ResidueField ↑Y) :
        (residuefieldiso_artin Λ Y).inv.hom a = (IsResidueAlgebra.algEquiv Λ ↑Y).symm a
        source
        @[simp]
        theorem residuefieldiso_artin_hom_hom_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ArtinResAlg Λ) (a : IsLocalRing.ResidueField Λ) :
        (residuefieldiso_artin Λ Y).hom.hom a = (IsResidueAlgebra.algEquiv Λ ↑Y) a
        source
        noncomputable def residuefieldiso_proartin (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ProArtinResAlg Λ) :
        Deformation.ProArtinResAlg.of Λ (IsLocalRing.ResidueField Λ) ≅ Deformation.ProArtinResAlg.of Λ (IsLocalRing.ResidueField ↑Y)
        Equations
        Instances For
          source
          @[simp]
          theorem residuefieldiso_proartin_hom_hom_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ProArtinResAlg Λ) (a : IsLocalRing.ResidueField Λ) :
          (residuefieldiso_proartin Λ Y).hom.hom a = (IsResidueAlgebra.algEquiv Λ ↑Y) a
          source
          @[simp]
          theorem residuefieldiso_proartin_inv_hom_apply (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ProArtinResAlg Λ) (a : IsLocalRing.ResidueField ↑Y) :
          (residuefieldiso_proartin Λ Y).inv.hom a = (IsResidueAlgebra.algEquiv Λ ↑Y).symm a
          source
          def isTerminal_residueField_artin {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] :
          CategoryTheory.Limits.IsTerminal Deformation.ArtinResAlg.residueField

          Alias of Deformation.ArtinResAlg.isTerminalResidueField.

          𝕜 is terminal in ArtinResAlg.

          Equations
          Instances For
            source
            noncomputable def isTerminal_residueField_artin' (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ArtinResAlg Λ) :
            CategoryTheory.Limits.IsTerminal (Deformation.ArtinResAlg.of Λ (IsLocalRing.ResidueField ↑Y))
            Equations
            Instances For
              source
              def isTerminal_residueField_proartin {Λ : Type u} [CommRing Λ] [IsLocalRing Λ] :
              CategoryTheory.Limits.IsTerminal Deformation.ProArtinResAlg.residueField

              Alias of Deformation.ProArtinResAlg.isTerminalResidueField.

              𝕜 is terminal in ProArtinResAlg.

              Equations
              Instances For
                source
                noncomputable def isTerminal_residueField_proartin' (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] (Y : Deformation.ProArtinResAlg Λ) :
                CategoryTheory.Limits.IsTerminal (Deformation.ProArtinResAlg.of Λ (IsLocalRing.ResidueField ↑Y))
                Equations
                Instances For
                  source
                  instance instHasTerminalArtinResAlg (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] :
                  CategoryTheory.Limits.HasTerminal (Deformation.ArtinResAlg Λ)
                  source
                  instance instHasTerminalProArtinResAlg (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] :
                  CategoryTheory.Limits.HasTerminal (Deformation.ProArtinResAlg Λ)
                  source
                  instance instHasBinaryProductsArtinResAlg (Λ : Type u) [CommRing Λ] [IsLocalRing Λ] :
                  CategoryTheory.Limits.HasBinaryProducts (Deformation.ArtinResAlg Λ)