Documentation Verification Report

FunctorCategory

📁 Source: Mathlib/CategoryTheory/Abelian/FunctorCategory.lean

Statistics

Metric	Count
Definitions `coimageObjIso`, `imageObjIso`, `functorCategoryAbelian`	3
Theorems `coimageImageComparison_app`, `coimageImageComparison_app'`, `coimageObjIso_hom`, `coimageObjIso_inv`, `functor_category_isIso_coimageImageComparison`, `imageObjIso_hom`, `imageObjIso_inv`	7
Total	10

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
`functorCategoryAbelian` 📖	CompOp	3 math math: `HomologicalComplex.quasiIso_iff_evaluation`, `HomologicalComplex.quasiIsoAt_iff_evaluation`, `CategoryTheory.ShortComplex.quasiIso_iff_evaluation`

CategoryTheory.Abelian.FunctorCategory

Definitions

Name	Category	Theorems
`coimageObjIso` 📖	CompOp	4 math math: `coimageImageComparison_app'`, `coimageImageComparison_app`, `coimageObjIso_inv`, `coimageObjIso_hom`
`imageObjIso` 📖	CompOp	4 math math: `coimageImageComparison_app'`, `coimageImageComparison_app`, `imageObjIso_hom`, `imageObjIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coimageImageComparison_app` 📖	mathematical	—	`CategoryTheory.Abelian.coimageImageComparison` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Functor.obj` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.ι` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Abelian.coimage` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Abelian.image` `CategoryTheory.Iso.inv` `coimageObjIso` `CategoryTheory.Iso.hom` `imageObjIso`	—	`CategoryTheory.Limits.coequalizer.hom_ext` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Limits.equalizer.hom_ext` `CategoryTheory.Category.assoc` `CategoryTheory.Abelian.coimage_image_factorisation` `CategoryTheory.Category.id_comp` `CategoryTheory.Limits.cokernel.desc.congr_simp` `CategoryTheory.Limits.PreservesCokernel.iso_inv` `CategoryTheory.Limits.PreservesKernel.iso_hom` `CategoryTheory.Limits.cokernel.π_desc_assoc` `CategoryTheory.Limits.kernel.lift_ι` `CategoryTheory.Category.comp_id` `CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj` `CategoryTheory.Limits.kernelComparison_comp_ι` `CategoryTheory.Limits.π_comp_cokernelComparison_assoc`
`coimageImageComparison_app'` 📖	mathematical	—	`CategoryTheory.NatTrans.app` `CategoryTheory.Abelian.coimage` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.ι` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Abelian.image` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Abelian.coimageImageComparison` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CategoryTheory.Iso.hom` `coimageObjIso` `CategoryTheory.Iso.inv` `imageObjIso`	—	`CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `coimageImageComparison_app` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.hom_inv_id_assoc`
`coimageObjIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Abelian.coimage` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.ι` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `coimageObjIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.PreservesCokernel.iso` `CategoryTheory.evaluation` `CategoryTheory.Limits.cokernel.map` `CategoryTheory.Limits.kernelComparison` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Limits.PreservesKernel.iso` `CategoryTheory.Limits.PreservesKernel.iso_hom`	—	`CategoryTheory.Limits.PreservesKernel.iso_hom` `CategoryTheory.Limits.cokernel.map.congr_simp`
`coimageObjIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Abelian.coimage` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.ι` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `coimageObjIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.map` `CategoryTheory.Limits.PreservesKernel.iso` `CategoryTheory.evaluation` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Iso.refl` `CategoryTheory.Limits.cokernelComparison`	—	`CategoryTheory.Limits.PreservesCokernel.iso_inv`
`functor_category_isIso_coimageImageComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Abelian.coimage` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.ι` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Abelian.image` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Abelian.coimageImageComparison`	—	`CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `coimageImageComparison_app'` `CategoryTheory.IsIso.comp_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Abelian.instIsIsoCoimageImageComparison` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.NatIso.isIso_of_isIso_app`
`imageObjIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Abelian.image` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `imageObjIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernelComparison` `CategoryTheory.evaluation` `CategoryTheory.Limits.kernel.map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Limits.PreservesCokernel.iso`	—	`CategoryTheory.Limits.PreservesKernel.iso_hom`
`imageObjIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Abelian.image` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Limits.instHasZeroMorphismsFunctor` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Limits.functorCategoryHasColimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Abelian.hasCoequalizers` `CategoryTheory.Functor.flip` `CategoryTheory.Limits.functorCategoryHasLimit` `CategoryTheory.Limits.cokernel` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Abelian.hasEqualizers` `CategoryTheory.NatTrans.app` `CategoryTheory.Limits.HasCokernels.has_colimit` `CategoryTheory.Abelian.has_cokernels` `CategoryTheory.Limits.HasKernels.has_limit` `CategoryTheory.Abelian.has_kernels` `imageObjIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Limits.kernel` `CategoryTheory.Limits.kernel.map` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Limits.cokernelComparison` `CategoryTheory.evaluation` `CategoryTheory.Limits.PreservesCokernel.iso` `CategoryTheory.Iso.refl` `CategoryTheory.Limits.PreservesCokernel.iso_inv` `CategoryTheory.Limits.PreservesKernel.iso`	—	`CategoryTheory.Limits.PreservesCokernel.iso_inv` `CategoryTheory.Limits.kernel.map.congr_simp`

---

← Back to Index