Categories.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

36 declarations, 0 contain sorry, 0 declared as axioms

The category of local proartinian algebras

We define IsLocalProartinianAlgebra, the typeclass for topological rings which are local and proartinian, and the category ProartinianCat 𝓞 of local proartinian 𝓞-algebras with a fixed residue field.

Imports (7)

Imported by 2 files

class Deformation.IsLocalProartinianAlgebra A local proartinian algebra is a topological ring that is local and proartinian, and that the induced map on the residue fields is bijective line 36 source
Source documentation
A local proartinian algebra is a topological ring that is local and proartinian, and that the induced map on the residue fields is bijective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, Algebra
2 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
class IsLocalProartinianAlgebra
    (R : Type u) [CommRing R] [TopologicalSpace R] [Algebra 𝓞 R] : Prop extends
  IsTopologicalRing R, IsLocalRing R, IsProartinian R,
  IsLocalHom (algebraMap 𝓞 R), IsResidueAlgebra 𝓞 R

section 𝓞_is_local

-- if 𝓞 admits a local proartinian algebra then 𝓞 is itself local.
```
Mentions: IsProartinian, IsResidueAlgebra
example Deformation.(example at line 44) line 44 source
Source comment
if 𝓞 admits a local proartinian algebra then 𝓞 is itself local.
```
example (𝓞 : Type u) [CommRing 𝓞]
    (R : Type u) [CommRing R] [TopologicalSpace R]
    [Algebra 𝓞 R] [IsLocalProartinianAlgebra 𝓞 R] : IsLocalRing 𝓞 := by
…
```
Mentions: Deformation.IsLocalProartinianAlgebra

example Deformation.(example at line 60) line 60 source

Source comment

If 𝓞 is a local ring complete wrt m-adic topology then 𝓞 → R is continuous.

example (𝓞 : Type u) [CommRing 𝓞] [TopologicalSpace 𝓞] [IsTopologicalRing 𝓞]
    [IsLocalRing 𝓞] [IsAdicTopology 𝓞]
    (R : Type u) [CommRing R] [TopologicalSpace R]
    [Algebra 𝓞 R] [IsLocalProartinianAlgebra 𝓞 R] : Continuous (algebraMap 𝓞 R) :=
…

Mentions: Deformation.IsLocalProartinianAlgebra

structure Deformation.ProartinianCat The category of local proartinian algebras over 𝓞 with fixed residue field 𝕜 line 69 source
Source documentation
The category of local proartinian algebras over 𝓞 with fixed residue field 𝕜.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing
```
structure ProartinianCat where
…
```
instance Deformation.ProartinianCat.(instance at line 88) line 88 source
abbrev Deformation.ProartinianCat.of Make a ProartinianCat from an unbundled algebra line 93 source
Source documentation
Make a ProartinianCat from an unbundled algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, Deformation.ProartinianCat
Proof uses: Deformation.ProartinianCat.mk
4 instances, coercions and auxiliary constants left out.
```
abbrev of (X : Type u) [CommRing X] [Algebra 𝓞 X]
    [TopologicalSpace X] [IsLocalProartinianAlgebra 𝓞 X] :
    ProartinianCat 𝓞 :=
…
```
Mentions: Deformation.IsLocalProartinianAlgebra, Deformation.ProartinianCat
lemma Deformation.ProartinianCat.coe_of line 98 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, Eq, Deformation.ProartinianCat.of
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
structure Deformation.ProartinianCat.Hom The type of morphisms in ProartinianCat 𝓞 line 105 source
Source documentation
The type of morphisms in ProartinianCat 𝓞.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
structure Hom (A B : ProartinianCat 𝓞) where
…
```
Mentions: Deformation.ProartinianCat
instance Deformation.ProartinianCat.(instance at line 109) line 109 source
instance Deformation.ProartinianCat.(instance at line 114) line 114 source
abbrev Deformation.ProartinianCat.ofHom Typecheck an ContinuousAlgHom as a morphism in ProartinianCat line 120 source
Source documentation
Typecheck an ContinuousAlgHom as a morphism in ProartinianCat.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, ContinuousAlgHom, Quiver.Hom, Deformation.ProartinianCat, Deformation.ProartinianCat.of
Proof uses: Deformation.ProartinianCat.Hom.mk
7 instances, coercions and auxiliary constants left out.
```
abbrev ofHom {A B : Type u}
    [CommRing A] [Algebra 𝓞 A] [TopologicalSpace A] [IsLocalProartinianAlgebra 𝓞 A]
    [CommRing B] [Algebra 𝓞 B] [TopologicalSpace B] [IsLocalProartinianAlgebra 𝓞 B]
    (f : A →A[𝓞] B) :
    of 𝓞 A ⟶ of 𝓞 B := ⟨f⟩
…
```
Mentions: Deformation.IsLocalProartinianAlgebra, Deformation.ProartinianCat.of
lemma Deformation.ProartinianCat.hom_id line 136 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat, Eq, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, CategoryTheory.CategoryStruct.id, ContinuousAlgHom.id
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.id_apply line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat, Eq, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, CategoryTheory.CategoryStruct.id
Proof uses: rfl
20 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.hom_comp line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat, Quiver.Hom, Eq, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, CategoryTheory.CategoryStruct.comp, ContinuousAlgHom.comp
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.comp_apply line 143 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat, Quiver.Hom, Eq, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, CategoryTheory.CategoryStruct.comp
Proof uses: rfl
22 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.hom_ext line 146 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat, Quiver.Hom, Eq, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom
Proof uses: Deformation.ProartinianCat.Hom.ext
18 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.hom_ofHom line 149 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, ContinuousAlgHom, Eq, Deformation.ProartinianCat.of, Deformation.ProartinianCat.Hom.hom, Deformation.ProartinianCat.ofHom
Proof uses: rfl
12 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.ofHom_hom line 152 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Deformation.ProartinianCat, Quiver.Hom, Eq, Deformation.ProartinianCat.of, Deformation.ProartinianCat.ofHom, Deformation.ProartinianCat.Hom.hom
Proof uses: rfl
16 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.ofHom_id line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, Eq, Quiver.Hom, Deformation.ProartinianCat, Deformation.ProartinianCat.of, Deformation.ProartinianCat.ofHom, ContinuousAlgHom.id, CategoryTheory.CategoryStruct.id
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.ofHom_comp line 158 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, ContinuousAlgHom, Eq, Quiver.Hom, Deformation.ProartinianCat, Deformation.ProartinianCat.of, Deformation.ProartinianCat.ofHom, ContinuousAlgHom.comp, CategoryTheory.CategoryStruct.comp
Proof uses: rfl
10 instances, coercions and auxiliary constants left out.
def Deformation.ProartinianCat.ofEquiv Build an isomorphism in the category ProartinianCat R from a ContinuousAlgEquiv between Algebras line 165 source
Source documentation
Build an isomorphism in the category ProartinianCat R from a ContinuousAlgEquiv between Algebras.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, Deformation.IsLocalProartinianAlgebra, ContinuousAlgEquiv, CategoryTheory.Iso, Deformation.ProartinianCat, Deformation.ProartinianCat.of
Proof uses: CategoryTheory.Iso.mk, Deformation.ProartinianCat.ofHom, ContinuousAlgEquiv.symm
9 instances, coercions and auxiliary constants left out.
```
def ofEquiv (e : X ≃A[𝓞] Y) : of 𝓞 X ≅ of 𝓞 Y where
…
```
Mentions: Deformation.ProartinianCat.of
def Deformation.ProartinianCat._root_.CategoryTheory.Iso.toContinuousAlgEquiv Build a ContinuousAlgEquiv from an isomorphism in the category ProartinianCat R line 170 source
Source documentation
Build a ContinuousAlgEquiv from an isomorphism in the category ProartinianCat R.
```
def _root_.CategoryTheory.Iso.toContinuousAlgEquiv (i : A ≅ B) : A ≃A[𝓞] B where
…
```
def Deformation.ProartinianCat.self 𝓞 as a proartinian local algebra line 184 source
Source documentation
𝓞 as a proartinian local algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Finite, IsLocalRing.ResidueField, IsAdicComplete, IsLocalRing.maximalIdeal, Deformation.ProartinianCat
Proof uses: Deformation.ProartinianCat.mk, Ideal.adicTopology
12 instances, coercions and auxiliary constants left out.
```
def self : 𝓒 𝓞 where
…
```
instance Deformation.ProartinianCat.(instance at line 193) line 193 source
def Deformation.ProartinianCat.fromSelf The structure map of a proartinian local algebra as a morphism in the category line 196 source
Source documentation
The structure map of a proartinian local algebra as a morphism in the category.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Finite, IsLocalRing.ResidueField, IsAdicComplete, IsLocalRing.maximalIdeal, Deformation.ProartinianCat, Quiver.Hom, Deformation.ProartinianCat.self
Proof uses: Deformation.ProartinianCat.Hom.mk, ContinuousAlgHom.mk, Algebra.ofId
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def fromSelf (R : ProartinianCat 𝓞) : self ⟶ R where
…
```
Mentions: Deformation.ProartinianCat, Deformation.ProartinianCat.self
instance Deformation.ProartinianCat.(instance at line 203) line 203 source
def Deformation.ProartinianCat.isInitialSelf 𝓞 is initial in ProartinianCat line 210 source
Source documentation
𝓞 is initial in ProartinianCat.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, IsNoetherianRing, Finite, IsLocalRing.ResidueField, IsAdicComplete, IsLocalRing.maximalIdeal, CategoryTheory.Limits.IsInitial, Deformation.ProartinianCat, Deformation.ProartinianCat.self
Proof uses: CategoryTheory.Limits.IsInitial.ofUnique
13 instances, coercions and auxiliary constants left out.
```
def isInitialSelf : IsInitial (self (𝓞 := 𝓞)) := .ofUnique _
…
```
Mentions: Deformation.ProartinianCat.self
def Deformation.ProartinianCat.residueField The residue field 𝕜 as a proartinian local algebra line 220 source
Source documentation
The residue field 𝕜 as a proartinian local algebra.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Deformation.ProartinianCat
Proof uses: Deformation.ProartinianCat.mk, IsLocalRing.ResidueField, Bot.bot, TopologicalSpace
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def residueField : 𝓒 𝓞 where
…
```
instance Deformation.ProartinianCat.(instance at line 229) line 229 source
instance Deformation.ProartinianCat.(instance at line 232) line 232 source
def Deformation.ProartinianCat.toResidueField line 237 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Deformation.ProartinianCat, Quiver.Hom, Deformation.ProartinianCat.residueField
Proof uses: Deformation.ProartinianCat.Hom.mk, ContinuousAlgHom.mk, AlgHom.comp, IsLocalRing.ResidueField, AlgEquiv.symm, IsResidueAlgebra.algEquiv, IsScalarTower.toAlgHom
22 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma Deformation.ProartinianCat.toResidueField_surjective line 247 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Deformation.ProartinianCat, Function.Surjective, Deformation.ProartinianCat.residueField, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, Deformation.ProartinianCat.toResidueField
Proof uses: Function.Surjective.comp, IsLocalRing.ResidueField, AlgEquiv, AlgEquiv.symm, IsResidueAlgebra.algEquiv, RingHom, AlgHom, IsScalarTower.toAlgHom, AlgEquiv.surjective, Ideal.Quotient.mk_surjective, IsLocalRing.maximalIdeal
34 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.ker_toResidueField line 251 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Deformation.ProartinianCat, Eq, Ideal, RingHom.ker, Deformation.ProartinianCat.residueField, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, Deformation.ProartinianCat.toResidueField, IsLocalRing.maximalIdeal
Proof uses: Eq.trans, IsLocalRing.ResidueField, RingHom, RingHom.comp, RingEquiv.toRingHom, AlgEquiv.toRingEquiv, AlgEquiv.symm, IsResidueAlgebra.algEquiv, AlgHom, IsScalarTower.toAlgHom, RingHom.ker_comp_of_injective, AlgEquiv.injective, Ideal.mk_ker
42 instances, coercions and auxiliary constants left out.
lemma Deformation.ProartinianCat.to_residueField_apply line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, Deformation.ProartinianCat, Quiver.Hom, Deformation.ProartinianCat.residueField, Eq, ContinuousAlgHom, Deformation.ProartinianCat.Hom.hom, RingHom, IsLocalRing.ResidueField, IsLocalRing.residue, IsResidueAlgebra.preimage
Proof uses: Trans.simple, Algebra.algebraMap, Eq.mpr, HSub.hSub, OfNat.ofNat, id, congrArg, Eq.symm, propext, sub_eq_zero, map_sub, outParam, MonoidHom, MonoidHom.id, Not, Ne, not_ne_iff, IsUnit, isUnit_iff_ne_zero, AlgHom.toRingHom and 12 more
90 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
instance Deformation.ProartinianCat.(instance at line 268) line 268 source
def Deformation.ProartinianCat.isTerminalResidueField line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, CategoryTheory.Limits.IsTerminal, Deformation.ProartinianCat, Deformation.ProartinianCat.residueField
Proof uses: CategoryTheory.Limits.IsTerminal.ofUnique
7 instances, coercions and auxiliary constants left out.