Documentation Verification Report

Homology

📁 Source: Mathlib/Algebra/Category/ModuleCat/Topology/Homology.lean

Statistics

Metric	Count
Definitions `coker`, `cokerπ`, `isColimitCoker`, `isLimitKer`, `ker`, `kerι`	6
Theorems `cokerπ_surjective`, `comp_cokerπ`, `hom_cokerπ`, `instCategoryWithHomology`, `instEpiCokerπ`, `instMonoKerι`, `kerι_apply`, `kerι_comp`	8
Total	14

TopModuleCat

Definitions

Name	Category	Theorems
`coker` 📖	CompOp	4 math math: `hom_cokerπ`, `comp_cokerπ`, `cokerπ_surjective`, `instEpiCokerπ`
`cokerπ` 📖	CompOp	4 math math: `hom_cokerπ`, `comp_cokerπ`, `cokerπ_surjective`, `instEpiCokerπ`
`isColimitCoker` 📖	CompOp	—
`isLimitKer` 📖	CompOp	—
`ker` 📖	CompOp	3 math math: `kerι_apply`, `instMonoKerι`, `kerι_comp`
`kerι` 📖	CompOp	3 math math: `kerι_apply`, `instMonoKerι`, `kerι_comp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cokerπ_surjective` 📖	mathematical	—	`ModuleCat.carrier` `toModuleCat` `coker` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `topologicalSpace` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `ContinuousLinearMap.funLike` `Hom.hom` `cokerπ`	—	`Submodule.mkQ_surjective`
`comp_cokerπ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `TopModuleCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `coker` `cokerπ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	—	`CategoryTheory.ConcreteCategory.ext` `ContinuousLinearMap.ext`
`hom_cokerπ` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `toModuleCat` `topologicalSpace` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `coker` `ModuleCat.isModule` `ContinuousLinearMap.funLike` `Hom.hom` `cokerπ` `LinearMap` `HasQuotient.Quotient` `Submodule` `Submodule.hasQuotient` `LinearMap.range` `ContinuousLinearMap.toLinearMap` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `LinearMap.instFunLike` `Submodule.mkQ`	—	—
`instCategoryWithHomology` 📖	mathematical	—	`CategoryTheory.CategoryWithHomology` `TopModuleCat` `instCategory` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	—	`CategoryTheory.ShortComplex.zero` `kerι_comp` `comp_cokerπ` `CategoryTheory.ConcreteCategory.isIso_iff_bijective` `ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier` `CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint` `instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap` `CategoryTheory.ShortComplex.LeftHomologyData.isPreservedBy_of_preserves` `CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf` `CategoryTheory.Functor.preservesHomologyOfExact` `CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits` `CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint` `CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits` `CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint` `instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap` `CategoryTheory.ShortComplex.RightHomologyData.isPreservedBy_of_preserves` `CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf` `CategoryTheory.ShortComplex.map_leftRightHomologyComparison'` `CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian` `Topology.IsEmbedding.of_comp` `ContinuousLinearMap.cont` `isEmbedding_of_isOpenQuotientMap_of_isInducing` `RingHomCompTriple.ids` `ContinuousLinearMap.coe_comp'` `hom_comp` `CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι` `Topology.IsInducing.subtypeVal` `IsOpenQuotientMap.isQuotientMap` `Submodule.isOpenQuotientMap_mkQ` `IsTopologicalAddGroup.toContinuousAdd` `Submodule.topologicalAddGroup` `instIsTopologicalAddGroupCarrier` `Subtype.val_injective` `Submodule.Quotient.eq` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `CategoryTheory.ConcreteCategory.congr_hom` `zero_add` `eq_sub_iff_add_eq` `Set.image_congr` `CategoryTheory.isIso_iff_of_reflects_iso` `instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier` `TopCat.isIso_iff_isHomeomorph` `isHomeomorph_iff_isEmbedding_surjective`
`instEpiCokerπ` 📖	mathematical	—	`CategoryTheory.Epi` `TopModuleCat` `instCategory` `coker` `cokerπ`	—	`CategoryTheory.ConcreteCategory.epi_of_surjective` `cokerπ_surjective`
`instMonoKerι` 📖	mathematical	—	`CategoryTheory.Mono` `TopModuleCat` `instCategory` `ker` `kerι`	—	`CategoryTheory.ConcreteCategory.mono_of_injective` `Subtype.val_injective`
`kerι_apply` 📖	mathematical	—	`DFunLike.coe` `ker` `CategoryTheory.ConcreteCategory.hom` `TopModuleCat` `instCategory` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `ModuleCat.carrier` `toModuleCat` `topologicalSpace` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `ContinuousLinearMap.funLike` `instConcreteCategoryContinuousLinearMapIdCarrier` `kerι` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.ker` `ContinuousLinearMap.toLinearMap` `Hom.hom`	—	—
`kerι_comp` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `TopModuleCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `ker` `kerι` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `instPreadditive`	—	`CategoryTheory.ConcreteCategory.ext` `ContinuousLinearMap.ext`

---

← Back to Index