Kernels

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

Statistics

Metric	Count
Definitions CokernelCofork, desc', ofEpiOfIsZero, ofId, ofπ, ofπ', isColimitOfIsColimitOfIff, isColimitOfIsColimitOfIff', mapIsoOfIsColimit, mapOfIsColimit, ofπ, HasCokernel, HasCokernels, HasKernel, HasKernels, cokernelIso, ofIso, ofIsoComp, isoKernel, ofCompIso, ofIso, KernelFork, lift', ofId, ofMonoOfIsZero, ofι, ofι', isLimitOfIsLimitOfIff, isLimitOfIsLimitOfIff', mapIsoOfIsLimit, mapOfIsLimit, ofι, coker, π, cokernel, cokernelIso, desc, desc', isColimitCoconeZeroCocone, map, mapIso, ofEpi, ofIsoComp, zeroCokernelCofork, π, cokernelCompIsIso, cokernelComparison, cokernelEpiComp, cokernelImageι, cokernelIsCokernel, cokernelIsoOfEq, cokernelZeroIsoTarget, compNatIso, isCokernelEpiComp, isCokernelOfComp, isColimitAux, isKernelCompMono, isKernelOfComp, isLimitAux, isoOfι, isoOfπ, ker, ι, kernel, isLimitConeZeroCone, isoKernel, lift', map, mapIso, ofCompIso, ofMono, zeroKernelFork, ι, kernelCompMono, kernelComparison, kernelFactorThruImage, kernelIsIsoComp, kernelIsKernel, kernelIsoOfEq, kernelZeroIsoSource, ofιCongr, ofπCongr, zeroCokernelOfZeroCancel, zeroKernelOfCancelZero	84
Theorems isIso_π, isZero_of_epi, condition, condition_assoc, mapIsoOfIsColimit_hom, mapIsoOfIsColimit_inv, π_eq_zero, π_mapOfIsColimit, π_mapOfIsColimit_assoc, π_ofπ, has_colimit, has_limit, isIso_ι, isZero_of_mono, app_one, condition, condition_assoc, mapIsoOfIsLimit_hom, mapIsoOfIsLimit_inv, mapOfIsLimit_ι, mapOfIsLimit_ι_assoc, ι_ofι, kernel_ι_comp, coequalizer_as_cokernel, condition, condition_assoc, π_app, coker_map, coker_obj, condition, condition_assoc, congr_hom, congr_inv, desc_epi, desc_zero, mapIso_hom, mapIso_inv, map_desc, map_id, map_zero, of_kernel_of_mono, π_desc, π_desc_assoc, π_of_epi, π_of_zero, π_zero_isIso, cokernelCompIsIso_hom, cokernelCompIsIso_inv, cokernelComparison_map_desc, cokernelComparison_map_desc_assoc, cokernelEpiComp_hom, cokernelEpiComp_inv, cokernelImageι_hom, cokernelImageι_inv, cokernelIsoOfEq_hom_comp_desc, cokernelIsoOfEq_hom_comp_desc_assoc, cokernelIsoOfEq_inv_comp_desc, cokernelIsoOfEq_inv_comp_desc_assoc, cokernelIsoOfEq_refl, cokernelIsoOfEq_trans, cokernelZeroIsoTarget_hom, cokernelZeroIsoTarget_inv, cokernel_map_comp_cokernelComparison, cokernel_map_comp_cokernelComparison_assoc, cokernel_not_iso_of_nonzero, cokernel_not_mono_of_nonzero, colimit_ι_zero_cokernel_desc, colimit_ι_zero_cokernel_desc_assoc, eq_zero_of_epi_kernel, eq_zero_of_mono_cokernel, equalizer_as_kernel, hasCokernel_comp_iso, hasCokernel_epi_comp, hasCokernels_of_hasCoequalizers, hasKernel_comp_mono, hasKernel_iso_comp, hasKernels_of_hasEqualizers, instIsIsoMapOfEpi, instIsIsoMapOfMono, isCokernelEpiComp_desc, isKernelCompMono_lift, isZero_cokernel_of_epi, isZero_kernel_of_mono, condition, condition_assoc, ι_app, ker_map, ker_obj, condition, condition_assoc, congr_hom, congr_inv, lift_map, lift_mono, lift_zero, lift_ι, lift_ι_assoc, mapIso_hom, mapIso_inv, map_id, map_zero, of_cokernel_of_epi, ι_of_mono, ι_of_zero, ι_zero_isIso, kernelCompMono_hom, kernelCompMono_inv, kernelComparison_comp_kernel_map, kernelComparison_comp_kernel_map_assoc, kernelComparison_comp_ι, kernelComparison_comp_ι_assoc, kernelFactorThruImage_hom_comp_ι, kernelFactorThruImage_hom_comp_ι_assoc, kernelFactorThruImage_inv_comp_ι, kernelFactorThruImage_inv_comp_ι_assoc, kernelIsIsoComp_hom, kernelIsIsoComp_inv, kernelIsoOfEq_hom_comp_ι, kernelIsoOfEq_hom_comp_ι_assoc, kernelIsoOfEq_inv_comp_ι, kernelIsoOfEq_inv_comp_ι_assoc, kernelIsoOfEq_refl, kernelIsoOfEq_trans, kernelZeroIsoSource_hom, kernelZeroIsoSource_inv, kernel_not_epi_of_nonzero, kernel_not_iso_of_nonzero, lift_comp_kernelIsoOfEq_hom, lift_comp_kernelIsoOfEq_hom_assoc, lift_comp_kernelIsoOfEq_inv, lift_comp_kernelIsoOfEq_inv_assoc, map_lift_kernelComparison, map_lift_kernelComparison_assoc, π_comp_cokernelComparison, π_comp_cokernelComparison_assoc, π_comp_cokernelIsoOfEq_hom, π_comp_cokernelIsoOfEq_hom_assoc, π_comp_cokernelIsoOfEq_inv, π_comp_cokernelIsoOfEq_inv_assoc	139
Total	223

CategoryTheory.Limits

Definitions

Name	Category	Theorems
CokernelCofork 📖	CompOp	—
HasCokernel 📖	MathDef	11 math math: instHasCokernelFromSubtype, HasCokernels.has_colimit, instHasCokernelInr, instHasCokernelι, hasCokernel_comp_iso, CategoryTheory.Preadditive.hasCokernel_of_hasCoequalizer, CategoryTheory.ShortComplex.HasLeftHomology.hasCokernel, instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom, CategoryTheory.ShortComplex.HasRightHomology.hasCokernel, hasCokernel_epi_comp, instHasCokernelInl
HasCokernels 📖	CompData	7 math math: CategoryTheory.NonPreadditiveAbelian.has_cokernels, ModuleCat.hasCokernels_moduleCat, CategoryTheory.AbelianOfAdjunction.hasCokernels, CategoryTheory.Abelian.has_cokernels, SemiNormedGrp.instHasCokernels, SemiNormedGrp₁.instHasCokernels, hasCokernels_of_hasCoequalizers
HasKernel 📖	MathDef	12 math math: CategoryTheory.Preadditive.hasKernel_of_hasEqualizer, instHasKernelSnd, instHasKernelFst, CategoryTheory.ShortComplex.HasLeftHomology.hasKernel, CategoryTheory.ShortComplex.HasRightHomology.hasKernel, CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels, HasKernels.has_limit, instHasKernelToSubtype, instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom, instHasKernelπ, hasKernel_iso_comp, hasKernel_comp_mono
HasKernels 📖	CompData	6 math math: CategoryTheory.NonPreadditiveAbelian.has_kernels, hasKernels_of_hasEqualizers, CategoryTheory.AbelianOfAdjunction.hasKernels, FDRep.instHasKernels, ModuleCat.hasKernels_moduleCat, CategoryTheory.Abelian.has_kernels
KernelFork 📖	CompOp	—
coker 📖	CompOp	5 math math: coker.π_app, coker_map, coker.condition_assoc, coker_obj, coker.condition
cokernel 📖	CompOp	176 math math: cokernelBiproductιIso_hom, CategoryTheory.kernelUnopOp_inv, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_H, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, ModuleCat.cokernel_π_ext, cokernelImageι_inv, cokernel.map_zero, isIso_cokernel_map_of_isPushout, imageToKernel_unop, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, cokernelCompIsIso_hom, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero, π_comp_cokernelIsoOfEq_hom_assoc, CategoryTheory.kernelCokernelCompSequence.inl_π_assoc, CategoryTheory.cokernelUnopUnop_inv, PreservesCokernel.π_iso_hom_assoc, CategoryTheory.kernelOpUnop_hom, cokernel.desc_epi, PreservesCokernel.iso_inv, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, imageToKernel_op, coker_map, CategoryTheory.Abelian.instEpiFactorThruImage, CategoryTheory.Abelian.tfae_epi, CategoryTheory.cokernelOpOp_hom, cokernel.map_desc, CategoryTheory.kernelCokernelCompSequence.inr_π_assoc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, cokernel.π_desc_assoc, cokernel.π_zero_isIso, cokernel_not_mono_of_nonzero, CategoryTheory.Abelian.im_map, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply, CategoryTheory.kernelUnopUnop_inv, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.Abelian.image_ι_comp_eq_zero, CategoryTheory.kernelOpUnop_inv, ModuleCat.cokernel_π_imageSubobject_ext, cokernel.condition, CategoryTheory.ShortComplex.Exact.mono_cokernelDesc, cokernel.map_id, CategoryTheory.ShortComplex.opcyclesIsoCokernel_inv, CategoryTheory.ShortComplex.exact_cokernel, CategoryTheory.cokernelUnopOp_hom, cokernelBiprodInlIso_inv, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q, CategoryTheory.NonPreadditiveAbelian.instEpiFactorThruImage, CategoryTheory.cokernel.π_unop, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, CategoryTheory.Abelian.mono_cokernel_map_of_isPullback, cokernel.mapIso_hom, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m, coker_obj, cokernelBiprodInrIso_inv, cokernelIsoOfEq_refl, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂, cokernel.π_of_zero, CategoryTheory.Abelian.imageIsoImage_inv, CategoryTheory.kernelUnopOp_hom, CategoryTheory.cokernel.π_op, π_comp_cokernelIsoOfEq_inv_assoc, CategoryTheory.instIsIsoIndCoimageImageComparison, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, CategoryTheory.NonPreadditiveAbelian.epi_r, CategoryTheory.kernelCokernelCompSequence.inr_π, CategoryTheory.NonPreadditiveAbelian.isIso_r, cokernel.desc_zero, CategoryTheory.cokernelOpUnop_inv, CategoryTheory.Preadditive.epi_iff_isZero_cokernel, cokernelBiprodInrIso_hom, CategoryTheory.kernel.ι_unop, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_H, CategoryTheory.ShortComplex.opcyclesIsoCokernel_hom, cokernel.condition_assoc, cokernelBiproductιIso_inv, cokernelBiproductFromSubtypeIso_hom, CategoryTheory.kernelCokernelCompSequence.instEpiπ, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₃, isZero_cokernel_of_epi, CategoryTheory.ObjectProperty.epiModSerre_iff, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, instIsIsoCokernelComparison, preserves_cokernel_iso_comp_cokernel_map, π_comp_cokernelComparison_assoc, CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_H, cokernel.π_desc, cokernel_map_comp_cokernelComparison, cokernelComparison_map_desc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', cokernelIsoOfEq_hom_comp_desc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, SemiNormedGrp.explicitCokernelIso_hom_π, cokernelEpiComp_inv, CategoryTheory.kernelUnopUnop_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, CategoryTheory.ShortComplex.HasRightHomology.hasKernel, cokernelIsoOfEq_inv_comp_desc, CategoryTheory.kernelCokernelCompSequence.δ_fac, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_ι, cokernelIsoOfEq_trans, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc, CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc, kernel.of_cokernel_of_epi, CategoryTheory.Abelian.coimageImageComparisonFunctor_map, cokernelIsoOfEq_hom_comp_desc_assoc, CategoryTheory.cokernelUnopUnop_hom, cokernel.congr_inv, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, π_comp_cokernelComparison, CategoryTheory.cokernelOpUnop_hom, CategoryTheory.kernel.ι_op, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_Q, CategoryTheory.kernelCokernelCompSequence.φ_π, CategoryTheory.NonPreadditiveAbelian.mono_r, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, cokernelBiprodInlIso_hom, CategoryTheory.Abelian.image.ι_comp_eq_zero, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e, cokernel_map_comp_cokernelComparison_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, CategoryTheory.ShortComplex.cokernelSequence_X₃, cokernelIsoOfEq_inv_comp_desc_assoc, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁, CategoryTheory.kernelOpOp_inv, PreservesCokernel.π_iso_hom, CategoryTheory.NonPreadditiveAbelian.diag_σ_assoc, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, cokernel.π_of_epi, SemiNormedGrp.explicitCokernelIso_hom_desc, cokernel.π_desc_apply, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁, CategoryTheory.Abelian.isIso_factorThruImage, cokernelCompIsIso_inv, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage, CategoryTheory.cokernelUnopOp_inv, SemiNormedGrp.explicitCokernelIso_inv_π, CategoryTheory.kernelOpOp_hom, CategoryTheory.NonPreadditiveAbelian.lift_σ_assoc, π_comp_cokernelIsoOfEq_inv, preserves_cokernel_iso_comp_cokernel_map_assoc, cokernelZeroIsoTarget_hom, CategoryTheory.kernelCokernelCompSequence.inl_π, cokernelComparison_map_desc_assoc, CategoryTheory.Abelian.instIsIsoCoimageImageComparison, π_comp_cokernelIsoOfEq_hom, cokernelZeroIsoTarget_inv, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, cokernelBiproductFromSubtypeIso_inv, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac, cokernelOrderHom_coe, instIsIsoMapOfEpi, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, cokernel.mapIso_inv, cokernelEpiComp_hom, CategoryTheory.cokernel_zero_of_nonzero_to_simple, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₂, CategoryTheory.cokernelOpOp_inv, cokernelImageι_hom, cokernel.congr_hom, cokernel.of_kernel_of_mono, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc, CategoryTheory.kernelCokernelCompSequence.φ_π_assoc, FGModuleCat.instIsIsoCoimageImageComparison, cokernel.condition_apply
cokernelCompIsIso 📖	CompOp	2 math math: cokernelCompIsIso_hom, cokernelCompIsIso_inv
cokernelComparison 📖	CompOp	10 math math: PreservesCokernel.iso_inv, instIsIsoCokernelComparison, π_comp_cokernelComparison_assoc, cokernel_map_comp_cokernelComparison, cokernelComparison_map_desc, π_comp_cokernelComparison, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, cokernel_map_comp_cokernelComparison_assoc, cokernelComparison_map_desc_assoc, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv
cokernelEpiComp 📖	CompOp	2 math math: cokernelEpiComp_inv, cokernelEpiComp_hom
cokernelImageι 📖	CompOp	2 math math: cokernelImageι_inv, cokernelImageι_hom
cokernelIsCokernel 📖	CompOp	—
cokernelIsoOfEq 📖	CompOp	10 math math: π_comp_cokernelIsoOfEq_hom_assoc, cokernelIsoOfEq_refl, π_comp_cokernelIsoOfEq_inv_assoc, cokernelIsoOfEq_hom_comp_desc, cokernelIsoOfEq_inv_comp_desc, cokernelIsoOfEq_trans, cokernelIsoOfEq_hom_comp_desc_assoc, cokernelIsoOfEq_inv_comp_desc_assoc, π_comp_cokernelIsoOfEq_inv, π_comp_cokernelIsoOfEq_hom
cokernelZeroIsoTarget 📖	CompOp	2 math math: cokernelZeroIsoTarget_hom, cokernelZeroIsoTarget_inv
compNatIso 📖	CompOp	—
isCokernelEpiComp 📖	CompOp	1 math math: isCokernelEpiComp_desc
isCokernelOfComp 📖	CompOp	—
isColimitAux 📖	CompOp	—
isKernelCompMono 📖	CompOp	1 math math: isKernelCompMono_lift
isKernelOfComp 📖	CompOp	—
isLimitAux 📖	CompOp	—
isoOfι 📖	CompOp	—
isoOfπ 📖	CompOp	—
ker 📖	CompOp	5 math math: ker.ι_app, ker_obj, ker.condition, ker.condition_assoc, ker_map
kernel 📖	CompOp	204 math math: CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂, CategoryTheory.kernelUnopOp_inv, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁, kernelIsoOfEq_trans, CategoryTheory.ShortComplex.Exact.epi_kernelLift, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_H, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, imageToKernel_unop, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂, kernelBiprodSndIso_hom, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, imageToKernel'_kernelSubobjectIso, CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_K, kernelSubobject_arrow'_apply, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', PreservesKernel.iso_inv_ι, kernel_not_epi_of_nonzero, CategoryTheory.cokernelUnopUnop_inv, CategoryTheory.kernelOpUnop_hom, isZero_kernel_of_mono, kernel.condition_apply, kernel.congr_inv, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, imageToKernel_op, kernelBiprodFstIso_hom, kernelFactorThruImage_hom_comp_ι_assoc, CategoryTheory.Abelian.coim_map, CategoryTheory.kernel_zero_of_nonzero_from_simple, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage, kernelBiproductπIso_hom, kernelCompMono_hom, CategoryTheory.cokernelOpOp_hom, kernel_map_comp_preserves_kernel_iso_inv_assoc, kernelSubobject_arrow_assoc, CategoryTheory.kernelCokernelCompSequence.ι_φ, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, kernelIsoOfEq_hom_comp_ι, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, kernelComparison_comp_ι, instIsIsoMapOfMono, CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc, lift_comp_kernelIsoOfEq_hom_assoc, kernel.mapIso_hom, kernel.lift_ι_apply, PreservesKernel.iso_inv_ι_assoc, CategoryTheory.kernelUnopUnop_inv, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.kernelCokernelCompSequence.ι_fst, CategoryTheory.kernelOpUnop_inv, kernelBiprodFstIso_inv, kernelBiproductToSubtypeIso_hom, kernelComparison_comp_kernel_map_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, lift_comp_kernelIsoOfEq_hom, kernelIsIsoComp_hom, CategoryTheory.cokernelUnopOp_hom, ker_obj, CategoryTheory.Abelian.instMonoFactorThruCoimage, kernel.map_zero, kernel.ι_of_mono, kernelIsIsoComp_inv, CategoryTheory.cokernel.π_unop, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, kernelSubobjectIso_comp_kernel_map, CategoryTheory.Abelian.epi_kernel_map_of_isPushout, CategoryTheory.ShortComplex.cyclesIsoKernel_hom, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, CategoryTheory.ShortComplex.kernelSequence_X₁, kernel.lift_mono, kernel.lift_map, kernel.lift_ι_assoc, kernelComparison_comp_ι_assoc, CategoryTheory.kernelCokernelCompSequence.ι_snd, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, CategoryTheory.kernelUnopOp_hom, CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc, CategoryTheory.ShortComplex.exact_kernel, CategoryTheory.cokernel.π_op, CategoryTheory.instIsIsoIndCoimageImageComparison, kernel.ι_of_zero, CategoryTheory.cokernelOpUnop_inv, kernelOrderHom_coe, instIsIsoKernelComparison, kernelIsoOfEq_hom_comp_ι_assoc, kernel.condition, CategoryTheory.kernel.ι_unop, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_H, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv, CategoryTheory.ObjectProperty.monoModSerre_iff, kernelBiproductπIso_inv, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, kernelSubobjectIso_comp_kernel_map_assoc, AddCommGrpCat.kernelIsoKer_inv_comp_ι, map_lift_kernelComparison, kernelSubobject_arrow, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, SheafOfModules.Presentation.map_relations_I, kernelComparison_comp_kernel_map, imageSubobjectIso_imageToKernel', CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', ModuleCat.kernelIsoKer_hom_ker_subtype, SheafOfModules.Presentation.mapRelations_mapGenerators, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, kernel.ι_zero_isIso, SheafOfModules.relationsOfIsCokernelFree_I, PreservesKernel.iso_hom, CategoryTheory.kernelUnopUnop_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, kernel.map_id, kernel_map_comp_preserves_kernel_iso_inv, CategoryTheory.kernelCokernelCompSequence.δ_fac, CategoryTheory.Preadditive.mono_iff_isZero_kernel, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, kernelFactorThruImage_inv_comp_ι, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc, kernel.of_cokernel_of_epi, kernel_map_comp_kernelSubobjectIso_inv, CategoryTheory.Abelian.coimageImageComparisonFunctor_map, SheafOfModules.Presentation.of_isIso_relations, CategoryTheory.cokernelUnopUnop_hom, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, CategoryTheory.Abelian.coimage.comp_π_eq_zero, map_lift_kernelComparison_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁, kernelSubobject_arrow'_assoc, CategoryTheory.ShortComplex.HasLeftHomology.hasCokernel, kernelZeroIsoSource_hom, CategoryTheory.Abelian.coimageIsoImage'_hom, CategoryTheory.cokernelOpUnop_hom, MonoFactorisation.kernel_ι_comp, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃, CategoryTheory.kernel.ι_op, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_π, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, kernel.condition_assoc, kernelIsoOfEq_inv_comp_ι, CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, kernelIsoOfEq_inv_comp_ι_assoc, kernelZeroIsoSource_inv, kernelBiprodSndIso_inv, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, SheafOfModules.relationsOfIsCokernelFree_s, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, kernel.lift_ι, CategoryTheory.kernelOpOp_inv, CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_H, CategoryTheory.Abelian.tfae_mono, CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, kernel_map_comp_kernelSubobjectIso_inv_assoc, kernelSubobject_arrow_apply, SheafOfModules.Presentation.IsFinite.finite_relations, kernelFactorThruImage_hom_comp_ι, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, CategoryTheory.cokernelUnopOp_inv, kernelIsoOfEq_refl, isIso_kernel_map_of_isPullback, kernelFactorThruImage_inv_comp_ι_assoc, CategoryTheory.kernelOpOp_hom, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, kernel.lift_zero, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel', CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃, CategoryTheory.Abelian.instIsIsoCoimageImageComparison, factorThruKernelSubobject_comp_kernelSubobjectIso, kernel.congr_hom, lift_comp_kernelIsoOfEq_inv, ModuleCat.kernelIsoKer_inv_kernel_ι, kernel.mapIso_inv, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac, CategoryTheory.ShortComplex.cyclesIsoKernel_inv, kernelCompMono_inv, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel', CategoryTheory.Abelian.isIso_factorThruCoimage, lift_comp_kernelIsoOfEq_inv_assoc, CategoryTheory.Abelian.comp_coimage_π_eq_zero, kernelBiproductToSubtypeIso_inv, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, kernelSubobject_arrow', CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f, CategoryTheory.kernelCokernelCompSequence.instMonoι, CategoryTheory.cokernelOpOp_inv, CategoryTheory.kernelCokernelCompSequence.ι_φ_assoc, cokernel.of_kernel_of_mono, ker_map, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc, FGModuleCat.instIsIsoCoimageImageComparison
kernelCompMono 📖	CompOp	3 math math: kernelCompMono_hom, SheafOfModules.Presentation.of_isIso_relations, kernelCompMono_inv
kernelComparison 📖	CompOp	10 math math: kernelComparison_comp_ι, kernelComparison_comp_kernel_map_assoc, kernelComparison_comp_ι_assoc, instIsIsoKernelComparison, map_lift_kernelComparison, kernelComparison_comp_kernel_map, PreservesKernel.iso_hom, map_lift_kernelComparison_assoc, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom
kernelFactorThruImage 📖	CompOp	4 math math: kernelFactorThruImage_hom_comp_ι_assoc, kernelFactorThruImage_inv_comp_ι, kernelFactorThruImage_hom_comp_ι, kernelFactorThruImage_inv_comp_ι_assoc
kernelIsIsoComp 📖	CompOp	2 math math: kernelIsIsoComp_hom, kernelIsIsoComp_inv
kernelIsKernel 📖	CompOp	—
kernelIsoOfEq 📖	CompOp	10 math math: kernelIsoOfEq_trans, kernelIsoOfEq_hom_comp_ι, lift_comp_kernelIsoOfEq_hom_assoc, lift_comp_kernelIsoOfEq_hom, kernelIsoOfEq_hom_comp_ι_assoc, kernelIsoOfEq_inv_comp_ι, kernelIsoOfEq_inv_comp_ι_assoc, kernelIsoOfEq_refl, lift_comp_kernelIsoOfEq_inv, lift_comp_kernelIsoOfEq_inv_assoc
kernelZeroIsoSource 📖	CompOp	2 math math: kernelZeroIsoSource_hom, kernelZeroIsoSource_inv
ofιCongr 📖	CompOp	—
ofπCongr 📖	CompOp	—
zeroCokernelOfZeroCancel 📖	CompOp	—
zeroKernelOfCancelZero 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coequalizer_as_cokernel 📖	mathematical	—	coequalizer.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero cokernel.π	—	—
coker_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow coker cokernel.desc CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.right cokernel.π	—	—
coker_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow coker cokernel CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
cokernelCompIsIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasCokernel_comp_iso cokernelCompIsIso cokernel.desc CategoryTheory.inv cokernel.π	—	hasCokernel_comp_iso
cokernelCompIsIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasCokernel_comp_iso cokernelCompIsIso cokernel.desc cokernel.π	—	hasCokernel_comp_iso
cokernelComparison_map_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	cokernel CategoryTheory.Functor.obj CategoryTheory.Functor.map cokernelComparison cokernel.desc	—	coequalizer.hom_ext π_comp_cokernelComparison_assoc CategoryTheory.Functor.map_comp cokernel.π_desc
cokernelComparison_map_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	cokernel CategoryTheory.Functor.obj CategoryTheory.Functor.map cokernelComparison cokernel.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokernelComparison_map_desc
cokernelEpiComp_hom 📖	mathematical	—	CategoryTheory.Iso.hom cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasCokernel_epi_comp cokernelEpiComp cokernel.desc cokernel.π	—	hasCokernel_epi_comp
cokernelEpiComp_inv 📖	mathematical	—	CategoryTheory.Iso.inv cokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasCokernel_epi_comp cokernelEpiComp cokernel.desc cokernel.π	—	hasCokernel_epi_comp
cokernelImageι_hom 📖	mathematical	—	CategoryTheory.Iso.hom cokernel image image.ι cokernelImageι cokernel.desc cokernel.π	—	—
cokernelImageι_inv 📖	mathematical	—	CategoryTheory.Iso.inv cokernel image image.ι cokernelImageι cokernel.desc cokernel.π	—	—
cokernelIsoOfEq_hom_comp_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	cokernel CategoryTheory.Iso.hom cokernelIsoOfEq cokernel.desc	—	cokernelIsoOfEq_refl CategoryTheory.Category.id_comp
cokernelIsoOfEq_hom_comp_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	cokernel CategoryTheory.Iso.hom cokernelIsoOfEq cokernel.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokernelIsoOfEq_hom_comp_desc
cokernelIsoOfEq_inv_comp_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	cokernel CategoryTheory.Iso.inv cokernelIsoOfEq cokernel.desc	—	cokernelIsoOfEq_refl CategoryTheory.Category.id_comp
cokernelIsoOfEq_inv_comp_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	cokernel CategoryTheory.Iso.inv cokernelIsoOfEq cokernel.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokernelIsoOfEq_inv_comp_desc
cokernelIsoOfEq_refl 📖	mathematical	—	cokernelIsoOfEq CategoryTheory.Iso.refl cokernel	—	CategoryTheory.Iso.ext coequalizer.hom_ext HasColimit.isoOfNatIso_ι_hom CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
cokernelIsoOfEq_trans 📖	mathematical	—	CategoryTheory.Iso.trans cokernel cokernelIsoOfEq Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	cokernelIsoOfEq_refl CategoryTheory.Iso.refl_trans
cokernelZeroIsoTarget_hom 📖	mathematical	—	CategoryTheory.Iso.hom cokernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasCoequalizer_of_self cokernelZeroIsoTarget cokernel.desc CategoryTheory.CategoryStruct.id	—	coequalizer.hom_ext hasCoequalizer_of_self coequalizer.isoTargetOfSelf_hom colimit.ι_desc cokernel.π_desc
cokernelZeroIsoTarget_inv 📖	mathematical	—	CategoryTheory.Iso.inv cokernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasCoequalizer_of_self cokernelZeroIsoTarget cokernel.π	—	hasCoequalizer_of_self
cokernel_map_comp_cokernelComparison 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	cokernel CategoryTheory.Functor.obj CategoryTheory.Functor.map cokernel.map cokernelComparison	—	cokernel.map_desc CategoryTheory.Functor.map_comp cokernel.condition CategoryTheory.Functor.map_zero CategoryTheory.Functor.congr_map cokernel.π_desc
cokernel_map_comp_cokernelComparison_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	cokernel CategoryTheory.Functor.obj CategoryTheory.Functor.map cokernel.map cokernelComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokernel_map_comp_cokernelComparison
cokernel_not_iso_of_nonzero 📖	—	—	—	—	cokernel_not_mono_of_nonzero CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso
cokernel_not_mono_of_nonzero 📖	mathematical	—	CategoryTheory.Mono cokernel cokernel.π	—	eq_zero_of_mono_cokernel
colimit_ι_zero_cokernel_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj WalkingParallelPair walkingParallelPairHomCategory parallelPair WalkingParallelPair.zero colimit colimit.ι cokernel.desc	—	colimit.w cokernel.condition zero_comp
colimit_ι_zero_cokernel_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj WalkingParallelPair walkingParallelPairHomCategory parallelPair WalkingParallelPair.zero colimit colimit.ι cokernel.desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimit_ι_zero_cokernel_desc
eq_zero_of_epi_kernel 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero	—	CategoryTheory.cancel_epi kernel.condition comp_zero
eq_zero_of_mono_cokernel 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero	—	CategoryTheory.cancel_mono cokernel.condition zero_comp
equalizer_as_kernel 📖	mathematical	—	equalizer.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero kernel.ι	—	—
hasCokernel_comp_iso 📖	mathematical	—	HasCokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc CategoryTheory.IsIso.hom_inv_id_assoc cokernel.condition CokernelCofork.condition cokernel.π_desc CategoryTheory.IsIso.inv_hom_id_assoc cokernel.desc.congr_simp coequalizer.hom_ext
hasCokernel_epi_comp 📖	mathematical	—	HasCokernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
hasCokernels_of_hasCoequalizers 📖	mathematical	—	HasCokernels	—	hasColimitOfHasColimitsOfShape
hasKernel_comp_mono 📖	mathematical	—	HasKernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
hasKernel_iso_comp 📖	mathematical	—	HasKernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id_assoc kernel.condition KernelFork.condition kernel.lift_ι_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id kernel.lift.congr_simp equalizer.hom_ext CategoryTheory.IsIso.inv_hom_id kernel.lift_ι
hasKernels_of_hasEqualizers 📖	mathematical	—	HasKernels	—	hasLimitOfHasLimitsOfShape
instIsIsoMapOfEpi 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso cokernel cokernel.map	—	CategoryTheory.cancel_epi CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.IsIso.hom_inv_id_assoc cokernel.condition comp_zero coequalizer.hom_ext cokernel.π_desc_assoc cokernel.π_desc CategoryTheory.Category.comp_id CategoryTheory.IsIso.inv_hom_id_assoc
instIsIsoMapOfMono 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.IsIso kernel kernel.map	—	CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.IsIso.inv_hom_id_assoc kernel.condition zero_comp equalizer.hom_ext kernel.lift_ι kernel.lift_ι_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.IsIso.inv_hom_id
isCokernelEpiComp_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	IsColimit.desc WalkingParallelPair walkingParallelPairHomCategory parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero CokernelCofork.ofπ CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cocone.pt WalkingParallelPair.one Cofork.π isCokernelEpiComp Cofork.ofπ	—	—
isKernelCompMono_lift 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	IsLimit.lift WalkingParallelPair walkingParallelPairHomCategory parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero KernelFork.ofι CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const Cone.pt WalkingParallelPair.zero Fork.ι isKernelCompMono Fork.ofι	—	—
isZero_cokernel_of_epi 📖	mathematical	—	IsZero cokernel	—	CokernelCofork.IsColimit.isZero_of_epi cokernel.condition
isZero_kernel_of_mono 📖	mathematical	—	IsZero kernel	—	KernelFork.IsLimit.isZero_of_mono kernel.condition
ker_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow ker kernel.lift CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel.ι CategoryTheory.CommaMorphism.left	—	—
ker_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow ker kernel CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
kernelCompMono_hom 📖	mathematical	—	CategoryTheory.Iso.hom kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasKernel_comp_mono kernelCompMono kernel.lift kernel.ι	—	hasKernel_comp_mono
kernelCompMono_inv 📖	mathematical	—	CategoryTheory.Iso.inv kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasKernel_comp_mono kernelCompMono kernel.lift kernel.ι	—	hasKernel_comp_mono
kernelComparison_comp_kernel_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj kernel CategoryTheory.Functor.map kernelComparison kernel.map	—	kernel.lift_map CategoryTheory.Functor.map_comp kernel.condition CategoryTheory.Functor.map_zero CategoryTheory.Functor.congr_map kernel.lift_ι
kernelComparison_comp_kernel_map_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Functor.obj kernel CategoryTheory.Functor.map kernelComparison kernel.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelComparison_comp_kernel_map
kernelComparison_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj kernel CategoryTheory.Functor.map kernelComparison kernel.ι	—	kernel.lift_ι
kernelComparison_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj kernel CategoryTheory.Functor.map kernelComparison kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelComparison_comp_ι
kernelFactorThruImage_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel image factorThruImage CategoryTheory.Iso.hom kernelFactorThruImage kernel.ι	—	hasKernel_comp_mono instMonoι CategoryTheory.Category.assoc kernel.lift_ι
kernelFactorThruImage_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel image factorThruImage CategoryTheory.Iso.hom kernelFactorThruImage kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelFactorThruImage_hom_comp_ι
kernelFactorThruImage_inv_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel image factorThruImage CategoryTheory.Iso.inv kernelFactorThruImage kernel.ι	—	hasKernel_comp_mono instMonoι CategoryTheory.Category.assoc kernel.lift_ι
kernelFactorThruImage_inv_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel image factorThruImage CategoryTheory.Iso.inv kernelFactorThruImage kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelFactorThruImage_inv_comp_ι
kernelIsIsoComp_hom 📖	mathematical	—	CategoryTheory.Iso.hom kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasKernel_iso_comp kernelIsIsoComp kernel.lift kernel.ι	—	hasKernel_iso_comp
kernelIsIsoComp_inv 📖	mathematical	—	CategoryTheory.Iso.inv kernel CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct hasKernel_iso_comp kernelIsIsoComp kernel.lift kernel.ι CategoryTheory.inv	—	hasKernel_iso_comp
kernelIsoOfEq_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Iso.hom kernelIsoOfEq kernel.ι	—	kernelIsoOfEq_refl CategoryTheory.Category.id_comp
kernelIsoOfEq_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Iso.hom kernelIsoOfEq kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelIsoOfEq_hom_comp_ι
kernelIsoOfEq_inv_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Iso.inv kernelIsoOfEq kernel.ι	—	kernelIsoOfEq_refl CategoryTheory.Category.id_comp
kernelIsoOfEq_inv_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct kernel CategoryTheory.Iso.inv kernelIsoOfEq kernel.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' kernelIsoOfEq_inv_comp_ι
kernelIsoOfEq_refl 📖	mathematical	—	kernelIsoOfEq CategoryTheory.Iso.refl kernel	—	CategoryTheory.Iso.ext equalizer.hom_ext HasLimit.isoOfNatIso_hom_π CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
kernelIsoOfEq_trans 📖	mathematical	—	CategoryTheory.Iso.trans kernel kernelIsoOfEq Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	kernelIsoOfEq_refl CategoryTheory.Iso.refl_trans
kernelZeroIsoSource_hom 📖	mathematical	—	CategoryTheory.Iso.hom kernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasEqualizer_of_self kernelZeroIsoSource kernel.ι	—	hasEqualizer_of_self
kernelZeroIsoSource_inv 📖	mathematical	—	CategoryTheory.Iso.inv kernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HasZeroMorphisms.zero hasEqualizer_of_self kernelZeroIsoSource kernel.lift CategoryTheory.CategoryStruct.id	—	equalizer.hom_ext hasEqualizer_of_self equalizer.isoSourceOfSelf_inv limit.lift_π kernel.lift_ι
kernel_not_epi_of_nonzero 📖	mathematical	—	CategoryTheory.Epi kernel kernel.ι	—	eq_zero_of_epi_kernel
kernel_not_iso_of_nonzero 📖	—	—	—	—	kernel_not_epi_of_nonzero CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso
lift_comp_kernelIsoOfEq_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	kernel kernel.lift CategoryTheory.Iso.hom kernelIsoOfEq	—	kernelIsoOfEq_refl CategoryTheory.Category.comp_id
lift_comp_kernelIsoOfEq_hom_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	kernel kernel.lift CategoryTheory.Iso.hom kernelIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_kernelIsoOfEq_hom
lift_comp_kernelIsoOfEq_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	kernel kernel.lift CategoryTheory.Iso.inv kernelIsoOfEq	—	kernelIsoOfEq_refl CategoryTheory.Category.comp_id
lift_comp_kernelIsoOfEq_inv_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	kernel kernel.lift CategoryTheory.Iso.inv kernelIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_comp_kernelIsoOfEq_inv
map_lift_kernelComparison 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj kernel CategoryTheory.Functor.map kernel.lift kernelComparison	—	equalizer.hom_ext CategoryTheory.Category.assoc kernelComparison_comp_ι CategoryTheory.Functor.map_comp kernel.lift_ι
map_lift_kernelComparison_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HasZeroMorphisms.zero	CategoryTheory.Functor.obj kernel CategoryTheory.Functor.map kernel.lift kernelComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_lift_kernelComparison
π_comp_cokernelComparison 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj cokernel CategoryTheory.Functor.map cokernel.π cokernelComparison	—	cokernel.π_desc
π_comp_cokernelComparison_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj cokernel CategoryTheory.Functor.map cokernel.π cokernelComparison	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_cokernelComparison
π_comp_cokernelIsoOfEq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cokernel cokernel.π CategoryTheory.Iso.hom cokernelIsoOfEq	—	cokernelIsoOfEq_refl CategoryTheory.Category.comp_id
π_comp_cokernelIsoOfEq_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cokernel cokernel.π CategoryTheory.Iso.hom cokernelIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_cokernelIsoOfEq_hom
π_comp_cokernelIsoOfEq_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cokernel cokernel.π CategoryTheory.Iso.inv cokernelIsoOfEq	—	cokernelIsoOfEq_refl CategoryTheory.Category.comp_id
π_comp_cokernelIsoOfEq_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cokernel cokernel.π CategoryTheory.Iso.inv cokernelIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_cokernelIsoOfEq_inv

CategoryTheory.Limits.CokernelCofork

Definitions

Name	Category	Theorems
isColimitOfIsColimitOfIff 📖	CompOp	—
isColimitOfIsColimitOfIff' 📖	CompOp	—
mapIsoOfIsColimit 📖	CompOp	2 math math: mapIsoOfIsColimit_inv, mapIsoOfIsColimit_hom
mapOfIsColimit 📖	CompOp	4 math math: π_mapOfIsColimit, mapIsoOfIsColimit_inv, mapIsoOfIsColimit_hom, π_mapOfIsColimit_assoc
ofπ 📖	CompOp	14 math math: CategoryTheory.Limits.cokernelBiproductιIso_hom, CategoryTheory.Preadditive.cokernelCoforkOfCofork_ofπ, CategoryTheory.ShortComplex.RightHomologyData.wι_assoc, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff, CategoryTheory.Limits.cokernelBiproductιIso_inv, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom, CategoryTheory.ShortComplex.RightHomologyData.wι, SheafOfModules.Presentation.map_relations_I, π_ofπ, CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_cocone, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv, CategoryTheory.Limits.isCokernelEpiComp_desc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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.Limits.Cofork.π	—	CategoryTheory.Limits.Cofork.condition CategoryTheory.Limits.zero_comp
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.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' condition
mapIsoOfIsColimit_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero mapIsoOfIsColimit mapOfIsColimit CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
mapIsoOfIsColimit_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero mapIsoOfIsColimit mapOfIsColimit CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
π_eq_zero 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Limits.WalkingParallelPair.zero	—	CategoryTheory.Limits.Cofork.app_zero_eq_comp_π_left condition
π_mapOfIsColimit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cofork.π mapOfIsColimit CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	CategoryTheory.Limits.IsColimit.fac
π_mapOfIsColimit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cofork.π mapOfIsColimit CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_mapOfIsColimit
π_ofπ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.Cofork.π ofπ	—	—

CategoryTheory.Limits.CokernelCofork.IsColimit

Definitions

Name	Category	Theorems
desc' 📖	CompOp	—
ofEpiOfIsZero 📖	CompOp	—
ofId 📖	CompOp	—
ofπ 📖	CompOp	2 math math: CategoryTheory.Limits.cokernelCoforkBiproductFromSubtype_isColimit, CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_inv
ofπ' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_π 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso CategoryTheory.Functor.obj 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.Cofork.π	—	CategoryTheory.Limits.isIso_colimit_cocone_parallelPair_of_eq
isZero_of_epi 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.Cofork.IsColimit.epi CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.cancel_epi CategoryTheory.Limits.CokernelCofork.condition_assoc CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp

CategoryTheory.Limits.HasCokernels

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_colimit 📖	mathematical	—	CategoryTheory.Limits.HasCokernel	—	—

CategoryTheory.Limits.HasKernels

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
has_limit 📖	mathematical	—	CategoryTheory.Limits.HasKernel	—	—

CategoryTheory.Limits.IsCokernel

Definitions

Name	Category	Theorems
cokernelIso 📖	CompOp	—
ofIso 📖	CompOp	—
ofIsoComp 📖	CompOp	—

CategoryTheory.Limits.IsKernel

Definitions

Name	Category	Theorems
isoKernel 📖	CompOp	—
ofCompIso 📖	CompOp	—
ofIso 📖	CompOp	—

CategoryTheory.Limits.KernelFork

Definitions

Name	Category	Theorems
isLimitOfIsLimitOfIff 📖	CompOp	—
isLimitOfIsLimitOfIff' 📖	CompOp	—
mapIsoOfIsLimit 📖	CompOp	2 math math: mapIsoOfIsLimit_inv, mapIsoOfIsLimit_hom
mapOfIsLimit 📖	CompOp	4 math math: mapOfIsLimit_ι_assoc, mapIsoOfIsLimit_inv, mapIsoOfIsLimit_hom, mapOfIsLimit_ι
ofι 📖	CompOp	13 math math: CategoryTheory.Limits.kernelForkBiproductToSubtype_cone, CategoryTheory.Limits.kernelBiproductπIso_hom, ι_ofι, CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom, CategoryTheory.Preadditive.kernelForkOfFork_ofι, CategoryTheory.ShortComplex.LeftHomologyData.wπ_assoc, CategoryTheory.Limits.kernelBiproductπIso_inv, CategoryTheory.ShortComplex.LeftHomologyData.wπ, CategoryTheory.Limits.isKernelCompMono_lift, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff, CategoryTheory.Limits.kernelBiproductToSubtypeIso_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
app_one 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.Cone.π CategoryTheory.Limits.WalkingParallelPair.one	—	CategoryTheory.Limits.Fork.app_one_eq_ι_comp_left condition
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.Limits.Fork.ι	—	CategoryTheory.Limits.Fork.condition CategoryTheory.Limits.HasZeroMorphisms.comp_zero
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.Limits.Fork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
mapIsoOfIsLimit_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero mapIsoOfIsLimit mapOfIsLimit CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
mapIsoOfIsLimit_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero mapIsoOfIsLimit mapOfIsLimit CategoryTheory.Arrow CategoryTheory.instCategoryArrow	—	—
mapOfIsLimit_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair.zero mapOfIsLimit CategoryTheory.Limits.Fork.ι CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.CommaMorphism.left	—	CategoryTheory.Limits.IsLimit.fac
mapOfIsLimit_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero mapOfIsLimit CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mapOfIsLimit_ι
ι_ofι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.Fork.ι ofι	—	—

CategoryTheory.Limits.KernelFork.IsLimit

Definitions

Name	Category	Theorems
lift' 📖	CompOp	—
ofId 📖	CompOp	—
ofMonoOfIsZero 📖	CompOp	—
ofι 📖	CompOp	2 math math: CategoryTheory.Limits.kernelBiproductToSubtypeIso_hom, CategoryTheory.Limits.kernelForkBiproductToSubtype_isLimit
ofι' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIso_ι 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso CategoryTheory.Functor.obj 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.Fork.ι	—	CategoryTheory.Limits.isIso_limit_cone_parallelPair_of_eq
isZero_of_mono 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.Fork.IsLimit.mono CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.cancel_mono CategoryTheory.Category.assoc CategoryTheory.Limits.KernelFork.condition CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp

CategoryTheory.Limits.MonoFactorisation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kernel_ι_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel I CategoryTheory.Limits.kernel.ι e Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.cancel_mono m_mono CategoryTheory.Limits.zero_comp CategoryTheory.Category.assoc fac CategoryTheory.Limits.kernel.condition

CategoryTheory.Limits.coker

Definitions

Name	Category	Theorems
π 📖	CompOp	3 math math: π_app, condition_assoc, condition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Arrow.leftFunc CategoryTheory.Arrow.rightFunc CategoryTheory.Limits.coker CategoryTheory.Arrow.leftToRight π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.instHasZeroMorphismsFunctor	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.cokernel.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Arrow.leftFunc CategoryTheory.Arrow.rightFunc CategoryTheory.Arrow.leftToRight CategoryTheory.Limits.coker π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.instHasZeroMorphismsFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Arrow.rightFunc CategoryTheory.Limits.coker π CategoryTheory.Limits.cokernel.π CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	—

CategoryTheory.Limits.cokernel

Definitions

Name	Category	Theorems
cokernelIso 📖	CompOp	—
desc 📖	CompOp	43 math math: CategoryTheory.kernelUnopOp_inv, CategoryTheory.Limits.cokernelImageι_inv, imageToKernel_unop, CategoryTheory.Limits.colimit_ι_zero_cokernel_desc_assoc, CategoryTheory.Limits.cokernelCompIsIso_hom, desc_epi, imageToKernel_op, CategoryTheory.Limits.coker_map, CategoryTheory.Abelian.coim_map, CategoryTheory.cokernelOpOp_hom, map_desc, π_desc_assoc, CategoryTheory.kernelOpUnop_inv, CategoryTheory.ShortComplex.Exact.mono_cokernelDesc, CategoryTheory.ShortComplex.opcyclesIsoCokernel_inv, desc_zero, CategoryTheory.cokernelOpUnop_inv, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_H, π_desc, CategoryTheory.Limits.cokernelComparison_map_desc, CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc, CategoryTheory.Limits.cokernelEpiComp_inv, CategoryTheory.kernelUnopUnop_hom, CategoryTheory.ShortComplex.HasRightHomology.hasKernel, CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_ι, CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc, CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc_assoc, CategoryTheory.cokernelUnopUnop_hom, congr_inv, CategoryTheory.Limits.colimit_ι_zero_cokernel_desc, CategoryTheory.Abelian.coimageIsoImage'_hom, CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc_assoc, SemiNormedGrp.explicitCokernelIso_hom_desc, π_desc_apply, CategoryTheory.Limits.cokernelCompIsIso_inv, CategoryTheory.cokernelUnopOp_inv, CategoryTheory.kernelOpOp_hom, CategoryTheory.Limits.cokernelZeroIsoTarget_hom, CategoryTheory.Limits.cokernelComparison_map_desc_assoc, CategoryTheory.Limits.cokernelEpiComp_hom, CategoryTheory.Limits.cokernelImageι_hom, congr_hom
desc' 📖	CompOp	—
isColimitCoconeZeroCocone 📖	CompOp	—
map 📖	CompOp	20 math math: map_zero, CategoryTheory.Limits.isIso_cokernel_map_of_isPushout, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃, map_desc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f, map_id, CategoryTheory.Abelian.mono_cokernel_map_of_isPullback, mapIso_hom, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂, CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map, CategoryTheory.Limits.cokernel_map_comp_cokernelComparison, CategoryTheory.Abelian.coimageImageComparisonFunctor_map, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, CategoryTheory.Limits.cokernel_map_comp_cokernelComparison_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁, CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, CategoryTheory.Limits.instIsIsoMapOfEpi, mapIso_inv
mapIso 📖	CompOp	2 math math: mapIso_hom, mapIso_inv
ofEpi 📖	CompOp	—
ofIsoComp 📖	CompOp	—
zeroCokernelCofork 📖	CompOp	—
π 📖	CompOp	112 math math: CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_p, CategoryTheory.Limits.coker.π_app, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, ModuleCat.cokernel_π_ext, CategoryTheory.Limits.cokernelImageι_inv, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.Limits.cokernelCompIsIso_hom, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero, CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom_assoc, CategoryTheory.kernelCokernelCompSequence.inl_π_assoc, CategoryTheory.cokernelUnopUnop_inv, CategoryTheory.Limits.PreservesCokernel.π_iso_hom_assoc, CategoryTheory.kernelOpUnop_hom, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel_π, CategoryTheory.Limits.coker_map, CategoryTheory.Abelian.instEpiFactorThruImage, CategoryTheory.Abelian.tfae_epi, CategoryTheory.kernelCokernelCompSequence.inr_π_assoc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, π_desc_assoc, π_zero_isIso, CategoryTheory.Limits.cokernel_not_mono_of_nonzero, CategoryTheory.Abelian.im_map, CategoryTheory.Limits.coequalizer_as_cokernel, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply, CategoryTheory.kernelUnopUnop_inv, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.Abelian.image_ι_comp_eq_zero, CategoryTheory.ShortComplex.cokernelSequence_g, ModuleCat.cokernel_π_imageSubobject_ext, condition, CategoryTheory.ShortComplex.exact_cokernel, CategoryTheory.cokernelUnopOp_hom, CategoryTheory.NonPreadditiveAbelian.instEpiFactorThruImage, CategoryTheory.cokernel.π_unop, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m, π_of_zero, CategoryTheory.Abelian.imageIsoImage_inv, CategoryTheory.kernelUnopOp_hom, CategoryTheory.cokernel.π_op, CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv_assoc, CategoryTheory.instIsIsoIndCoimageImageComparison, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, CategoryTheory.kernelCokernelCompSequence.inr_π, CategoryTheory.kernel.ι_unop, CategoryTheory.ShortComplex.opcyclesIsoCokernel_hom, condition_assoc, CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.Limits.π_comp_cokernelComparison_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p, π_desc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, SemiNormedGrp.explicitCokernelIso_hom_π, CategoryTheory.Limits.cokernelEpiComp_inv, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, CategoryTheory.kernelCokernelCompSequence.δ_fac, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc, CategoryTheory.Limits.kernel.of_cokernel_of_epi, CategoryTheory.Abelian.coimageImageComparisonFunctor_map, congr_inv, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, CategoryTheory.Limits.π_comp_cokernelComparison, CategoryTheory.cokernelOpUnop_hom, CategoryTheory.kernel.ι_op, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_π, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, CategoryTheory.Abelian.image.ι_comp_eq_zero, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, CategoryTheory.kernelOpOp_inv, CategoryTheory.Limits.PreservesCokernel.π_iso_hom, CategoryTheory.NonPreadditiveAbelian.diag_σ_assoc, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, π_of_epi, π_desc_apply, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁, CategoryTheory.Abelian.isIso_factorThruImage, CategoryTheory.Limits.cokernelCompIsIso_inv, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage, SemiNormedGrp.explicitCokernelIso_inv_π, CategoryTheory.NonPreadditiveAbelian.lift_σ_assoc, CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv, CategoryTheory.kernelCokernelCompSequence.inl_π, CategoryTheory.Abelian.instIsIsoCoimageImageComparison, CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom, CategoryTheory.Limits.cokernelZeroIsoTarget_inv, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac, CategoryTheory.Limits.cokernelOrderHom_coe, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, CategoryTheory.Limits.cokernelEpiComp_hom, CategoryTheory.cokernel_zero_of_nonzero_to_simple, CategoryTheory.cokernelOpOp_inv, CategoryTheory.Limits.cokernelImageι_hom, congr_hom, of_kernel_of_mono, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc, FGModuleCat.instIsIsoCoimageImageComparison, condition_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.CokernelCofork.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
congr_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.cokernel congr desc π	—	—
congr_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.cokernel congr desc π	—	—
desc_epi 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Epi CategoryTheory.Limits.cokernel desc	—	CategoryTheory.whisker_eq CategoryTheory.cancel_epi π_desc_assoc
desc_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	desc CategoryTheory.Limits.cokernel	—	CategoryTheory.Limits.coequalizer.hom_ext π_desc CategoryTheory.Limits.comp_zero
mapIso_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Limits.cokernel mapIso map	—	—
mapIso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.Limits.cokernel mapIso map	—	—
map_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.cokernel map desc	—	CategoryTheory.Limits.coequalizer.hom_ext π_desc_assoc CategoryTheory.Category.assoc π_desc
map_id 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	map CategoryTheory.Limits.cokernel	—	CategoryTheory.Limits.coequalizer.hom_ext π_desc CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
map_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	map CategoryTheory.Limits.cokernel	—	CategoryTheory.Limits.coequalizer.hom_ext π_desc CategoryTheory.Limits.zero_comp CategoryTheory.Limits.comp_zero
of_kernel_of_mono 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.cokernel CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι π	—	CategoryTheory.Limits.coequalizer.π_of_eq CategoryTheory.Limits.kernel.ι_of_mono
π_desc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.cokernel π desc	—	CategoryTheory.Limits.IsColimit.fac condition CategoryTheory.Limits.zero_comp
π_desc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.cokernel π desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_desc
π_of_epi 📖	mathematical	—	π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.zero_of_target_iso_zero
π_of_zero 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.cokernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.hasCoequalizer_of_self π	—	CategoryTheory.Limits.coequalizer.π_of_self
π_zero_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.cokernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.hasCoequalizer_of_self π	—	CategoryTheory.Limits.coequalizer.π_of_self

CategoryTheory.Limits.ker

Definitions

Name	Category	Theorems
ι 📖	CompOp	3 math math: ι_app, condition, condition_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Limits.ker CategoryTheory.Arrow.leftFunc CategoryTheory.Arrow.rightFunc ι CategoryTheory.Arrow.leftToRight Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.instHasZeroMorphismsFunctor	—	CategoryTheory.NatTrans.ext' CategoryTheory.Limits.kernel.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Limits.ker CategoryTheory.Arrow.leftFunc ι CategoryTheory.Arrow.rightFunc CategoryTheory.Arrow.leftToRight Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.instHasZeroMorphismsFunctor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Limits.ker CategoryTheory.Arrow.leftFunc ι CategoryTheory.Limits.kernel.ι CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—

CategoryTheory.Limits.kernel

Definitions

Name	Category	Theorems
isLimitConeZeroCone 📖	CompOp	—
isoKernel 📖	CompOp	—
lift' 📖	CompOp	—
map 📖	CompOp	26 math math: CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂, CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv_assoc, CategoryTheory.Limits.instIsIsoMapOfMono, mapIso_hom, CategoryTheory.Limits.kernelComparison_comp_kernel_map_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, map_zero, CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map, CategoryTheory.Abelian.epi_kernel_map_of_isPushout, lift_map, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g, CategoryTheory.Limits.kernelSubobjectIso_comp_kernel_map_assoc, CategoryTheory.Limits.kernelComparison_comp_kernel_map, map_id, CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv, CategoryTheory.Abelian.coimageImageComparisonFunctor_map, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f, CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, CategoryTheory.Limits.isIso_kernel_map_of_isPullback, mapIso_inv, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv
mapIso 📖	CompOp	2 math math: mapIso_hom, mapIso_inv
ofCompIso 📖	CompOp	—
ofMono 📖	CompOp	—
zeroKernelFork 📖	CompOp	—
ι 📖	CompOp	124 math math: CategoryTheory.kernelUnopOp_inv, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero, CategoryTheory.Limits.kernelSubobject_arrow'_apply, CategoryTheory.Limits.PreservesKernel.iso_inv_ι, CategoryTheory.Limits.kernel_not_epi_of_nonzero, condition_apply, CategoryTheory.Limits.equalizer_as_kernel, congr_inv, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι_assoc, CategoryTheory.Abelian.coim_map, CategoryTheory.kernel_zero_of_nonzero_from_simple, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage, CategoryTheory.Limits.kernelCompMono_hom, CategoryTheory.cokernelOpOp_hom, CategoryTheory.Limits.kernelSubobject_arrow_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, CategoryTheory.Limits.kernelComparison_comp_ι, CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc, CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_i, lift_ι_apply, CategoryTheory.Limits.PreservesKernel.iso_inv_ι_assoc, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i, CategoryTheory.kernelCokernelCompSequence.ι_fst, CategoryTheory.kernelOpUnop_inv, CategoryTheory.Limits.ker.ι_app, CategoryTheory.Limits.kernelIsIsoComp_hom, CategoryTheory.Abelian.instMonoFactorThruCoimage, ι_of_mono, CategoryTheory.Limits.kernelIsIsoComp_inv, CategoryTheory.cokernel.π_unop, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, lift_ι_assoc, CategoryTheory.Limits.kernelComparison_comp_ι_assoc, CategoryTheory.kernelCokernelCompSequence.ι_snd, CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc, CategoryTheory.ShortComplex.exact_kernel, CategoryTheory.cokernel.π_op, CategoryTheory.instIsIsoIndCoimageImageComparison, ι_of_zero, CategoryTheory.cokernelOpUnop_inv, CategoryTheory.ShortComplex.kernelSequence_f, CategoryTheory.Limits.kernelOrderHom_coe, CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι_assoc, condition, CategoryTheory.kernel.ι_unop, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, AddCommGrpCat.kernelIsoKer_inv_comp_ι, CategoryTheory.Limits.kernelSubobject_arrow, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, SheafOfModules.Presentation.map_relations_I, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', ModuleCat.kernelIsoKer_hom_ker_subtype, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, ι_zero_isIso, CategoryTheory.kernelUnopUnop_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, CategoryTheory.kernelCokernelCompSequence.δ_fac, CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_ι, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac_assoc, of_cokernel_of_epi, CategoryTheory.Abelian.coimageImageComparisonFunctor_map, CategoryTheory.cokernelUnopUnop_hom, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, CategoryTheory.Abelian.coimage.comp_π_eq_zero, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁, CategoryTheory.Limits.kernelSubobject_arrow'_assoc, CategoryTheory.Limits.kernelZeroIsoSource_hom, CategoryTheory.Abelian.coimageIsoImage'_hom, CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_ι, CategoryTheory.Limits.MonoFactorisation.kernel_ι_comp, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃, CategoryTheory.kernel.ι_op, CategoryTheory.ComposableArrows.Exact.cokerIsoKer_hom_fac, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, condition_assoc, CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι_assoc, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, lift_ι, CategoryTheory.Abelian.tfae_mono, CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, CategoryTheory.Limits.kernelSubobject_arrow_apply, CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι, CategoryTheory.cokernelUnopOp_inv, CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι_assoc, CategoryTheory.kernelOpOp_hom, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, CategoryTheory.Abelian.instIsIsoCoimageImageComparison, congr_hom, ModuleCat.kernelIsoKer_inv_kernel_ι, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac, CategoryTheory.ShortComplex.cyclesIsoKernel_inv, CategoryTheory.Limits.kernelCompMono_inv, CategoryTheory.Abelian.isIso_factorThruCoimage, CategoryTheory.Abelian.comp_coimage_π_eq_zero, CategoryTheory.Limits.kernelSubobject_arrow', CategoryTheory.Limits.cokernel.of_kernel_of_mono, CategoryTheory.Limits.ker_map, CategoryTheory.ComposableArrows.IsComplex.cokerToKer_fac_assoc, FGModuleCat.instIsIsoCoimageImageComparison

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.KernelFork.condition
condition_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
congr_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Limits.kernel congr lift ι	—	—
congr_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.kernel congr lift ι	—	—
lift_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.kernel lift map	—	CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Category.assoc lift_ι lift_ι_assoc
lift_mono 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Mono CategoryTheory.Limits.kernel lift	—	CategoryTheory.eq_whisker CategoryTheory.cancel_mono CategoryTheory.Category.assoc lift_ι
lift_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	lift CategoryTheory.Limits.kernel	—	CategoryTheory.Limits.equalizer.hom_ext lift_ι CategoryTheory.Limits.zero_comp
lift_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.kernel lift ι	—	CategoryTheory.Limits.IsLimit.fac condition CategoryTheory.Limits.comp_zero
lift_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.kernel lift ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_ι
mapIso_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Limits.kernel mapIso map	—	—
mapIso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.Iso.inv CategoryTheory.Limits.kernel mapIso map	—	—
map_id 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	map CategoryTheory.Limits.kernel	—	CategoryTheory.Limits.equalizer.hom_ext lift_ι CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
map_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	map CategoryTheory.Limits.kernel	—	CategoryTheory.Limits.equalizer.hom_ext lift_ι CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
of_cokernel_of_epi 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.kernel CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π ι	—	CategoryTheory.Limits.equalizer.ι_of_eq CategoryTheory.Limits.cokernel.π_of_epi
ι_of_mono 📖	mathematical	—	ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.zero_of_source_iso_zero
ι_of_zero 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.kernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.hasEqualizer_of_self ι	—	CategoryTheory.Limits.equalizer.ι_of_self
ι_zero_isIso 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.kernel Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.hasEqualizer_of_self ι	—	CategoryTheory.Limits.equalizer.ι_of_self

---

← Back to Index