Documentation Verification Report

Abelian

📁 Source: Mathlib/Algebra/Category/FGModuleCat/Abelian.lean

Statistics

Metric	Count
Definitions `instAbelian`	1
Theorems `instIsIsoCoimageImageComparison`	1
Total	2

FGModuleCat

Definitions

Name	Category	Theorems
`instAbelian` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoCoimageImageComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `FGModuleCat` `CategoryTheory.ObjectProperty.FullSubcategory.category` `ModuleCat` `ModuleCat.moduleCategory` `ModuleCat.isFG` `CategoryTheory.Abelian.coimage` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Preadditive.fullSubcategory` `ModuleCat.instPreadditive` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Limits.hasKernels_of_hasEqualizers` `instHasLimitsOfShapeOfFinCategory` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.instFinCategoryWalkingParallelPair` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Limits.hasCokernels_of_hasCoequalizers` `instHasColimitsOfShapeOfFinCategory` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.ι` `CategoryTheory.Abelian.image` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Abelian.coimageImageComparison`	—	`CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Limits.hasKernels_of_hasEqualizers` `instHasLimitsOfShapeOfFinCategory` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Limits.hasCokernels_of_hasCoequalizers` `instHasColimitsOfShapeOfFinCategory` `CategoryTheory.IsIso.of_isIso_fac_right` `CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom` `CategoryTheory.Functor.preservesZeroMorphisms_of_full` `instFullModuleCatForget₂LinearMapIdCarrierObjIsFG` `CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit` `ModuleCat.HasColimit.instHasColimit` `AddCommGrpCat.hasColimit` `UnivLE.small` `univLE_of_max` `UnivLE.self` `ModuleCat.hasLimit` `small_subtype` `small_Pi` `CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Abelian.instIsIsoCoimageImageComparison` `CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison` `CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map`

---

← Back to Index