Documentation Verification Report

Kernels

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean

Statistics

Metric	Count
Definitions `isColimitMapCoconeEquiv`, `map`, `mapIsColimit`, `isLimitMapConeEquiv`, `map`, `mapIsLimit`, `iso`, `iso`, `isColimitCoforkMapOfIsColimit'`, `isColimitMapCoconeCoforkEquiv'`, `isColimitOfHasCokernelOfPreservesColimit`, `isLimitForkMapOfIsLimit'`, `isLimitMapConeForkEquiv'`, `isLimitOfHasKernelOfPreservesLimit`	14
Theorems `map_condition`, `map_condition_assoc`, `map_π`, `map_condition`, `map_condition_assoc`, `map_ι`, `iso_inv`, `of_iso_comparison`, `π_iso_hom`, `π_iso_hom_assoc`, `iso_hom`, `iso_inv_ι`, `iso_inv_ι_assoc`, `of_iso_comparison`, `instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom`, `instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom`, `instIsIsoCokernelComparison`, `instIsIsoKernelComparison`, `kernel_map_comp_preserves_kernel_iso_inv`, `kernel_map_comp_preserves_kernel_iso_inv_assoc`, `preservesCokernel_zero`, `preservesCokernel_zero'`, `preservesKernel_zero`, `preservesKernel_zero'`, `preserves_cokernel_iso_comp_cokernel_map`, `preserves_cokernel_iso_comp_cokernel_map_assoc`	26
Total	40

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`isColimitCoforkMapOfIsColimit'` 📖	CompOp	—
`isColimitMapCoconeCoforkEquiv'` 📖	CompOp	—
`isColimitOfHasCokernelOfPreservesColimit` 📖	CompOp	—
`isLimitForkMapOfIsLimit'` 📖	CompOp	—
`isLimitMapConeForkEquiv'` 📖	CompOp	—
`isLimitOfHasKernelOfPreservesLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom` 📖	mathematical	—	`HasCokernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	—
`instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom` 📖	mathematical	—	`HasKernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map`	—	—
`instIsIsoCokernelComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `cokernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `cokernelComparison`	—	`PreservesCokernel.iso_inv` `CategoryTheory.Iso.isIso_inv`
`instIsIsoKernelComparison` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `kernel` `CategoryTheory.Functor.map` `kernelComparison`	—	`PreservesKernel.iso_hom` `CategoryTheory.Iso.isIso_hom`
`kernel_map_comp_preserves_kernel_iso_inv` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`kernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `kernel.map` `CategoryTheory.Iso.inv` `PreservesKernel.iso`	—	`CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Category.assoc` `PreservesKernel.iso_hom` `CategoryTheory.Iso.eq_inv_comp` `kernelComparison_comp_kernel_map`
`kernel_map_comp_preserves_kernel_iso_inv_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`kernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `kernel.map` `CategoryTheory.Iso.inv` `PreservesKernel.iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `kernel_map_comp_preserves_kernel_iso_inv`
`preservesCokernel_zero` 📖	mathematical	—	`PreservesColimit` `WalkingParallelPair` `walkingParallelPairHomCategory` `parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasZeroMorphisms.zero`	—	`CokernelCofork.IsColimit.isIso_π` `CategoryTheory.Functor.map_zero` `CategoryTheory.Category.id_comp`
`preservesCokernel_zero'` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasZeroMorphisms.zero`	`PreservesColimit` `WalkingParallelPair` `walkingParallelPairHomCategory` `parallelPair`	—	`preservesCokernel_zero`
`preservesKernel_zero` 📖	mathematical	—	`PreservesLimit` `WalkingParallelPair` `walkingParallelPairHomCategory` `parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasZeroMorphisms.zero`	—	`KernelFork.IsLimit.isIso_ι` `CategoryTheory.Functor.map_zero` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Functor.map_inv` `CategoryTheory.IsIso.inv_hom_id`
`preservesKernel_zero'` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HasZeroMorphisms.zero`	`PreservesLimit` `WalkingParallelPair` `walkingParallelPairHomCategory` `parallelPair`	—	`preservesKernel_zero`
`preserves_cokernel_iso_comp_cokernel_map` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.obj` `cokernel` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `PreservesCokernel.iso` `cokernel.map`	—	`CategoryTheory.Iso.comp_inv_eq` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.eq_inv_comp` `PreservesCokernel.iso_inv` `cokernel_map_comp_cokernelComparison`
`preserves_cokernel_iso_comp_cokernel_map_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	`CategoryTheory.Functor.obj` `cokernel` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `PreservesCokernel.iso` `cokernel.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `preserves_cokernel_iso_comp_cokernel_map`

CategoryTheory.Limits.CokernelCofork

Definitions

Name	Category	Theorems
`isColimitMapCoconeEquiv` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `map_π`
`mapIsColimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Cofork.π`	—	`CategoryTheory.Functor.map_comp` `condition` `CategoryTheory.Functor.map_zero`
`map_condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.Limits.Cofork.π`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_condition`
`map_π` 📖	mathematical	—	`CategoryTheory.Limits.Cofork.π` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `map` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.WalkingParallelPair.one` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cocone.pt`	—	—

CategoryTheory.Limits.KernelFork

Definitions

Name	Category	Theorems
`isLimitMapConeEquiv` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `map_ι`
`mapIsLimit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.WalkingParallelPair.zero` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Fork.ι`	—	`CategoryTheory.Functor.map_comp` `condition` `CategoryTheory.Functor.map_zero`
`map_condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero` `CategoryTheory.Limits.WalkingParallelPair.zero` `CategoryTheory.Functor.map` `CategoryTheory.Limits.Fork.ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `map_condition`
`map_ι` 📖	mathematical	—	`CategoryTheory.Limits.Fork.ι` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero` `map` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.parallelPair` `CategoryTheory.Limits.WalkingParallelPair.zero`	—	—

CategoryTheory.Limits.PreservesCokernel

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	8 math math: `π_iso_hom_assoc`, `iso_inv`, `CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map`, `CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom`, `π_iso_hom`, `CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc`, `CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom`, `CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.cokernel` `CategoryTheory.Functor.map` `iso` `CategoryTheory.Limits.cokernelComparison`	—	`CategoryTheory.cancel_epi` `CategoryTheory.Limits.coequalizer.π_epi` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv` `CategoryTheory.Limits.π_comp_cokernelComparison`
`of_iso_comparison` 📖	mathematical	—	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone` `CategoryTheory.Limits.cokernel.condition` `CategoryTheory.Limits.zero_comp`
`π_iso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.cokernel` `CategoryTheory.Functor.map` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom`
`π_iso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.cokernel` `CategoryTheory.Functor.map` `CategoryTheory.Limits.cokernel.π` `CategoryTheory.Iso.hom` `iso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `π_iso_hom`

CategoryTheory.Limits.PreservesKernel

Definitions

Name	Category	Theorems
`iso` 📖	CompOp	8 math math: `iso_inv_ι`, `CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv_assoc`, `iso_inv_ι_assoc`, `iso_hom`, `CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv`, `CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv`, `CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom`, `CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.Functor.obj` `CategoryTheory.Limits.kernel` `CategoryTheory.Functor.map` `iso` `CategoryTheory.Limits.kernelComparison`	—	`CategoryTheory.cancel_mono` `CategoryTheory.Limits.equalizer.ι_mono` `CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp` `CategoryTheory.Limits.kernelComparison_comp_ι`
`iso_inv_ι` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.kernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Limits.kernel.ι`	—	`CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp`
`iso_inv_ι_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.kernel` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `iso` `CategoryTheory.Limits.kernel.ι`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `iso_inv_ι`
`of_iso_comparison` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CategoryTheory.Limits.WalkingParallelPair` `CategoryTheory.Limits.walkingParallelPairHomCategory` `CategoryTheory.Limits.parallelPair` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone` `CategoryTheory.Limits.kernel.condition` `CategoryTheory.Limits.comp_zero`

---

← Back to Index