Basic

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

Statistics

Metric	Count
Definitions biproductToPushout, biproductToPushoutCofork, isColimitBiproductToPushout, imageFactorisation, imageMonoFactorisation, isLimitPullbackToBiproduct, pullbackToBiproduct, pullbackToBiproductFork, coim, coimIsoIm, coimageFunctor, coimageFunctorIsoImageFunctor, coimageIsoImage, coimageIsoImage', coimageStrongEpiMonoFactorisation, epiDesc, epiIsCokernelOfKernel, im, imageFunctor, imageIsoImage, imageStrongEpiMonoFactorisation, isColimitMapCoconeOfCokernelCoforkOfπ, isLimitMapConeOfKernelForkOfι, monoIsKernelOfCokernel, monoLift, nonPreadditiveAbelian, ofCoimageImageComparisonIsIso, toPreadditive, abelian	29
Theorems hasImages, imageMonoFactorisation_I, imageMonoFactorisation_e, imageMonoFactorisation_e', imageMonoFactorisation_m, instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison, instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi, isNormalEpiCategory, isNormalMonoCategory, coimIsoIm_hom_app, coimIsoIm_inv_app, coim_map, coim_obj, comp_π_eq_zero, coimageIsoImage'_hom, coimageStrongEpiMonoFactorisation_I, coimageStrongEpiMonoFactorisation_e, coimageStrongEpiMonoFactorisation_m, comp_coimage_π_eq_zero, comp_epiDesc, comp_epiDesc_assoc, epi_fst_of_factor_thru_epi_mono_factorization, epi_fst_of_isLimit, epi_of_cokernel_π_eq_zero, epi_pullback_of_epi_f, epi_pullback_of_epi_g, epi_snd_of_isLimit, factorThruImage_comp_coimageIsoImage'_inv, hasBinaryBiproducts, hasCoequalizers, hasEqualizers, hasFiniteBiproducts, hasFiniteColimits, hasFiniteLimits, hasPullbacks, hasPushouts, hasZeroObject, has_cokernels, has_finite_products, has_kernels, im_map, im_obj, ι_comp_eq_zero, imageIsoImage_hom_comp_image_ι, imageIsoImage_inv, imageStrongEpiMonoFactorisation_I, imageStrongEpiMonoFactorisation_e, imageStrongEpiMonoFactorisation_m, image_ι_comp_eq_zero, instEpiFactorThruImage, instHasStrongEpiMonoFactorisations, instIsIsoCoimageImageComparison, instMonoFactorThruCoimage, isIso_factorThruCoimage, isIso_factorThruImage, monoLift_comp, monoLift_comp_assoc, mono_inl_of_factor_thru_epi_mono_factorization, mono_inl_of_isColimit, mono_inr_of_isColimit, mono_of_kernel_ι_eq_zero, mono_pushout_of_mono_f, mono_pushout_of_mono_g, toIsNormalEpiCategory, toIsNormalMonoCategory	65
Total	94

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
coim 📖	CompOp	4 math math: coim_map, coim_obj, coimIsoIm_hom_app, coimIsoIm_inv_app
coimIsoIm 📖	CompOp	2 math math: coimIsoIm_hom_app, coimIsoIm_inv_app
coimageFunctor 📖	CompOp	—
coimageFunctorIsoImageFunctor 📖	CompOp	—
coimageIsoImage 📖	CompOp	—
coimageIsoImage' 📖	CompOp	2 math math: factorThruImage_comp_coimageIsoImage'_inv, coimageIsoImage'_hom
coimageStrongEpiMonoFactorisation 📖	CompOp	3 math math: coimageStrongEpiMonoFactorisation_e, coimageStrongEpiMonoFactorisation_I, coimageStrongEpiMonoFactorisation_m
epiDesc 📖	CompOp	2 math math: comp_epiDesc, comp_epiDesc_assoc
epiIsCokernelOfKernel 📖	CompOp	—
im 📖	CompOp	4 math math: im_map, im_obj, coimIsoIm_hom_app, coimIsoIm_inv_app
imageFunctor 📖	CompOp	—
imageIsoImage 📖	CompOp	2 math math: imageIsoImage_inv, imageIsoImage_hom_comp_image_ι
imageStrongEpiMonoFactorisation 📖	CompOp	3 math math: imageStrongEpiMonoFactorisation_e, imageStrongEpiMonoFactorisation_m, imageStrongEpiMonoFactorisation_I
isColimitMapCoconeOfCokernelCoforkOfπ 📖	CompOp	—
isLimitMapConeOfKernelForkOfι 📖	CompOp	—
monoIsKernelOfCokernel 📖	CompOp	—
monoLift 📖	CompOp	2 math math: monoLift_comp, monoLift_comp_assoc
nonPreadditiveAbelian 📖	CompOp	10 math math: imageStrongEpiMonoFactorisation_e, instEpiFactorThruImage, coimageStrongEpiMonoFactorisation_e, instMonoFactorThruCoimage, coimageStrongEpiMonoFactorisation_I, imageStrongEpiMonoFactorisation_m, imageStrongEpiMonoFactorisation_I, isIso_factorThruImage, isIso_factorThruCoimage, coimageStrongEpiMonoFactorisation_m
ofCoimageImageComparisonIsIso 📖	CompOp	—
toPreadditive 📖	CompOp	643 math math: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, CategoryTheory.InjectiveResolution.Hom.hom'_f, CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, CategoryTheory.ShortComplex.SnakeInput.epi_L₃_g, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, CategoryTheory.ShortComplex.SnakeInput.L₀'_exact, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂, CategoryTheory.ObjectProperty.isoModSerre_zero_iff, CategoryTheory.ShortComplex.SnakeInput.w₀₂_assoc, CategoryTheory.kernelUnopOp_inv, FunctorCategory.coimageImageComparison_app', CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, CategoryTheory.ShortComplex.SnakeInput.op_δ, DerivedCategory.right_fac, CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.ShortComplex.SnakeInput.naturality_δ, CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, CategoryTheory.ShortComplex.SnakeInput.L₃_exact, Pseudoelement.pseudoZero_def, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂, CategoryTheory.ShortComplex.cokernelSequence_f, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up, CategoryTheory.ShortComplex.SnakeInput.L₁_exact, LeftResolution.chainComplexMap_zero, CategoryTheory.ShortComplex.instIsNormalEpiCategory, Ext.mk₀_addEquiv₀_apply, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, AlgebraicGeometry.Scheme.Modules.instAdditivePullback, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁, CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, CategoryTheory.kernelCokernelCompSequence.inl_π_assoc, HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₃, groupCohomology.mapShortComplex₃_exact, HomologicalComplex.instIsNormalEpiCategory, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₃, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', CategoryTheory.cokernelUnopUnop_inv, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, AlgebraicGeometry.tilde.map_sub, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.Functor.homologySequence_comp, CategoryTheory.kernelOpUnop_hom, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₁, CategoryTheory.InjectiveResolution.of_def, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.InjectiveResolution.instIsLECochainComplexOfNatInt, CochainComplex.cm5b.fac, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃_assoc, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CategoryTheory.ShortComplex.SnakeInput.op_L₂, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃, CochainComplex.IsKInjective.rightOrthogonal, CochainComplex.IsKInjective.Qh_map_bijective, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd, CategoryTheory.ShortComplex.SnakeInput.op_v₁₂, CategoryTheory.ShortComplex.SnakeInput.id_f₂, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, HomotopyCategory.instIsHomologicalIntUpHomologyFunctor, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.HomologySequence.exact₂, CategoryTheory.IsPullback.exact_shortComplex', coim_map, Ext.mk₀_neg, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂, CategoryTheory.instIsIsoToRightDerivedZero', CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, tfae_epi, CategoryTheory.ShortComplex.SnakeInput.comp_f₀, CategoryTheory.cokernelOpOp_hom, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, Pseudoelement.zero_eq_zero', CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down, CategoryTheory.ShortComplex.SnakeInput.instEpiGL₀', AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor, LeftResolution.exactAt_map_chainComplex_succ, CategoryTheory.ShortComplex.kernelSequence_exact, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₃, postcomp_extClass_surjective_of_projective_X₂, CategoryTheory.kernelCokernelCompSequence.ι_φ, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, LeftResolution.map_chainComplex_d, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, CochainComplex.mappingCone.inr_descShortComplex_assoc, CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f, Pseudoelement.pseudoZero_iff, HomologicalComplex.instEpiGShortComplexTruncLE, CategoryTheory.kernelCokernelCompSequence.inr_π_assoc, FunctorCategory.coimageImageComparison_app, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc, im_map, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.InjectivePresentation.shortExact_shortComplex, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, toIsNormalEpiCategory, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂, CategoryTheory.ShortComplex.SnakeInput.L₂'_g, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, HomologicalComplex.quasiIso_iff_evaluation, subobjectIsoSubobjectOp_apply, CategoryTheory.ShortComplex.SnakeInput.functorL₀_map, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, CategoryTheory.kernelUnopUnop_inv, CochainComplex.isKInjective_shift_iff, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, Ext.mk₀_smul, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, CategoryTheory.kernelCokernelCompSequence.ι_fst, CategoryTheory.ShortComplex.cokernelSequence_g, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, CategoryTheory.kernelOpUnop_inv, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.g'_eq, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f, CategoryTheory.ShortComplex.SnakeInput.L₁'_f, DerivedCategory.instLinearCochainComplexIntQ, LeftResolution.chainComplexMap_f_1, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂, CategoryTheory.InjectiveResolution.extMk_zero, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂_assoc, CategoryTheory.ShortComplex.exact_cokernel, CategoryTheory.cokernelUnopOp_hom, groupHomology.mapShortComplex₃_exact, CategoryTheory.Functor.IsHomological.toPreservesZeroMorphisms, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, CategoryTheory.kernelCokernelCompSequence.φ_snd_assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃_assoc, HomologicalComplex.instMonoFShortComplexTruncLE, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.ObjectProperty.monoModSerre_zero_iff, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, Pseudoelement.zero_morphism_ext, CategoryTheory.ShortComplex.SnakeInput.snd_δ, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, CategoryTheory.ProjectiveResolution.instIsKProjectiveCochainComplex, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, full_comp_preadditiveCoyonedaObj, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, DerivedCategory.instIsIsoMapCochainComplexIntQ, HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g, precomp_extClass_surjective_of_projective_X₂, CategoryTheory.simple_of_cosimple, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc, DerivedCategory.HomologySequence.comp_δ_assoc, CategoryTheory.cokernel.π_unop, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, mono_cokernel_map_of_isPullback, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, epi_kernel_map_of_isPushout, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₃, CategoryTheory.ShortComplex.kernelSequence_X₁, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₃, CategoryTheory.ShortComplex.SnakeInput.functorL₀_obj, CategoryTheory.Functor.homologySequence_exact₂, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.ShortComplex.SnakeInput.L₀_exact, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, CategoryTheory.instHasInjectiveDimensionLTBiprod, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CategoryTheory.Functor.homologySequenceδ_comp_assoc, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁_assoc, CategoryTheory.ProjectiveResolution.of_def, CategoryTheory.ShortComplex.instIsNormalMonoCategory, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂_assoc, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc, Ext.mk₀_add, AlgebraicTopology.inclusionOfMooreComplex_app, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂, CategoryTheory.kernelCokernelCompSequence.ι_snd, CategoryTheory.ShortComplex.SnakeInput.L₁'_g, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, imageIsoImage_inv, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₂, CategoryTheory.ShortComplex.SnakeInput.op_L₀, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π', CategoryTheory.ShortComplex.SnakeInput.functorL₂_obj, CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi, CategoryTheory.kernelUnopOp_hom, CategoryTheory.ObjectProperty.epiModSerre_zero_iff, CategoryTheory.ProjectiveResolution.Hom.hom'_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂, CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₂, CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', CategoryTheory.ShortComplex.exact_kernel, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, CategoryTheory.InjectiveResolution.instHasInjectiveResolution, instAdditiveAddCommGrpCatExtFunctorObj, CategoryTheory.cokernel.π_op, HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₁, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g, CategoryTheory.ShortComplex.SnakeInput.functorL₁_map, CategoryTheory.instIsIsoIndCoimageImageComparison, DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, CategoryTheory.kernelCokernelCompSequence.inl_φ, CategoryTheory.kernelCokernelCompSequence.inr_π, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, CategoryTheory.Functor.homologySequenceComposableArrows₅_exact, CategoryTheory.cokernelOpUnop_inv, HomologicalComplex.mono_homologyMap_shortComplexTruncLE_g, CategoryTheory.ShortComplex.kernelSequence_f, CategoryTheory.ShortComplex.SnakeInput.comp_f₂, CategoryTheory.Functor.comp_homologySequenceδ, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, CategoryTheory.ProjectiveResolution.instIsGECochainComplexOfNatInt, CategoryTheory.kernel.ι_unop, CategoryTheory.kernelCokernelCompSequence_exact, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, CategoryTheory.ShortComplex.SnakeInput.w₁₃_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc, CategoryTheory.ShortComplex.SnakeInput.functorP_map, CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₂, DerivedCategory.isLE_Q_obj_iff, factorThruImage_comp_coimageIsoImage'_inv, CochainComplex.cm5b.fac_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃, AlgebraicTopology.normalizedMooreComplex_objD, CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up, CategoryTheory.ObjectProperty.monoModSerre_iff, CategoryTheory.ProjectiveResolution.lift_commutes_zero, HomologicalComplex.quasiIsoAt_shortComplexTruncLE_g, coim_obj, CategoryTheory.kernelCokernelCompSequence.instEpiπ, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₃, CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ, CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective, Ext.mk₀_sum, CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, CategoryTheory.ObjectProperty.epiModSerre_iff, HomologicalComplex.shortComplexTruncLE_f, CochainComplex.instIsKProjectiveObjIntShiftFunctor, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, HomologicalComplex.isGrothendieckAbelian, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁_assoc, CategoryTheory.ShortComplex.SnakeInput.w₀₂, Pseudoelement.zero_morphism_ext', Ext.biprodAddEquiv_apply_fst, CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁, CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj, CochainComplex.IsKProjective.Qh_map_bijective, DerivedCategory.isGE_Q_obj_iff, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc, CategoryTheory.InjectiveResolution.desc_commutes, hasBinaryBiproducts, CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.InjectiveResolution.desc_commutes_assoc, CategoryTheory.ShortComplex.SnakeInput.id_f₁, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₁, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, CochainComplex.cm5b.instQuasiIsoIntP, CategoryTheory.ShortComplex.SnakeInput.op_L₃, AlgebraicTopology.NormalizedMooreComplex.d_squared, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements, Ext.mk₀_zero, CochainComplex.cm5b.instIsStrictlyGEI, CategoryTheory.ShortComplex.SnakeInput.functorL₃_map, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, CochainComplex.cm5b.instMonoFIntI, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁_assoc, CategoryTheory.Functor.instAdditiveOfIsHomological, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₃, CategoryTheory.InjectiveResolution.instHasInjectiveResolutions, CategoryTheory.ShortComplex.SnakeInput.id_f₀, CategoryTheory.ProjectiveResolution.extMk_zero, CategoryTheory.kernelUnopUnop_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₃, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective, CategoryTheory.ShortComplex.SnakeInput.op_v₂₃, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₀, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc, CategoryTheory.ShortComplex.SnakeInput.comp_f₁_assoc, CategoryTheory.ShortComplex.SnakeInput.op_v₀₁, im_obj, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₂, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.kernelCokernelCompSequence.δ_fac, DerivedCategory.HomologySequence.exact₁, CategoryTheory.Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono, CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective, HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, DoldKan.equivalence_inverse, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂_assoc, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, HomologicalComplex.shortComplexTruncLE_shortExact, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, CochainComplex.IsKProjective.leftOrthogonal, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₁, CochainComplex.cm5b.instInjectiveXIntI, CochainComplex.cm5b.instMonoIntI, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, AlgebraicGeometry.Scheme.Modules.Hom.add_app, groupCohomology.mapShortComplex₁_exact, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, HomologicalComplex.shortComplexTruncLE_X₂, CategoryTheory.ShortComplex.cokernelSequence_exact, CategoryTheory.instHasProjectiveDimensionLTBiprod, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_g, CochainComplex.isKProjective_iff_leftOrthogonal, HomologicalComplex.quasiIsoAt_iff_evaluation, CategoryTheory.presheafToSheaf_additive, CategoryTheory.Functor.map_distinguished_exact, CategoryTheory.ShortComplex.SnakeInput.comp_f₃, CategoryTheory.cokernelUnopUnop_hom, CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom, CochainComplex.shortComplexTruncLE_shortExact, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.cm5b.i_f_comp, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, CategoryTheory.ShortComplex.SnakeInput.L₂'_exact, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι, Pseudoelement.zero_eq_zero, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₁, CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements, groupHomology.mapShortComplex₁_exact, CategoryTheory.Functor.homologySequence_exact₁, imageIsoImage_hom_comp_image_ι, CategoryTheory.ShortComplex.exact_iff_image_eq_kernel, HomotopyCategory.mem_subcategoryAcyclic_iff, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁, CategoryTheory.InjectiveResolution.instIsKInjectiveCochainComplex, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_f, CategoryTheory.ShortComplex.SnakeInput.id_f₃, CategoryTheory.epi_from_simple_zero_of_not_iso, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_obj, DerivedCategory.right_fac_of_isStrictlyLE, coimage.comp_π_eq_zero, Ext.smul_eq_comp_mk₀, AlgebraicGeometry.tilde.map_add, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁, CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, Pseudoelement.pseudoZero_aux, Ext.addEquiv₀_symm_apply, CategoryTheory.ShortComplex.SnakeInput.mono_L₂_f, has_cokernels, AlgebraicTopology.NormalizedMooreComplex.obj_X, coimageIsoImage'_hom, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, ChainComplex.linearYonedaObj_d, CategoryTheory.categoryWithHomology_of_abelian, HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g, CategoryTheory.cokernelOpUnop_hom, CategoryTheory.ShortComplex.cokernelSequence_X₁, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃, CategoryTheory.ShortComplex.quasiIso_iff_evaluation, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, Ext.mk₀_eq_zero_iff, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', CategoryTheory.kernel.ι_op, CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc, preadditiveCoyonedaObj_map_surjective, CategoryTheory.kernelCokernelCompSequence.φ_π, CategoryTheory.InjectiveResolution.desc_commutes_zero, FunctorCategory.coimageObjIso_inv, image.ι_comp_eq_zero, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, CochainComplex.cm5b.i_f_comp_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, CategoryTheory.ShortComplex.cokernelSequence_X₃, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₂, DoldKan.equivalence_functor, CochainComplex.mappingCone.inr_descShortComplex, DerivedCategory.instAdditiveCochainComplexIntQ, CochainComplex.cm5b.I_d, CategoryTheory.ProjectiveResolution.exact₀, DerivedCategory.instAdditiveSingleFunctor, AlgebraicGeometry.tilde.map_zero, CategoryTheory.IsPushout.exact_shortComplex, CategoryTheory.ShortComplex.SnakeInput.op_L₁, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd_assoc, CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down, DerivedCategory.Qh_obj_singleFunctors_obj, FunctorCategory.imageObjIso_hom, CategoryTheory.Functor.IsHomological.exact, Ext.mk₀_linearEquiv₀_apply, CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, CochainComplex.mappingCone.inl_v_descShortComplex_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁, CategoryTheory.kernelOpOp_inv, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f, CochainComplex.mappingCone.inr_f_descShortComplex_f, toIsNormalMonoCategory, CategoryTheory.IsPushout.hom_eq_add_up_to_refinements, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', DerivedCategory.exists_iso_Q_obj_of_isLE, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, tfae_mono, HomologicalComplex.shortComplexTruncLE_X₁, Ext.addEquivBiprod_symm_apply, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, LeftResolution.map_chainComplex_d_1_0, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₁, DoldKan.comparisonN_hom_app_f, CategoryTheory.ShortComplex.SnakeInput.L₂'_f, CategoryTheory.kernelCokernelCompSequence.inl_φ_assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁_assoc, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, FunctorCategory.functor_category_isIso_coimageImageComparison, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, CategoryTheory.ProjectiveResolution.instHasProjectiveResolution, DerivedCategory.instEssSurjCochainComplexIntQ, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, Ext.linearEquiv₀_symm_apply, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₃, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁, CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderExtensions, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃, DerivedCategory.instLinearSingleFunctor, CategoryTheory.InjectiveResolution.exact₀, LeftResolution.chainComplexMap_f_succ_succ, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc, CategoryTheory.ShortComplex.SnakeInput.L₂_exact, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₂, CategoryTheory.cokernelUnopOp_inv, CategoryTheory.ShortComplex.kernelSequence_g, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁, CochainComplex.isKProjective_shift_iff, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₁, CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down, HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE, CategoryTheory.kernelOpOp_hom, LeftResolution.map_chainComplex_d_1_0_assoc, DerivedCategory.instLinearHomotopyCategoryIntUpQh, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₂, Ext.addEquivBiprod_apply_snd, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, CategoryTheory.ShortComplex.SnakeInput.epi_L₁_g, AlgebraicGeometry.tilde.map_neg, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, CategoryTheory.ShortComplex.kernelSequence_X₃, Pseudoelement.eq_zero_iff, HomologicalComplex.shortExact_iff_degreewise_shortExact, HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.ShortComplex.SnakeInput.comp_f₁, CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, DerivedCategory.HomologySequence.δ_comp_assoc, CategoryTheory.kernelCokernelCompSequence.inl_π, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, DerivedCategory.HomologySequence.δ_comp, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc, DerivedCategory.mem_distTriang_iff, CategoryTheory.ShortComplex.cokernelSequence_X₂, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃, CochainComplex.isKInjective_iff_rightOrthogonal, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, instIsIsoCoimageImageComparison, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, Ext.biprodAddEquiv_symm_apply, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, CategoryTheory.Functor.exact_tfae, DerivedCategory.HomologySequence.exact₃, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, DerivedCategory.Q_map_eq_of_homotopy, CategoryTheory.exact_f_d, CategoryTheory.exact_d_f, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CategoryTheory.kernelCokernelCompSequence.φ_snd, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, FunctorCategory.coimageObjIso_hom, subobjectIsoSubobjectOp_symm_apply, hasFiniteBiproducts, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, DerivedCategory.isIso_Q_map_iff_quasiIso, DerivedCategory.isIso_Qh_map_iff, CategoryTheory.Functor.map_distinguished_op_exact, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, CategoryTheory.ShortComplex.instMonoFKernelSequence, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel', DerivedCategory.left_fac_of_isStrictlyGE, CategoryTheory.Functor.homologySequenceδ_comp, HomologicalComplex.instIsNormalMonoCategory, HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, Ext.addEquivBiprod_apply_fst, CategoryTheory.ShortComplex.SnakeInput.w₁₃, epiWithInjectiveKernel_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst, HomologicalComplex.shortComplexTruncLE_X₃_isSupportedOutside, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, CategoryTheory.InjectiveResolution.descFOne_zero_comm, DoldKan.comparisonN_inv_app_f, FunctorCategory.imageObjIso_inv, CategoryTheory.ShortComplex.SnakeInput.functorL₂_map, CategoryTheory.ShortComplex.SnakeInput.instMonoFL₀'OfL₁, Pseudoelement.zero_apply, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₁, CategoryTheory.ShortComplex.instEpiGCokernelSequence, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc, HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CategoryTheory.cokernel_zero_of_nonzero_to_simple, AlgebraicGeometry.Scheme.Modules.instAdditivePushforward, CochainComplex.cm5b, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₁, Ext.biprodAddEquiv_apply_snd, HomologicalComplex.exact_iff_degreewise_exact, CategoryTheory.Functor.comp_homologySequenceδ_assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₀, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₂, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CategoryTheory.kernelCokernelCompSequence.instMonoι, coimIsoIm_hom_app, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom', CategoryTheory.cokernelOpOp_inv, CategoryTheory.ShortComplex.kernelSequence_X₂, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, has_kernels, CategoryTheory.kernelCokernelCompSequence.ι_φ_assoc, DerivedCategory.left_fac, AlgebraicTopology.normalizedMooreComplex_obj, CochainComplex.cm5b.I_X, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff, coimIsoIm_inv_app, CategoryTheory.instIsIsoFromLeftDerivedZero', CategoryTheory.kernelCokernelCompSequence.φ_π_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_f, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, ChainComplex.linearYonedaObj_X, DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coimIsoIm_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow coim im CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category coimIsoIm coimageImageComparison CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
coimIsoIm_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Arrow CategoryTheory.instCategoryArrow im coim CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category coimIsoIm CategoryTheory.inv coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom image coimageImageComparison instIsIsoCoimageImageComparison	—	—
coim_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow coim CategoryTheory.Limits.cokernel.desc CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.kernel CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Limits.kernel.ι coimage CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CommaMorphism.left coimage.π	—	—
coim_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow coim coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
coimageIsoImage'_hom 📖	mathematical	—	CategoryTheory.Iso.hom coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations coimageIsoImage' CategoryTheory.Limits.cokernel.desc CategoryTheory.Limits.factorThruImage	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations CategoryTheory.Limits.cokernel.π_desc CategoryTheory.cancel_mono CategoryTheory.Limits.instMonoι CategoryTheory.Category.assoc CategoryTheory.Limits.IsImage.lift_ι CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.image.fac
coimageStrongEpiMonoFactorisation_I 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation coimageStrongEpiMonoFactorisation coimage CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	—	—
coimageStrongEpiMonoFactorisation_e 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.e CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation coimageStrongEpiMonoFactorisation coimage.π CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	—	—
coimageStrongEpiMonoFactorisation_m 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation coimageStrongEpiMonoFactorisation factorThruCoimage CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	—	—
comp_coimage_π_eq_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	coimage CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι coimage.π	—	CategoryTheory.Limits.zero_of_comp_mono CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels instMonoFactorThruCoimage CategoryTheory.Category.assoc CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.kernel.condition
comp_epiDesc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.kernel.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	epiDesc	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.IsColimit.fac CategoryTheory.Limits.KernelFork.condition
comp_epiDesc_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.kernel.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	epiDesc	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_epiDesc
epi_fst_of_factor_thru_epi_mono_factorization 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PullbackCone.fst	—	epi_fst_of_isLimit CategoryTheory.cancel_mono
epi_fst_of_isLimit 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PullbackCone.fst	—	CategoryTheory.epi_of_epi_fac CategoryTheory.Limits.hasLimitOfHasLimitsOfShape epi_pullback_of_epi_g CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
epi_of_cokernel_π_eq_zero 📖	mathematical	CategoryTheory.Limits.cokernel.π CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Epi	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Preadditive.epi_of_cokernel_zero
epi_pullback_of_epi_f 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.snd	—	CategoryTheory.Preadditive.epi_of_cancel_zero CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Limits.comp_zero zero_add CategoryTheory.Limits.KernelFork.condition CategoryTheory.Limits.biprod.epi_desc_of_epi_left CategoryTheory.Limits.biprod.inl_desc CategoryTheory.Category.assoc CategoryTheory.cancel_epi CategoryTheory.Limits.biprod.inr_desc CategoryTheory.Limits.HasZeroMorphisms.comp_zero
epi_pullback_of_epi_g 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.pullback CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.pullback.fst	—	CategoryTheory.Preadditive.epi_of_cancel_zero CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Limits.comp_zero add_zero CategoryTheory.Limits.KernelFork.condition CategoryTheory.Limits.biprod.epi_desc_of_epi_right CategoryTheory.Preadditive.instEpiNegHom CategoryTheory.Limits.biprod.inr_desc CategoryTheory.Category.assoc CategoryTheory.cancel_epi CategoryTheory.Preadditive.neg_comp CategoryTheory.Limits.biprod.inl_desc CategoryTheory.Limits.HasZeroMorphisms.comp_zero
epi_snd_of_isLimit 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingCospan CategoryTheory.Limits.WidePullbackShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.cospan CategoryTheory.Limits.PullbackCone.snd	—	CategoryTheory.epi_of_epi_fac CategoryTheory.Limits.hasLimitOfHasLimitsOfShape epi_pullback_of_epi_f CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
factorThruImage_comp_coimageIsoImage'_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.factorThruImage CategoryTheory.Iso.inv coimageIsoImage' CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations CategoryTheory.Limits.image.fac_lift
hasBinaryBiproducts 📖	mathematical	—	CategoryTheory.Limits.HasBinaryBiproducts CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	—	CategoryTheory.Limits.hasBinaryBiproducts_of_finite_biproducts hasFiniteBiproducts
hasCoequalizers 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizers	—	CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels has_cokernels
hasEqualizers 📖	mathematical	—	CategoryTheory.Limits.HasEqualizers	—	CategoryTheory.Preadditive.hasEqualizers_of_hasKernels has_kernels
hasFiniteBiproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteBiproducts CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	—	CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts has_finite_products
hasFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits	—	CategoryTheory.Limits.hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts hasFiniteBiproducts hasCoequalizers
hasFiniteLimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteLimits	—	CategoryTheory.Limits.hasFiniteLimits_of_hasEqualizers_and_finite_products has_finite_products hasEqualizers
hasPullbacks 📖	mathematical	—	CategoryTheory.Limits.HasPullbacks	—	CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers CategoryTheory.Limits.hasLimitsOfShape_discrete has_finite_products Finite.of_fintype hasEqualizers
hasPushouts 📖	mathematical	—	CategoryTheory.Limits.HasPushouts	—	CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts hasFiniteBiproducts Finite.of_fintype hasCoequalizers
hasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject	—	CategoryTheory.Limits.hasZeroObject_of_hasInitial_object CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteBiproducts hasFiniteBiproducts Finite.of_fintype
has_cokernels 📖	mathematical	—	CategoryTheory.Limits.HasCokernels CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	—	—
has_finite_products 📖	mathematical	—	CategoryTheory.Limits.HasFiniteProducts	—	—
has_kernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	—	—
im_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow im CategoryTheory.Limits.kernel.lift CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Limits.cokernel CategoryTheory.Comma.left CategoryTheory.Comma.hom CategoryTheory.Limits.cokernel.π image CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image.ι CategoryTheory.CommaMorphism.right	—	—
im_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow im image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
imageIsoImage_hom_comp_image_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations CategoryTheory.Iso.hom imageIsoImage CategoryTheory.Limits.image.ι CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations CategoryTheory.Limits.IsImage.lift_ι
imageIsoImage_inv 📖	mathematical	—	CategoryTheory.Iso.inv image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations imageIsoImage CategoryTheory.Limits.kernel.lift CategoryTheory.Limits.image.ι	—	CategoryTheory.Limits.image.ext CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations instHasStrongEpiMonoFactorisations CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.NormalMonoCategory.hasEqualizers has_finite_products toIsNormalMonoCategory CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Limits.IsImage.isoExt_inv CategoryTheory.Limits.image.isImage_lift CategoryTheory.Limits.image.fac_lift imageStrongEpiMonoFactorisation_e CategoryTheory.Category.assoc CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.equalizer_as_kernel CategoryTheory.Limits.image.fac
imageStrongEpiMonoFactorisation_I 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.I CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation imageStrongEpiMonoFactorisation image CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	—	—
imageStrongEpiMonoFactorisation_e 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.e CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation imageStrongEpiMonoFactorisation factorThruImage CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	—	—
imageStrongEpiMonoFactorisation_m 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.m CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation imageStrongEpiMonoFactorisation image.ι CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	—	—
image_ι_comp_eq_zero 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian	image CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π image.ι	—	CategoryTheory.Limits.zero_of_epi_comp CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels instEpiFactorThruImage CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.kernel.lift_ι_assoc
instEpiFactorThruImage 📖	mathematical	—	CategoryTheory.Epi image CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π factorThruImage	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.NonPreadditiveAbelian.instEpiFactorThruImage
instHasStrongEpiMonoFactorisations 📖	mathematical	—	CategoryTheory.Limits.HasStrongEpiMonoFactorisations	—	—
instIsIsoCoimageImageComparison 📖	mathematical	—	CategoryTheory.IsIso coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι image CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π coimageImageComparison	—	CategoryTheory.Limits.HasKernels.has_limit has_kernels CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Category.assoc coimage_image_factorisation CategoryTheory.Limits.IsImage.lift_fac CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.kernel.condition CategoryTheory.Iso.isIso_hom
instMonoFactorThruCoimage 📖	mathematical	—	CategoryTheory.Mono coimage CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι factorThruCoimage	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage
isIso_factorThruCoimage 📖	mathematical	—	CategoryTheory.IsIso coimage CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι factorThruCoimage	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage
isIso_factorThruImage 📖	mathematical	—	CategoryTheory.IsIso image CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π factorThruImage	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage
monoLift_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.cokernel.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	monoLift	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.IsLimit.fac CategoryTheory.Limits.CokernelCofork.condition
monoLift_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Limits.cokernel.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	monoLift	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.NonPreadditiveAbelian.has_cokernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' monoLift_comp
mono_inl_of_factor_thru_epi_mono_factorization 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inl	—	mono_inl_of_isColimit CategoryTheory.cancel_epi
mono_inl_of_isColimit 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inl	—	CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.hasColimitOfHasColimitsOfShape mono_pushout_of_mono_g CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
mono_inr_of_isColimit 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.PushoutCocone.inr	—	CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.hasColimitOfHasColimitsOfShape mono_pushout_of_mono_f CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom
mono_of_kernel_ι_eq_zero 📖	mathematical	CategoryTheory.Limits.kernel.ι CategoryTheory.NonPreadditiveAbelian.toHasZeroMorphisms nonPreadditiveAbelian CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Mono	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.NonPreadditiveAbelian.has_kernels CategoryTheory.Preadditive.mono_of_kernel_zero
mono_pushout_of_mono_f 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.pushout CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inr	—	CategoryTheory.Preadditive.mono_of_cancel_zero CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Limits.zero_comp zero_add CategoryTheory.Limits.CokernelCofork.condition CategoryTheory.Limits.biprod.mono_lift_of_mono_left CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.Limits.biprod.lift_snd
mono_pushout_of_mono_g 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.pushout CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingSpan CategoryTheory.Limits.WidePushoutShape.category CategoryTheory.Limits.WalkingPair CategoryTheory.Limits.span CategoryTheory.Limits.pushout.inl	—	CategoryTheory.Preadditive.mono_of_cancel_zero CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct hasBinaryBiproducts CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Limits.zero_comp add_zero CategoryTheory.Limits.CokernelCofork.condition CategoryTheory.Limits.biprod.mono_lift_of_mono_right CategoryTheory.Preadditive.instMonoNegHom CategoryTheory.Limits.biprod.lift_snd CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.Preadditive.comp_neg neg_zero CategoryTheory.Limits.biprod.lift_fst
toIsNormalEpiCategory 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	—	—
toIsNormalMonoCategory 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive	—	—

CategoryTheory.Abelian.BiproductToPushoutIsCokernel

Definitions

Name	Category	Theorems
biproductToPushout 📖	CompOp	—
biproductToPushoutCofork 📖	CompOp	—
isColimitBiproductToPushout 📖	CompOp	—

CategoryTheory.Abelian.OfCoimageImageComparisonIsIso

Definitions

Name	Category	Theorems
imageFactorisation 📖	CompOp	—
imageMonoFactorisation 📖	CompOp	6 math math: imageMonoFactorisation_I, imageMonoFactorisation_m, instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison, imageMonoFactorisation_e', instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi, imageMonoFactorisation_e

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasImages 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Abelian.coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.image CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.coimageImageComparison	CategoryTheory.Limits.HasImages	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit
imageMonoFactorisation_I 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.I imageMonoFactorisation CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
imageMonoFactorisation_e 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.e imageMonoFactorisation CategoryTheory.Limits.kernel.lift CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	—
imageMonoFactorisation_e' 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.e imageMonoFactorisation CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.image CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.coimageImageComparison	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.cokernel.π_desc_assoc
imageMonoFactorisation_m 📖	mathematical	—	CategoryTheory.Limits.MonoFactorisation.m imageMonoFactorisation CategoryTheory.Limits.kernel.ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	—
instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.MonoFactorisation.I imageMonoFactorisation CategoryTheory.Limits.MonoFactorisation.e	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit imageMonoFactorisation_e' CategoryTheory.IsIso.comp_isIso CategoryTheory.Limits.cokernel.of_kernel_of_mono
instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Limits.MonoFactorisation.I imageMonoFactorisation CategoryTheory.Limits.MonoFactorisation.m	—	CategoryTheory.Limits.kernel.of_cokernel_of_epi
isNormalEpiCategory 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Abelian.coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.image CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.coimageImageComparison	CategoryTheory.IsNormalEpiCategory	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.kernel.condition instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts CategoryTheory.IsIso.comp_inv_eq imageMonoFactorisation_e' CategoryTheory.Limits.MonoFactorisation.fac CategoryTheory.Limits.colimit.ι_desc CategoryTheory.cancel_epi CategoryTheory.Limits.CokernelCofork.π_ofπ
isNormalMonoCategory 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Abelian.coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.image CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.coimageImageComparison	CategoryTheory.IsNormalMonoCategory	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.cokernel.condition instIsIsoEImageMonoFactorisationOfHasZeroObjectOfMonoOfCoimageImageComparison CategoryTheory.Limits.hasZeroObject_of_hasFiniteBiproducts CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_comp_eq CategoryTheory.Limits.MonoFactorisation.fac CategoryTheory.Limits.limit.lift_π CategoryTheory.cancel_mono CategoryTheory.Limits.KernelFork.ι_ofι

CategoryTheory.Abelian.PullbackToBiproductIsKernel

Definitions

Name	Category	Theorems
isLimitPullbackToBiproduct 📖	CompOp	—
pullbackToBiproduct 📖	CompOp	—
pullbackToBiproductFork 📖	CompOp	—

CategoryTheory.Abelian.coimage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_π_eq_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.coimage CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.cancel_mono CategoryTheory.Abelian.instMonoFactorThruCoimage CategoryTheory.Category.assoc CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.zero_comp

CategoryTheory.Abelian.image

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_comp_eq_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.cancel_epi CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.Limits.kernel.lift_ι_assoc CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.comp_zero

CategoryTheory.NonPreadditiveAbelian

Definitions

Name	Category	Theorems
abelian 📖	CompOp	—

---

← Back to Index