Homology.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

17 declarations, 0 contain sorry, 0 declared as axioms

Kernels, cokernels and homology of topological modules

This file develops API for the concrete kernel and cokernel models of TopModuleCat:

TopModuleCat.cokerDesc: the universal property of the concrete quotient TopModuleCat.coker.
TopModuleCat.cokerCongr: cokernels of morphisms identified under an isomorphism of the targets are isomorphic.
TopModuleCat.cokerDescCLM and TopModuleCat.cokerDescBilinear: descending continuous linear maps and jointly continuous bilinear pairings along cokernel projections.
HomologicalComplex.cyclesIsoKer and HomologicalComplex.homologyIsoCoker: the cycles and homology of a complex of topological modules identified with the kernel of the differential carrying the subspace topology, respectively the quotient of the cycles by the boundaries carrying the quotient topology.

Material destined for Mathlib.Algebra.Category.ModuleCat.Topology.Homology.

Imports (3)

Imported by 3 files

def TopModuleCat.cokerDesc The universal property of the concrete quotient TopModuleCat.coker: a morphism killing the range descends to the quotient line 46 source
Source documentation
The universal property of the concrete quotient TopModuleCat.coker: a morphism killing the range descends to the quotient.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, Eq, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, TopModuleCat.coker
Proof uses: CategoryTheory.Limits.IsColimit.desc, CategoryTheory.Limits.WalkingParallelPair, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.CokernelCofork.ofπ, TopModuleCat.cokerπ, TopModuleCat.isColimitCoker
18 instances, coercions and auxiliary constants left out.
```
noncomputable def cokerDesc (φ : M ⟶ N) (ψ : N ⟶ P) (w : φ ≫ ψ = 0) : coker φ ⟶ P :=
…
```
lemma TopModuleCat.cokerπ_cokerDesc line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, Eq, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, TopModuleCat.coker, TopModuleCat.cokerπ, TopModuleCat.cokerDesc
Proof uses: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.WalkingParallelPair, CategoryTheory.Limits.parallelPair, CategoryTheory.Limits.CokernelCofork.ofπ, TopModuleCat.comp_cokerπ, TopModuleCat.isColimitCoker, CategoryTheory.Limits.WalkingParallelPair.one
17 instances, coercions and auxiliary constants left out.
lemma TopModuleCat.cokerDesc_apply line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, Eq, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, TopModuleCat.toModuleCat, ContinuousLinearMap, RingHom.id, TopModuleCat.coker, CategoryTheory.ConcreteCategory.hom, TopModuleCat.cokerDesc, TopModuleCat.cokerπ
Proof uses: id, congrArg, TopModuleCat.cokerπ_cokerDesc
36 instances, coercions and auxiliary constants left out.
lemma TopModuleCat.cokerπ_eq_zero_iff line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, TopModuleCat.toModuleCat, Iff, Eq, TopModuleCat.coker, ContinuousLinearMap, RingHom.id, CategoryTheory.ConcreteCategory.hom, TopModuleCat.cokerπ, OfNat.ofNat, LinearMap.range, TopModuleCat.Hom.hom, Membership.mem, Submodule
Proof uses: Submodule.Quotient.mk_eq_zero
34 instances, coercions and auxiliary constants left out.
def TopModuleCat.cokerCongr Cokernels of morphisms identified under an isomorphism of the targets are isomorphic line 64 source
Source documentation
Cokernels of morphisms identified under an isomorphism of the targets are isomorphic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, CategoryTheory.Iso, Eq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, TopModuleCat.coker
Proof uses: CategoryTheory.Iso.mk, TopModuleCat.cokerDesc, TopModuleCat.cokerπ, CategoryTheory.Iso.inv
12 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
noncomputable def cokerCongr {φ : M ⟶ N} {ψ : M ⟶ N'} (e : N ≅ N') (w : φ ≫ e.hom = ψ) :
    coker φ ≅ coker ψ where
…
```
lemma TopModuleCat.cokerπ_cokerCongr_hom line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, CategoryTheory.Iso, Eq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, TopModuleCat.coker, TopModuleCat.cokerπ, TopModuleCat.cokerCongr
Proof uses: TopModuleCat.cokerπ_cokerDesc
9 instances, coercions and auxiliary constants left out.
lemma TopModuleCat.isOpenQuotientMap_cokerπ line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, IsOpenQuotientMap, TopModuleCat.toModuleCat, TopModuleCat.coker, LinearMap.range, RingHom.id, TopModuleCat.Hom.hom, ContinuousLinearMap, TopModuleCat.cokerπ
Proof uses: Submodule.isOpenQuotientMap_mkQ
34 instances, coercions and auxiliary constants left out.
lemma TopModuleCat.cokerπ_surjective' line 79 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, TopModuleCat.toModuleCat, TopModuleCat.coker, Exists, Eq, ContinuousLinearMap, RingHom.id, CategoryTheory.ConcreteCategory.hom, TopModuleCat.cokerπ
Proof uses: TopModuleCat.cokerπ_surjective
19 instances, coercions and auxiliary constants left out.
def TopModuleCat.cokerDescCLM Descend a continuous linear map along cokernel projections on both sides line 87 source
Source documentation
Descend a continuous linear map along cokernel projections on both sides.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, ContinuousLinearMap, RingHom.id, TopModuleCat.toModuleCat, Eq, TopModuleCat.coker, CategoryTheory.ConcreteCategory.hom, TopModuleCat.cokerπ, OfNat.ofNat, LinearMap.range, TopModuleCat.Hom.hom
Proof uses: TopModuleCat.of, TopModuleCat.cokerDesc, TopModuleCat.ofHom, ContinuousLinearMap.comp
52 instances, coercions and auxiliary constants left out.
```
noncomputable def cokerDescCLM (φ₂ : M₂ ⟶ N₂) (φ₃ : M₃ ⟶ N₃) (u : ↥N₂ →L[k] ↥N₃)
    (h : ∀ y, cokerπ φ₃ (u (φ₂ y)) = 0) :
    ↥(coker φ₂) →L[k] ↥(coker φ₃) :=
…
```
lemma TopModuleCat.cokerDescCLM_apply line 94 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, ContinuousLinearMap, RingHom.id, TopModuleCat.toModuleCat, Eq, TopModuleCat.coker, CategoryTheory.ConcreteCategory.hom, TopModuleCat.cokerπ, OfNat.ofNat, LinearMap.range, TopModuleCat.Hom.hom, TopModuleCat.cokerDescCLM
Proof uses: id, congrArg, TopModuleCat.of, CategoryTheory.CategoryStruct.comp, TopModuleCat.cokerDesc, TopModuleCat.ofHom, ContinuousLinearMap.comp, CategoryTheory.ConcreteCategory.hom_ext, TopModuleCat.cokerπ_cokerDesc
59 instances, coercions and auxiliary constants left out.
lemma TopModuleCat.continuous_cokerDescCLM_uncurry The descended family of continuous linear maps has jointly continuous uncurried form line 103 source
Source documentation
The descended family of continuous linear maps has jointly continuous uncurried form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, TopModuleCat.toModuleCat, ContinuousLinearMap, RingHom.id, Eq, TopModuleCat.coker, CategoryTheory.ConcreteCategory.hom, TopModuleCat.cokerπ, OfNat.ofNat, LinearMap.range, TopModuleCat.Hom.hom, Continuous, Prod, Prod.fst, Prod.snd, TopModuleCat.cokerDescCLM
Proof uses: Iff.mp, Function.comp, Prod.map, id, IsOpenQuotientMap.continuous_comp_iff, IsOpenQuotientMap.prodMap, IsOpenQuotientMap.id, TopModuleCat.isOpenQuotientMap_cokerπ, Continuous.comp, LinearMap, ContinuousLinearMap.continuous
51 instances, coercions and auxiliary constants left out.
```
lemma continuous_cokerDescCLM_uncurry (φ₂ : M₂ ⟶ N₂) (φ₃ : M₃ ⟶ N₃)
    (F : ↥N₁ → (↥N₂ →L[k] ↥N₃)) (h : ∀ σ y, cokerπ φ₃ (F σ (φ₂ y)) = 0)
    (hF : Continuous fun p : ↥N₁ × ↥N₂ ↦ F p.1 p.2) :
    Continuous fun p : ↥N₁ × ↥(coker φ₂) ↦ cokerDescCLM φ₂ φ₃ (F p.1) (h p.1) p.2 :=
…
```
Mentions: TopModuleCat.cokerDescCLM
def TopModuleCat.cokerDescBilinear Descend a bilinear pairing, bundled as a morphism into the internal hom, along cokernel projections in all three slots line 112 source
Source documentation
Descend a bilinear pairing, bundled as a morphism into the internal hom, along cokernel projections in all three slots.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, TopModuleCat.linHom, Continuous, Prod, TopModuleCat.toModuleCat, RingHom.id, ContinuousLinearMap, CategoryTheory.ConcreteCategory.hom, Prod.fst, Prod.snd, Eq, TopModuleCat.coker, TopModuleCat.cokerπ, OfNat.ofNat, LinearMap.range, TopModuleCat.Hom.hom
Proof uses: TopModuleCat.cokerDesc, TopModuleCat.homOfBilinear, TopModuleCat.cokerDescCLM
48 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
noncomputable def cokerDescBilinear {M₁ : TopModuleCat.{v} k}
    (φ₁ : M₁ ⟶ N₁) (φ₂ : M₂ ⟶ N₂) (φ₃ : M₃ ⟶ N₃) (F : N₁ ⟶ linHom N₂ N₃)
    (hF : Continuous fun p : ↥N₁ × ↥N₂ ↦ F p.1 p.2)
    (h₁ : ∀ (y : ↥M₁) (τ : ↥N₂), cokerπ φ₃ (F (φ₁ y) τ) = 0)
    (h₂ : ∀ (σ : ↥N₁) (y : ↥M₂), cokerπ φ₃ (F σ (φ₂ y)) = 0) :
    coker φ₁ ⟶ linHom (coker φ₂) (coker φ₃) :=
…
```
Mentions: TopModuleCat.linHom
lemma TopModuleCat.cokerDescBilinear_apply line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, TopModuleCat, Quiver.Hom, TopModuleCat.linHom, Continuous, Prod, TopModuleCat.toModuleCat, RingHom.id, ContinuousLinearMap, CategoryTheory.ConcreteCategory.hom, Prod.fst, Prod.snd, Eq, TopModuleCat.coker, TopModuleCat.cokerπ, OfNat.ofNat, LinearMap.range, TopModuleCat.Hom.hom, TopModuleCat.cokerDescBilinear
Proof uses: rfl
44 instances, coercions and auxiliary constants left out.
def HomologicalComplex.cyclesIsoKer The cycles of a complex of topological modules, identified with the kernel of the differential carrying the subspace topology line 157 source
Source documentation
The cycles of a complex of topological modules, identified with the kernel of the differential carrying the subspace topology.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, ComplexShape, HomologicalComplex, TopModuleCat, Eq, ComplexShape.next, CategoryTheory.Iso, HomologicalComplex.cycles, HomologicalComplex.sc, TopModuleCat.ker, HomologicalComplex.X, HomologicalComplex.d
Proof uses: CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit, CategoryTheory.Limits.KernelFork.ofι, HomologicalComplex.iCycles, TopModuleCat.kerι, HomologicalComplex.cyclesIsKernel, TopModuleCat.isLimitKer, CategoryTheory.Iso.refl, CategoryTheory.Arrow, CategoryTheory.Arrow.mk
14 instances, coercions and auxiliary constants left out.
```
noncomputable def cyclesIsoKer (i j : ι) (hij : c.next i = j) :
    K.cycles i ≅ TopModuleCat.ker (K.d i j) :=
…
```
lemma HomologicalComplex.cyclesIsoKer_hom_kerι line 162 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, ComplexShape, HomologicalComplex, TopModuleCat, Eq, ComplexShape.next, Quiver.Hom, HomologicalComplex.cycles, HomologicalComplex.sc, HomologicalComplex.X, CategoryTheory.CategoryStruct.comp, TopModuleCat.ker, HomologicalComplex.d, CategoryTheory.Iso.hom, HomologicalComplex.cyclesIsoKer, TopModuleCat.kerι, HomologicalComplex.iCycles
Proof uses: CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι, CategoryTheory.Limits.KernelFork.ofι, TopModuleCat.kerι_comp, TopModuleCat.isLimitKer, CategoryTheory.CategoryStruct.id, CategoryTheory.Arrow, CategoryTheory.Arrow.mk
16 instances, coercions and auxiliary constants left out.
lemma HomologicalComplex.cyclesIsoKer_hom_apply_coe line 167 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, ComplexShape, HomologicalComplex, TopModuleCat, Eq, ComplexShape.next, TopModuleCat.toModuleCat, HomologicalComplex.cycles, HomologicalComplex.sc, HomologicalComplex.X, Membership.mem, Submodule, LinearMap.ker, RingHom.id, TopModuleCat.Hom.hom, HomologicalComplex.d, ContinuousLinearMap, TopModuleCat.ker, CategoryTheory.ConcreteCategory.hom and 3 more
Proof uses: id, congrArg, Quiver.Hom, CategoryTheory.CategoryStruct.comp, TopModuleCat.kerι, HomologicalComplex.cyclesIsoKer_hom_kerι
42 instances, coercions and auxiliary constants left out.
def HomologicalComplex.homologyIsoCoker The homology of a complex of topological modules, identified with the quotient of the cycles by the boundaries, carrying the quotient topology line 174 source
Source documentation
The homology of a complex of topological modules, identified with the quotient of the cycles by the boundaries, carrying the quotient topology.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, TopologicalSpace, ComplexShape, HomologicalComplex, TopModuleCat, Eq, ComplexShape.prev, CategoryTheory.Iso, HomologicalComplex.homology, HomologicalComplex.sc, TopModuleCat.coker, HomologicalComplex.X, HomologicalComplex.cycles, HomologicalComplex.toCycles
Proof uses: CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit, CategoryTheory.Limits.CokernelCofork.ofπ, HomologicalComplex.homologyπ, TopModuleCat.cokerπ, HomologicalComplex.homologyIsCokernel, TopModuleCat.isColimitCoker, CategoryTheory.Iso.refl, CategoryTheory.Arrow, CategoryTheory.Arrow.mk
14 instances, coercions and auxiliary constants left out.
```
noncomputable def homologyIsoCoker (i j : ι) (hij : c.prev j = i) :
    K.homology j ≅ TopModuleCat.coker (K.toCycles i j) :=
…
```