feat(Algebra/Category): introduce the category of local algebras with a fixed residue field

Mathlib.lean

@@ -146,6 +146,10 @@ public import Mathlib.Algebra.Category.Grp.Zero
 public import Mathlib.Algebra.Category.GrpWithZero
 public import Mathlib.Algebra.Category.HopfAlgCat.Basic
 public import Mathlib.Algebra.Category.HopfAlgCat.Monoidal
+public import Mathlib.Algebra.Category.LocAlgCat.BaseCat
+public import Mathlib.Algebra.Category.LocAlgCat.Basic
+public import Mathlib.Algebra.Category.LocAlgCat.Cotangent
+public import Mathlib.Algebra.Category.LocAlgCat.Defs
 public import Mathlib.Algebra.Category.ModuleCat.AB
 public import Mathlib.Algebra.Category.ModuleCat.Abelian
 public import Mathlib.Algebra.Category.ModuleCat.Adjunctions
@@ -490,6 +494,7 @@ public import Mathlib.Algebra.Group.Units.Defs
 public import Mathlib.Algebra.Group.Units.Equiv
 public import Mathlib.Algebra.Group.Units.Hom
 public import Mathlib.Algebra.Group.Units.Opposite
+public import Mathlib.Algebra.Group.Units.ULift
 public import Mathlib.Algebra.Group.WithOne.Basic
 public import Mathlib.Algebra.Group.WithOne.Defs
 public import Mathlib.Algebra.Group.WithOne.Map

Mathlib/Algebra/Category/LocAlgCat/BaseCat.lean

@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Bingyu Xia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bingyu Xia
+-/
+
+module
+
+public import Mathlib.Algebra.Category.LocAlgCat.Basic
+public import Mathlib.RingTheory.Length
+
+import Mathlib.RingTheory.HopkinsLevitzki
+
+/-!
+# The Base Category for Deformation Theory
+
+This file introduces `BaseCat`, the base category used in formal deformation theory
+(e.g., for Schlessinger's criteria and Artin's axioms). It is defined as the full subcategory
+of `LocAlgCat Λ k` consisting of Artinian local algebras.
+
+## Main Results
+
+* `BaseCat`: The category of Artinian local `Λ`-algebras with a fixed residue field `k`.
+
+* `BaseCat.IsSmallExtension`: The typeclass representing a small extension.
+  A morphism `f : A ⟶ B` is a small extension if it is surjective and its kernel is a principal
+  ideal annihilated by the maximal ideal of `A`.
+
+* `BaseCat.induction_on_isSmallExtension`: Any surjective morphism in `BaseCat` can
+  be factored into a finite composition of small extensions.
+
+-/
+
+@[expose] public section
+
+universe w v u
+
+open IsLocalRing CategoryTheory Function
+
+variable {Λ : Type u} [CommRing Λ] {k : Type v} [Field k] [Algebra Λ k]
+
+/-- The base category for deformation theory over `Λ`. This is the full subcategory of
+`LocAlgCat Λ k` consisting of Artinian local `Λ`-algebras with residue field `k`. -/
+@[stacks 06GC]
+abbrev BaseCat (Λ : Type u) [CommRing Λ] (k : Type v) [Field k] [Algebra Λ k] :=
+  ObjectProperty.FullSubcategory fun A : LocAlgCat.{w} Λ k ↦ IsArtinianRing A
+
+namespace BaseCat
+
+variable {A B : BaseCat.{w} Λ k} {f : A ⟶ B}
+
+instance (A : BaseCat Λ k) : IsArtinianRing A.obj := A.property
+
+variable (Λ k) in
+/-- The object in the base category associated to a type equipped with appropriate typeclasses.
+This is a preferred way to construct a term of `BaseCat`. -/
+abbrev of (X : Type w) [CommRing X] [IsLocalRing X] [Algebra Λ X] [Algebra X k]
+    [IsScalarTower Λ X k] [IsArtinianRing X] (hX : Surjective (algebraMap X k)) :
+    BaseCat Λ k := ⟨.of Λ k X hX, inferInstance⟩
+
+/-- The quotient of an object `A` in `BaseCat` by a proper ideal `I`. -/
+def ofQuot (A : BaseCat.{w} Λ k) (I : Ideal A.obj) [Nontrivial (A.obj ⧸ I)] : BaseCat Λ k :=
+  ⟨A.obj.ofQuot I, Ideal.Quotient.mk_surjective.isArtinianRing⟩
+
+/-- Upgrades the canonical quotient map from `A` to `A ⧸ I` to a morphism in `BaseCat`. -/
+def toOfQuot (A : BaseCat.{w} Λ k) (I : Ideal A.obj) [Nontrivial (A.obj ⧸ I)] :
+    A ⟶ A.ofQuot I := ObjectProperty.homMk (A.obj.toOfQuot I)
+
+/-- A morphism `f : A ⟶ B` in `BaseCat` is a small extension if it is a surjective map
+whose kernel is a principal ideal annihilated by the maximal ideal of `A`. -/
+@[stacks 06GD]
+class IsSmallExtension (f : A ⟶ B) : Prop where
+  private mk ::
+  surjective (f) : Function.Surjective f.hom.toAlgHom
+  isPrincipal_ker (f) : (RingHom.ker f.hom.toAlgHom).IsPrincipal
+  le_annihilator_ker (f) : maximalIdeal A.obj ≤ (RingHom.ker f.hom.toAlgHom).annihilator
+
+theorem isSmallExtenstion_iff : IsSmallExtension f ↔ Function.Surjective f.hom.toAlgHom ∧
+    ∃ x : A.obj, Ideal.span {x} = RingHom.ker f.hom.toAlgHom ∧
+      ∀ y ∈ maximalIdeal A.obj, x * y = 0 := by
+  refine ⟨fun ⟨_, ⟨x, hx⟩, h⟩ ↦ ⟨IsSmallExtension.surjective f, x, ?_, fun y y_in ↦ ?_⟩,
+    fun ⟨h, x, x_span, hx⟩ ↦ ⟨h, ⟨x, ?_⟩, ?_⟩⟩
+  · simp [hx]
+  · rw [mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton, ← hx]
+    exact h y_in
+  · simp [← x_span]
+  · intro y y_in
+    rw [← x_span, Ideal.span, Submodule.mem_annihilator_span_singleton, smul_eq_mul, mul_comm]
+    exact hx y y_in
+
+theorem isSmallExtension_of_bijective (h : Bijective f.hom.toAlgHom) : IsSmallExtension f :=
+  (isSmallExtenstion_iff).mpr ⟨h.surjective, 0, by
+    have := h.injective
+    rw [RingHom.injective_iff_ker_eq_bot] at this
+    simp [this]⟩
+
+theorem IsSmallExtension.toOfQuot_span_singleton (A : BaseCat.{w} Λ k) (x : A.obj)
+    [Nontrivial (A.obj ⧸ (Ideal.span {x}))] (h : ∀ y ∈ maximalIdeal A.obj, x * y = 0) :
+    IsSmallExtension (A.toOfQuot (Ideal.span {x})) := by
+  rw [isSmallExtenstion_iff]
+  refine ⟨Ideal.Quotient.mk_surjective, x, ?_, h⟩
+  ext; rw [← Submodule.Quotient.mk_eq_zero]
+  exact Iff.rfl
+
+open Submodule in
+@[elab_as_elim, stacks 06GE]
+theorem induction_on_isSmallExtension (hf : Surjective f.hom.toAlgHom)
+    {P : ∀ {A B : BaseCat.{w} Λ k} (f : A ⟶ B), Surjective f.hom.toAlgHom → Prop}
+    (small_ext : ∀ {X Y : BaseCat.{w} Λ k} (f : X ⟶ Y) [IsSmallExtension f],
+      P f (IsSmallExtension.surjective f))
+    (comp : ∀ {A B C : BaseCat.{w} Λ k} (f : A ⟶ B) (g : B ⟶ C) [IsSmallExtension f]
+      (hg : Surjective g.hom.toAlgHom), P g hg →
+    P (f ≫ g) (hg.comp (IsSmallExtension.surjective f))) : P f hf := by
+  obtain ⟨n, hn⟩ : ∃ n : ℕ, n = Module.length A.obj A.obj :=
+    ENat.ne_top_iff_exists.mp Module.length_ne_top
+  symm at hn; revert A
+  induction n using Nat.strong_induction_on with
+  | h n ih =>
+    intro A f hf hlen
+    have hn : n ≠ 0 := by
+      intro hn; revert hlen
+      have : Nontrivial A.obj := inferInstance
+      simpa [hn, Module.length_eq_zero_iff, ← not_nontrivial_iff_subsingleton]
+    let I := RingHom.ker f.hom.toAlgHom
+    by_cases hI : I = ⊥
+    · rw [← RingHom.injective_iff_ker_eq_bot] at hI
+      have : IsSmallExtension f := isSmallExtension_of_bijective ⟨hI, hf⟩
+      exact small_ext f
+    obtain ⟨x, hx, x_ne⟩ := (Submodule.ne_bot_iff _).mp (Ideal.annihilator_inf_ne_bot
+      ((isArtinianRing_iff_isNilpotent_maximalIdeal A.obj).mp inferInstance) hI)
+    have x_in : x ∈ I := (mem_inf.mp hx).right
+    replace hx : ∀ y ∈ maximalIdeal A.obj, x * y = 0 := mem_annihilator.mp (mem_inf.mp hx).left
+    have span_ne_top : Ideal.span {x} ≠ ⊤ := by
+      refine Ideal.span_singleton_ne_top (le_maximalIdeal ?_ x_in)
+      rw [Ideal.ne_top_iff_exists_maximal]
+      exact ⟨maximalIdeal A.obj, maximalIdeal.isMaximal A.obj, le_maximalIdeal
+        (RingHom.ker_ne_top f.hom.toAlgHom)⟩
+    have : Nontrivial (A.obj ⧸ Ideal.span {x}) := Ideal.Quotient.nontrivial_iff.mpr span_ne_top
+    have : IsLocalRing (A.obj ⧸ Ideal.span {x}) := .of_surjective' _ Ideal.Quotient.mk_surjective
+    have aux : ∀ a ∈ Ideal.span {x}, (LocAlgCat.Hom.toAlgHom f.hom) a = 0 := by
+      intro _ h; rw [Ideal.mem_span_singleton'] at h
+      rcases h with ⟨_, rfl⟩; rw [← RingHom.mem_ker]
+      exact Ideal.mul_mem_left _ _ x_in
+    let C := A.ofQuot (Ideal.span {x})
+    let g : A ⟶ C := A.toOfQuot (Ideal.span {x})
+    have hg : IsSmallExtension g := IsSmallExtension.toOfQuot_span_singleton A x hx
+    let u : C.obj →ₐ[Λ] B.obj := Ideal.Quotient.liftₐ (Ideal.span {x}) f.hom.toAlgHom aux
+    have u_surj : Surjective u :=
+      Ideal.Quotient.lift_surjective_of_surjective (Ideal.span {x}) aux hf
+    let f' : C ⟶ B := ObjectProperty.homMk (LocAlgCat.ofHom u (eq_maximalIdeal
+      (Ideal.comap_isMaximal_of_surjective _ ‹_›)) (AlgHom.ext fun t ↦ by
+        induction t using Quotient.induction_on with
+        | H t =>
+          simp [← AlgHom.comp_apply, f.hom.residue_comp, u]
+          simpa [LocAlgCat.residue, ← Ideal.Quotient.algebraMap_eq] using
+            IsScalarTower.algebraMap_apply ..))
+    obtain ⟨m, hm⟩ : ∃ n : ℕ, n = Module.length C.obj C.obj :=
+      ENat.ne_top_iff_exists.mp Module.length_ne_top
+    symm at hm; suffices h : m < n by
+      change P (g ≫ f') _; apply comp
+      · apply ih m h; exact hm
+      · exact u_surj
+    change Module.length (A.obj ⧸ Ideal.span {x}) (A.obj ⧸ Ideal.span {x}) = m at hm
+    have := Submodule.length_le_length_restrictScalars A.obj (R := (A.obj ⧸ Ideal.span {x}))
+      (M := (A.obj ⧸ Ideal.span {x})) ⊤
+    rw [Module.length_top, restrictScalars_top, Module.length_top] at this
+    rw [← ENat.coe_lt_coe, ← hlen, ← hm]
+    exact lt_of_le_of_lt this (length_quotient_lt (Ideal.span {x}) (by simpa))
+
+end BaseCat

Mathlib/Algebra/Category/LocAlgCat/Basic.lean

@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2026 Bingyu Xia. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bingyu Xia
+-/
+
+module
+
+public import Mathlib.Algebra.Category.LocAlgCat.Defs
+
+/-!
+# Basic Constructions and Lemmas in `LocAlgCat`
+
+## Main Results
+
+* `LocAlgCat.ofQuot` : The object in `LocAlgCat` obtained from quotienting by a proper ideal.
+
+* `LocAlgCat.toOfQuot` : The canonical quotient morphism `A ⟶ A.ofQuot I`.
+
+* `LocAlgCat.mapOfQuot` : The categorical morphism between quotient objects induced
+  by a morphism `f : A ⟶ B`. This is the categorical counterpart to `Ideal.quotientMapₐ`.
+
+* `LocAlgCat.infinitesimalNeighborhood` : The quotient of a local algebra by the
+  `n`-th power of its maximal ideal.
+
+* `LocAlgCat.specialFiber` : The special fiber of `A` over a local base ring `Λ`,
+  defined as the quotient of `A` by the extended maximal ideal of `Λ`.
+
+-/
+
+@[expose] public section
+
+universe w v u
+
+namespace LocAlgCat
+
+open IsLocalRing CategoryTheory Function
+
+variable {Λ : Type u} [CommRing Λ] {k : Type v} [Field k] [Algebra Λ k] {A B : LocAlgCat.{w} Λ k}
+
+instance [IsLocalHom (algebraMap Λ k)] : IsLocalHom (algebraMap Λ A) :=
+  haveI : IsLocalHom ((algebraMap A k).comp (algebraMap Λ A)) := by
+    rwa [← IsScalarTower.algebraMap_eq]
+  isLocalHom_of_comp _ (algebraMap A k)
+
+lemma comap_algebraMap_maximalIdeal [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)] :
+    (maximalIdeal A).comap (algebraMap Λ A) = maximalIdeal Λ := by
+  have := ((local_hom_TFAE (algebraMap Λ k)).out 0 4).mp ‹_›
+  rw [eq_comm, ← this, IsScalarTower.algebraMap_eq Λ A, ← Ideal.comap_comap,
+    eq_maximalIdeal (Ideal.comap_isMaximal_of_surjective _ A.surj)]
+
+instance [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)] :
+    Nontrivial (A ⧸ ((maximalIdeal Λ).map (algebraMap Λ A))) :=
+  Ideal.Quotient.nontrivial_iff.mpr <| ne_top_of_le_ne_top
+  (maximalIdeal.isMaximal A).ne_top <| ((local_hom_TFAE (algebraMap Λ A)).out 0 2).mp
+    (by infer_instance)
+
+section ofQuot
+
+variable {I : Ideal A}
+
+/-- The residue algebra structure on `ofQuot`. -/
+instance ofQuotResidueAlgebra [Nontrivial (A ⧸ I)] : Algebra (A ⧸ I) k :=
+  (Ideal.Quotient.lift I (algebraMap A k) fun a a_in ↦ by
+    rw [← residue_apply, residue_eq_zero_iff]
+    exact le_maximalIdeal (by rwa [← Ideal.Quotient.nontrivial_iff]) a_in).toAlgebra
+
+instance isScalarTower_ofQuotResidueAlgebra [Nontrivial (A ⧸ I)] : IsScalarTower Λ (A ⧸ I) k :=
+  .of_algebraMap_eq fun r ↦ by rw [IsScalarTower.algebraMap_apply Λ A (A ⧸ I),
+    Ideal.Quotient.algebraMap_eq, RingHom.algebraMap_toAlgebra, Ideal.Quotient.lift_mk,
+    IsScalarTower.algebraMap_apply Λ A]
+
+instance isScalarTower_ofQuotResidueAlgebra' [Nontrivial (A ⧸ I)] : IsScalarTower A (A ⧸ I) k :=
+  .of_algebraMap_eq fun _ ↦ by rw [RingHom.algebraMap_toAlgebra, Ideal.Quotient.algebraMap_eq,
+    Ideal.Quotient.lift_mk]
+
+/-- The quotient of an object `A` in `LocAlgCat` by a proper ideal `I`. -/
+def ofQuot (A : LocAlgCat.{w} Λ k) (I : Ideal A) [Nontrivial (A ⧸ I)] : LocAlgCat.{w} Λ k :=
+  letI : IsLocalRing (A ⧸ I) := .of_surjective' _ Ideal.Quotient.mk_surjective
+  of Λ k (A ⧸ I) (Surjective.of_comp (g := Ideal.Quotient.mk _) (by
+    rw [← RingHom.coe_comp, RingHom.algebraMap_toAlgebra, Ideal.Quotient.lift_comp_mk]
+    exact A.surj))
+
+@[simp]
+lemma residue_ofQuot_mk_apply [Nontrivial (A ⧸ I)] (a : A) :
+    (A.ofQuot I).residue (Ideal.Quotient.mk I a) = A.residue a := rfl
+
+instance algebraOfQuot (A : LocAlgCat.{w} Λ k) {I : Ideal A} [Nontrivial (A ⧸ I)] :
+    Algebra A (A.ofQuot I) := Ideal.Quotient.algebra _
+
+instance isScalarTower_algebraOfQuot (A : LocAlgCat.{w} Λ k) {I : Ideal A} [Nontrivial (A ⧸ I)] :
+    IsScalarTower Λ A (A.ofQuot I) := .of_algebraMap_eq fun _ ↦ rfl
+
+/-- Upgrades the canonical quotient map from `A` to `A ⧸ I` to a morphism in `LocAlgCat`. -/
+def toOfQuot (A : LocAlgCat.{w} Λ k) (I : Ideal A) [Nontrivial (A ⧸ I)] : A ⟶ A.ofQuot I :=
+  letI : IsLocalRing (A ⧸ I) := .of_surjective' _ Ideal.Quotient.mk_surjective
+  ofHom (IsScalarTower.toAlgHom Λ A (A ⧸ I)) (eq_maximalIdeal (Ideal.comap_isMaximal_of_surjective
+    _ Ideal.Quotient.mk_surjective)) (by ext; simpa [residue] using residue_ofQuot_mk_apply ..)
+
+@[simp]
+lemma toAlgHom_toOfQuot_apply [Nontrivial (A ⧸ I)] (a : A) :
+    (A.toOfQuot I).toAlgHom a = Ideal.Quotient.mk I a := rfl
+
+@[simp]
+lemma ker_toAlgHom_toOfQuot [Nontrivial (A ⧸ I)] : RingHom.ker (A.toOfQuot I).toAlgHom = I :=
+  Ideal.mk_ker
+
+lemma surjective_toAlgHom_toOfQuot [Nontrivial (A ⧸ I)] : Surjective (A.toOfQuot I).toAlgHom :=
+  Ideal.Quotient.mk_surjective
+
+theorem map_toAlgHom_toOfQuot_maximalIdeal_eq [Nontrivial (A ⧸ I)] :
+    (maximalIdeal A).map (A.toOfQuot I).toAlgHom = maximalIdeal (A.ofQuot I) :=
+  map_maximalIdeal_of_surjective _ surjective_toAlgHom_toOfQuot
+
+/-- The morphism between quotient objects in `LocAlgCat` induced by a morphism `f : A ⟶ B`.
+This is the categorical counterpart to `Ideal.quotientMapₐ`. -/
+def mapOfQuot (f : A ⟶ B) {J : Ideal B} [Nontrivial (A ⧸ I)] [Nontrivial (B ⧸ J)]
+    (hf : I ≤ J.comap f.toAlgHom) : A.ofQuot I ⟶ B.ofQuot J :=
+  haveI : IsLocalRing (A ⧸ I) := .of_surjective' _ Ideal.Quotient.mk_surjective
+  haveI : IsLocalRing (B ⧸ J) := .of_surjective' _ Ideal.Quotient.mk_surjective
+  ofHom (Ideal.quotientMapₐ J f.toAlgHom hf) (by
+    rw [← (Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective).eq_iff,
+      ← Ideal.comap_coe (Ideal.quotientMapₐ J f.toAlgHom hf), Ideal.comap_comap]
+    change Ideal.comap (((Ideal.quotientMap J f.toAlgHom hf)).comp (Ideal.Quotient.mk I))
+      (maximalIdeal (B ⧸ J)) = _
+    rw [Ideal.quotientMap_comp_mk, ← Ideal.comap_comap, Ideal.comap_coe, eq_maximalIdeal
+      (Ideal.comap_isMaximal_of_surjective ((Ideal.Quotient.mk J)) Ideal.Quotient.mk_surjective),
+        f.comap_maximalIdeal_eq, eq_maximalIdeal (Ideal.comap_isMaximal_of_surjective
+          (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective)] ) (AlgHom.ext fun x ↦ by
+    rcases Ideal.Quotient.mk_surjective x with ⟨x, rfl⟩
+    exact DFunLike.congr_fun f.residue_comp x )
+
+@[simp, reassoc]
+theorem toOfQuot_comp_mapOfQuot (f : A ⟶ B) {J : Ideal B} [Nontrivial (A ⧸ I)] [Nontrivial (B ⧸ J)]
+    (hf : I ≤ J.comap f.toAlgHom) : A.toOfQuot I ≫ mapOfQuot f hf = f ≫ B.toOfQuot J := rfl
+
+@[simp]
+lemma toAlgHom_mapOfQuot_apply (f : A ⟶ B) {J : Ideal B} [Nontrivial (A ⧸ I)] [Nontrivial (B ⧸ J)]
+    (hf : I ≤ J.comap f.toAlgHom) (a : A) : (mapOfQuot f hf).toAlgHom (Ideal.Quotient.mk I a) =
+      Ideal.Quotient.mk J (f.toAlgHom a) := rfl
+
+/-- The quotient of a local algebra by the `n`-th power of its maximal ideal.
+Geometrically, this represents an infinitesimal neighborhood of the closed point. -/
+abbrev infinitesimalNeighborhood {n : ℕ} (hn : n ≠ 0) (A : LocAlgCat.{w} Λ k) : LocAlgCat Λ k :=
+  letI : Nontrivial (A ⧸ (maximalIdeal A) ^ n) := by
+    rw [Ideal.Quotient.nontrivial_iff, Ideal.ne_top_iff_exists_maximal]
+    exact ⟨maximalIdeal A, maximalIdeal.isMaximal A, Ideal.pow_le_self hn⟩
+  A.ofQuot (maximalIdeal A ^ n)
+
+/-- The canonical quotient morphism from `A` to its infinitesimal neighborhood. -/
+abbrev toInfinitesimalNeighborhood {n : ℕ} (hn : n ≠ 0) (A : LocAlgCat.{w} Λ k) :
+    A ⟶ A.infinitesimalNeighborhood hn :=
+  letI : Nontrivial (A ⧸ (maximalIdeal A) ^ n) := by
+    rw [Ideal.Quotient.nontrivial_iff, Ideal.ne_top_iff_exists_maximal]
+    exact ⟨maximalIdeal A, maximalIdeal.isMaximal A, Ideal.pow_le_self hn⟩
+  toOfQuot ..
+
+/-- The morphism between infinitesimal neighborhoods induced by a morphism in `LocAlgCat`. -/
+abbrev mapInfinitesimalNeighborhood {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hmn : n ≤ m) (f : A ⟶ B) :
+    A.infinitesimalNeighborhood hm ⟶ B.infinitesimalNeighborhood hn :=
+  letI : Nontrivial (A ⧸ (maximalIdeal A) ^ m) := by
+    rw [Ideal.Quotient.nontrivial_iff, Ideal.ne_top_iff_exists_maximal]
+    exact ⟨maximalIdeal A, maximalIdeal.isMaximal A, Ideal.pow_le_self hm⟩
+  letI : Nontrivial (B ⧸ (maximalIdeal B) ^ n) := by
+    rw [Ideal.Quotient.nontrivial_iff, Ideal.ne_top_iff_exists_maximal]
+    exact ⟨maximalIdeal B, maximalIdeal.isMaximal B, Ideal.pow_le_self hn⟩
+  mapOfQuot f (le_trans (Ideal.pow_le_pow_right hmn) (f.comap_maximalIdeal_eq ▸
+      Ideal.le_comap_pow f.toAlgHom n))
+
+/-- The special fiber of `A` over `Λ` when `Λ` is a local ring, defined as the quotient by
+the extended maximal ideal of `Λ`, viewed as an object in `LocAlgCat`. -/
+abbrev specialFiber [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)]
+    (A : LocAlgCat.{w} Λ k) : LocAlgCat.{w} Λ k := A.ofQuot ((maximalIdeal Λ).map (algebraMap Λ A))
+
+/-- The canonical morphism from `A` to its special fiber. -/
+abbrev toSpecialFiber [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)]
+    (A : LocAlgCat.{w} Λ k) : A ⟶ A.specialFiber := toOfQuot ..
+
+/-- The morphism between special fibers induced by a morphism between two objects. -/
+abbrev mapSpecialFiber [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)]
+    (f : A ⟶ B) : A.specialFiber ⟶ B.specialFiber :=
+  mapOfQuot f (by rw [Ideal.map_le_iff_le_comap, ← Ideal.comap_coe f.toAlgHom,
+    Ideal.comap_comap, AlgHom.comp_algebraMap, ← Ideal.map_le_iff_le_comap])
+
+@[simp]
+lemma algebraMap_specialFiber_apply_eq_zero [IsLocalRing Λ] [IsLocalHom (algebraMap Λ k)]
+    (A : LocAlgCat.{w} Λ k) {y : Λ} (y_in : y ∈ maximalIdeal Λ) :
+    algebraMap Λ A.specialFiber y = 0 := by
+  rw [IsScalarTower.algebraMap_apply Λ A A.specialFiber]
+  exact Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_map_of_mem _ y_in)
+
+end ofQuot
+
+end LocAlgCat