Basic

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

Statistics

Metric	Count
Definitions AbelianStruct, cokernelCofork, image, imageIsCokernel, imageIsKernel, imageι, imageπ, isColimitCokernelCofork, isLimitKernelFork, kernelFork, biproductToPushout, biproductToPushoutCofork, isColimitBiproductToPushout, imageFactorisation, imageMonoFactorisation, isLimitPullbackToBiproduct, pullbackToBiproduct, pullbackToBiproductFork, coim, coimIsoIm, coimageFunctor, coimageFunctorIsoImageFunctor, coimageIsoImage, coimageIsoImage', coimageStrongEpiMonoFactorisation, epiDesc, epiIsCokernelOfKernel, im, imageFunctor, imageIsoImage, imageStrongEpiMonoFactorisation, isColimitMapCoconeOfCokernelCoforkOfπ, isLimitMapConeOfKernelForkOfι, mk', monoIsKernelOfCokernel, monoLift, nonPreadditiveAbelian, ofCoimageImageComparisonIsIso, toPreadditive, abelian	40
Theorems fac, fac_assoc, imageι_π, imageι_π_assoc, ι_imageπ, ι_imageπ_assoc, 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	71
Total	111

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
AbelianStruct 📖	CompData	—
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	—
mk' 📖	CompOp	—
monoIsKernelOfCokernel 📖	CompOp	—
monoLift 📖	CompOp	2 math math: monoLift_comp, monoLift_comp_assoc
nonPreadditiveAbelian 📖	CompOp	12 math math: imageStrongEpiMonoFactorisation_e, instEpiFactorThruImage, coimageStrongEpiMonoFactorisation_e, image_ι_comp_eq_zero, instMonoFactorThruCoimage, coimageStrongEpiMonoFactorisation_I, imageStrongEpiMonoFactorisation_m, imageStrongEpiMonoFactorisation_I, isIso_factorThruImage, isIso_factorThruCoimage, comp_coimage_π_eq_zero, coimageStrongEpiMonoFactorisation_m
ofCoimageImageComparisonIsIso 📖	CompOp	—
toPreadditive 📖	CompOp	1211 math math: CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_left, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, SpectralObject.δ_eq_zero_of_isIso₂, CategoryTheory.InjectiveResolution.Hom.hom'_f, CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, SpectralObject.H_map_twoδ₂Toδ₁_toCycles_assoc, CategoryTheory.ShortComplex.SnakeInput.epi_L₃_g, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, CategoryTheory.ShortComplex.SnakeInput.L₀'_exact, SpectralObject.exact₁', SpectralObject.dCokernelSequence_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂, CategoryTheory.ObjectProperty.isoModSerre_zero_iff, CategoryTheory.ShortComplex.SnakeInput.w₀₂_assoc, Preradical.shortComplex_X₁, CategoryTheory.kernelUnopOp_inv, CategoryTheory.ShortComplex.ShortExact.epi_δ, FunctorCategory.coimageImageComparison_app', CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, SpectralObject.SpectralSequence.HomologyData.kfSc_exact, CategoryTheory.ShortComplex.Exact.comp_descToInjective, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, CategoryTheory.ShortComplex.SnakeInput.op_δ, DerivedCategory.right_fac, CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc, SpectralObject.leftHomologyDataShortComplex_H, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff, SpectralObject.homologyDataIdId_left_π, SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_i, SpectralObject.dKernelSequence_exact, CategoryTheory.SpectralSequence.pageFunctor_map, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CategoryTheory.ShortComplex.SnakeInput.naturality_δ, Preradical.instEpiGShortComplexObj, CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁, Preradical.instMonoFShortComplexObj, CategoryTheory.ObjectProperty.exists_epiModSerre_comp_eq_zero_iff, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, SpectralObject.instMonoFKernelSequenceE, SpectralObject.SpectralSequence.HomologyData.kfSc_g, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc, SpectralObject.zero₂_assoc, CochainComplex.Lifting.π_f_cochain₁_v_ι_f, CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff, SpectralObject.cokernelSequenceCycles_X₁, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, SpectralObject.cokernelSequenceCyclesEIso_hom_τ₁, CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff, CategoryTheory.ShortComplex.SnakeInput.L₃_exact, Pseudoelement.pseudoZero_def, imageToKernel_unop, CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂, SpectralObject.dKernelSequence_X₂, SpectralObject.sc₂_X₃, CategoryTheory.ShortComplex.cokernelSequence_f, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, SpectralObject.cyclesIso_inv_i_assoc, CategoryTheory.ShortComplex.ShortExact.mono_δ, SpectralObject.cokernelSequenceOpcycles_X₂, SpectralObject.instMonoFKernelSequenceOpcycles, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up, CochainComplex.IsKInjective.nonempty_homotopy_zero, CategoryTheory.ShortComplex.SnakeInput.L₁_exact, LeftResolution.chainComplexMap_zero, CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero, SpectralObject.cokernelSequenceCyclesEIso_inv_τ₃, CategoryTheory.ShortExact.shortExact_map_iff, CategoryTheory.ShortComplex.instIsNormalEpiCategory, Ext.mk₀_addEquiv₀_apply, CategoryTheory.ProjectiveResolution.iso_hom_naturality_assoc, Preradical.shortComplex_g, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements, SpectralObject.δToCycles_πE, Pseudoelement.exact_of_pseudo_exact, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_Q, CategoryTheory.InjectiveResolution.iso_hom_naturality, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃, DerivedCategory.HomologySequence.comp_δ, Preradical.shortComplexObj_X₂, SpectralObject.kernelSequenceCyclesE_X₁, Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, SpectralObject.shortComplex_X₂, SpectralObject.SpectralSequence.HomologyData.kf_w, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality_assoc, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, AlgebraicGeometry.Scheme.Modules.instAdditivePullback, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Functor.homologySequence_comp_assoc, SpectralObject.cokernelSequenceOpcyclesE_exact, CochainComplex.homologyMap_homologyδOfTriangle_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g, CochainComplex.mappingCone.homologySequenceδ_triangleh, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁, Ext.contravariant_sequence_exact₁', CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, SpectralObject.kernelSequenceOpcycles_f, CochainComplex.IsKProjective.homotopyZero_def, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, SpectralObject.sc₁_f, CategoryTheory.kernelCokernelCompSequence.inl_π_assoc, HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₃, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply, groupCohomology.mapShortComplex₃_exact, SpectralObject.δ_δ_assoc, SpectralObject.opcyclesIso_hom_δFromOpcycles, HomologicalComplex.instIsNormalEpiCategory, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₃, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₃, SpectralObject.homologyDataIdId_left_i, SpectralObject.Ψ_opcyclesMap, CategoryTheory.JointlyReflectIsomorphisms.quasiIso_iff, CategoryTheory.cokernelUnopUnop_inv, SpectralObject.homologyDataIdId_left_H, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, AlgebraicGeometry.tilde.map_sub, CategoryTheory.ShortComplex.ShortExact.d_eq_zero_of_f_eq_d_apply, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.Functor.homologySequence_comp, CategoryTheory.kernelOpUnop_hom, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₁, CategoryTheory.InjectiveResolution.of_def, SpectralObject.dCokernelSequence_X₂, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁, SpectralObject.dHomologyData_iso_inv, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, SpectralObject.instMonoFKernelSequenceOpcyclesE, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_K, CategoryTheory.InjectiveResolution.instIsLECochainComplexOfNatInt, CochainComplex.cm5b.fac, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃_assoc, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, HomologicalComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements, CategoryTheory.ShortComplex.SnakeInput.op_L₂, SpectralObject.δToCycles_cyclesIso_inv_assoc, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc, CochainComplex.IsKInjective.rightOrthogonal, SpectralObject.cyclesIso_hom_i, 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, CategoryTheory.ShortComplex.ShortExact.comp_δ, HomotopyCategory.instIsHomologicalIntUpHomologyFunctor, imageToKernel_op, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, SpectralObject.instMonoFKernelSequenceCyclesE, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, HomologicalComplex.shortExact_of_degreewise_shortExact, DerivedCategory.HomologySequence.exact₂, CategoryTheory.IsPullback.exact_shortComplex', SpectralObject.cyclesMap_Ψ_exact, coim_map, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, SpectralObject.kernelSequenceCycles_g, CategoryTheory.ProjectiveResolution.sub_extMk, DerivedCategory.homologyFunctorFactors_hom_naturality, Ext.mk₀_neg, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂, SpectralObject.homologyDataIdId_iso_inv, CategoryTheory.instIsIsoToRightDerivedZero', CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g, CategoryTheory.Limits.CokernelCofork.IsColimit.comp_π_eq_zero_iff_up_to_refinements, TopCat.Sheaf.exact_iff_stalkFunctor_map_exact, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc, tfae_epi, CategoryTheory.ShortComplex.SnakeInput.comp_f₀, CategoryTheory.cokernelOpOp_hom, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full, SpectralObject.δ_δ, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, Pseudoelement.zero_eq_zero', CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff, SpectralObject.cyclesIso_hom_i_assoc, Preradical.shortExact_shortComplexObj, CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down, CategoryTheory.ShortComplex.SnakeInput.instEpiGL₀', AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, AlgebraicGeometry.instAdditiveModuleCatCarrierModulesSpecOfFunctor, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι, LeftResolution.exactAt_map_chainComplex_succ, CategoryTheory.ShortComplex.kernelSequence_exact, SpectralObject.SpectralSequence.page_d, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc, CochainComplex.Lifting.exists_hom, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₃, postcomp_extClass_surjective_of_projective_X₂, CategoryTheory.kernelCokernelCompSequence.ι_φ, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc, DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, LeftResolution.map_chainComplex_d, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, SpectralObject.cokernelSequenceCyclesE_exact, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, SpectralObject.cokernelSequenceOpcycles_exact, SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃_assoc, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, SpectralObject.leftHomologyDataShortComplex_f', DerivedCategory.triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKProjective, CochainComplex.mappingCone.inr_descShortComplex_assoc, CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f, Pseudoelement.pseudoZero_iff, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_π, CategoryTheory.ShortComplex.ShortExact.δ_eq', HomologicalComplex.instEpiGShortComplexTruncLE, SpectralObject.shortComplex_g, DerivedCategory.mappingCone_triangle_distinguished, CategoryTheory.JointlyReflectIsomorphisms.shortExact_iff, CategoryTheory.kernelCokernelCompSequence.inr_π_assoc, SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_exact, SpectralObject.sequenceΨ_exact, SpectralObject.kernelSequenceOpcyclesE_X₁, FunctorCategory.coimageImageComparison_app, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, Ext.contravariant_sequence_exact₂', SpectralObject.instEpiGShortComplexOpcyclesThreeδ₂Toδ₁, CochainComplex.HomComplex.CohomologyClass.bijective_toSmallShiftedHom_of_isKInjective, CochainComplex.homologyδOfTriangle_homologyMap_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, SpectralObject.cyclesIso_inv_cyclesMap_assoc, HomologicalComplex.HomologySequence.snakeInput_v₂₃, Preradical.ι_π_assoc, CategoryTheory.ShortComplex.Exact.liftFromProjective_comp_assoc, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, HomologicalComplex.HomologySequence.mapSnakeInput_f₃, CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc, SpectralObject.map_fourδ₁Toδ₀_d, SpectralObject.SpectralSequence.HomologyData.kfSc_f, im_map, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc, HomologicalComplex.HomologySequence.snakeInput_L₁, CategoryTheory.ShortComplex.epi_of_epi_of_epi_of_epi, Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_H, SpectralObject.homologyDataIdId_iso_hom, SpectralObject.sc₃_g, CategoryTheory.InjectivePresentation.shortExact_shortComplex, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, toIsNormalEpiCategory, SpectralObject.SpectralSequence.pageD_pageD, SpectralObject.cokernelSequenceOpcyclesE_X₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₁, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂, SpectralObject.kernelSequenceE_exact, CategoryTheory.ShortComplex.ShortExact.extClass_hom, CategoryTheory.ShortComplex.SnakeInput.L₂'_g, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel, SpectralObject.d_d, SpectralObject.cokernelSequenceOpcycles_X₃, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, SpectralObject.p_opcyclesIso_inv, CategoryTheory.ShortComplex.Exact.liftFromProjective_comp, CochainComplex.homologyδOfTriangle_homologyMap, SpectralObject.kernelSequenceOpcyclesE_X₃, HomologicalComplex.quasiIso_iff_evaluation, CategoryTheory.InjectiveResolution.extMk_surjective, subobjectIsoSubobjectOp_apply, CategoryTheory.ShortComplex.SnakeInput.functorL₀_map, SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₂, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, CategoryTheory.kernelUnopUnop_inv, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc, CochainComplex.isKInjective_shift_iff, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, Ext.covariant_sequence_exact₁', Ext.mk₀_smul, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i, SpectralObject.instEpiGCokernelSequenceOpcyclesE, SpectralObject.zero₃, CochainComplex.homologyMap_comp_eq_zero_of_distTriang, SpectralObject.rightHomologyDataShortComplex_ι, SpectralObject.cyclesMap_Ψ_assoc, CategoryTheory.ProjectiveResolution.extMk_comp_mk₀, DerivedCategory.shiftMap_homologyFunctor_map_Qh_assoc, SpectralObject.Ψ_opcyclesMap_exact, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, SpectralObject.instMonoFShortComplexOpcyclesThreeδ₂Toδ₁, 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, CategoryTheory.Functor.preservesHomology_of_map_exact, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, SpectralObject.map_fourδ₁Toδ₀_d_assoc, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f, SpectralObject.cokernelSequenceE_g, DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso, Ext.covariant_sequence_exact₃', CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f, DerivedCategory.triangleOfSES_obj₃, TopCat.instAdditivePresheafStalkFunctor, SpectralObject.dHomologyData_left_i, CochainComplex.homologyMap_exact₃_of_distTriang, SpectralObject.kernelSequenceE_g, CategoryTheory.ShortComplex.SnakeInput.L₁'_f, DerivedCategory.instLinearCochainComplexIntQ, CochainComplex.homologyMap_exact₂_of_distTriang, CategoryTheory.InjectiveResolution.add_extMk, SpectralObject.exact₂', LeftResolution.chainComplexMap_f_1, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂, SpectralObject.homologyDataIdId_right_p, SpectralObject.kernelSequenceE_X₁, CategoryTheory.InjectiveResolution.extMk_zero, SpectralObject.dShortComplex_g, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂_assoc, CategoryTheory.ShortComplex.exact_cokernel, SpectralObject.rightHomologyDataShortComplex_H, SpectralObject.exact₂, CategoryTheory.cokernelUnopOp_hom, SpectralObject.dKernelSequence_X₃, CategoryTheory.Functor.preservesHomology_of_preservesMonos_and_cokernels, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality, groupHomology.mapShortComplex₃_exact, SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_shortExact, 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.ProjectiveResolution.extMk_hom, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, CategoryTheory.ObjectProperty.monoModSerre_zero_iff, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, SpectralObject.ιE_δFromOpcycles_assoc, Pseudoelement.zero_morphism_ext, CategoryTheory.ShortComplex.SnakeInput.snd_δ, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂, CochainComplex.homologyMap_exact₁_of_distTriang, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, CategoryTheory.ProjectiveResolution.instIsKProjectiveCochainComplex, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, CochainComplex.IsKInjective.homotopyZero_def, CategoryTheory.ShortComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, SpectralObject.shortComplexMap_id, full_comp_preadditiveCoyonedaObj, HomologicalComplex.HomologySequence.snakeInput_v₀₁, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, SpectralObject.cokernelSequenceCycles_exact, HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g, precomp_extClass_surjective_of_projective_X₂, CategoryTheory.ShortComplex.SnakeInput.mono_δ, CategoryTheory.simple_of_cosimple, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, SpectralObject.dHomologyData_right_Q, CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc, HomologicalComplex.HomologySequence.quasiIso_τ₃, DerivedCategory.HomologySequence.comp_δ_assoc, SpectralObject.dShortComplex_f, CategoryTheory.cokernel.π_unop, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι, SpectralObject.cokernelSequenceCyclesEIso_hom_τ₃, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, Preradical.toColon_hom_left_colonπ_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, SpectralObject.dHomologyData_left_H, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc, SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₃, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, mono_cokernel_map_of_isPullback, CategoryTheory.SpectralSequence.pageHomologyNatIso_hom_app, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, SpectralObject.kernelSequenceOpcycles_X₂, epi_kernel_map_of_isPushout, CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply, DerivedCategory.triangleOfSES.map_hom₁, SpectralObject.kernelSequenceCyclesE_g, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₃, CategoryTheory.ShortComplex.kernelSequence_X₁, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₃, CategoryTheory.ShortComplex.SnakeInput.functorL₀_obj, CategoryTheory.Functor.homologySequence_exact₂, Preradical.ι_π, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.ShortComplex.SnakeInput.L₀_exact, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, CategoryTheory.ShortComplex.ShortExact.extClass_naturality, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, SpectralObject.cokernelSequenceCycles_X₂, SpectralObject.sc₂_g, 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.ShortComplex.comp_pOpcycles_eq_zero_iff_up_to_refinements, SpectralObject.cokernelSequenceOpcyclesE_X₂, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, CategoryTheory.ProjectiveResolution.iso_hom_naturality, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂_assoc, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, SpectralObject.H_map_twoδ₂Toδ₁_toCycles, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc, Ext.mk₀_add, AlgebraicTopology.inclusionOfMooreComplex_app, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂, CategoryTheory.kernelCokernelCompSequence.ι_snd, CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₂, CategoryTheory.ShortComplex.SnakeInput.L₁'_g, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, SpectralObject.δToCycles_πE_assoc, SpectralObject.p_opcyclesIso_hom, SpectralObject.sc₁_X₁, imageIsoImage_inv, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₂, CategoryTheory.ProjectiveResolution.add_extMk, 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.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ObjectProperty.epiModSerre_zero_iff, CategoryTheory.ProjectiveResolution.Hom.hom'_f, SpectralObject.cokernelSequenceCycles_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₂, CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₂, CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', ChainComplex.isIso_descOpcycles_iff, CategoryTheory.ObjectProperty.instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, CategoryTheory.ShortComplex.exact_kernel, SpectralObject.zero₂, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, CategoryTheory.InjectiveResolution.instHasInjectiveResolution, instAdditiveAddCommGrpCatExtFunctorObj, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₁, CategoryTheory.cokernel.π_op, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_p, SpectralObject.kernelSequenceOpcyclesE_exact, HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₁, CategoryTheory.ShortComplex.ShortExact.comp_extClass_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g, CategoryTheory.ShortComplex.SnakeInput.functorL₁_map, CategoryTheory.instIsIsoIndCoimageImageComparison, DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, CategoryTheory.kernelCokernelCompSequence.inl_φ, CategoryTheory.kernelCokernelCompSequence.inr_π, Preradical.shortComplexObj_X₁, CategoryTheory.InjectiveResolution.extMk_eq_zero_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ObjectProperty.epiModSerre.isoModSerre_image_ι, 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.Functor.preservesHomology_of_preservesEpis_and_kernels, SpectralObject.cokernelSequenceCyclesE_g, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CategoryTheory.ShortComplex.SnakeInput.comp_f₂, CategoryTheory.Functor.comp_homologySequenceδ, SpectralObject.instMonoFKernelSequenceCycles, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, CategoryTheory.ProjectiveResolution.instIsGECochainComplexOfNatInt, CategoryTheory.kernel.ι_unop, SpectralObject.shortComplexMap_comp_assoc, CategoryTheory.kernelCokernelCompSequence_exact, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, SpectralObject.cokernelSequenceE_X₂, CategoryTheory.InjectiveResolution.toRightDerivedZero'_naturality, CategoryTheory.ShortComplex.SnakeInput.w₁₃_assoc, CategoryTheory.ShortComplex.comp_homologyπ_eq_iff_up_to_refinements, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc, CategoryTheory.ShortComplex.SnakeInput.functorP_map, HomologicalComplex.i_cyclesMk, SpectralObject.p_opcyclesIso_hom_assoc, SpectralObject.cokernelSequenceCyclesE_X₁, SpectralObject.homologyDataIdId_right_ι, SpectralObject.exact₃', CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality, CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, Preradical.toColon_hom_left_colonπ, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, HomologicalComplex.HomologySequence.epi_homologyMap_τ₃, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₂, DerivedCategory.isLE_Q_obj_iff, factorThruImage_comp_coimageIsoImage'_inv, CochainComplex.cm5b.fac_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃, TopCat.Sheaf.IsFlasque.epi_of_shortExact, Ext.covariant_sequence_exact₃, AlgebraicTopology.normalizedMooreComplex_objD, CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up, CochainComplex.IsKProjective.nonempty_homotopy_zero, HomologicalComplex.opcycles_right_exact, SpectralObject.cokernelSequenceCycles_X₃, CategoryTheory.ObjectProperty.monoModSerre_iff, CategoryTheory.ProjectiveResolution.lift_commutes_zero, DerivedCategory.triangleOfSES_obj₁, CategoryTheory.ShortComplex.SnakeInput.isIso_δ, Preradical.shortComplex_X₂, HomologicalComplex.quasiIsoAt_shortComplexTruncLE_g, coim_obj, SpectralObject.cokernelSequenceCyclesEIso_hom_τ₂, 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, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp, SpectralObject.cokernelSequenceCycles_g, Ext.mk₀_sum, CategoryTheory.ShortComplex.ShortExact.δ_apply', CategoryTheory.ShortComplex.quasiIso_iff_of_zeros', SpectralObject.SpectralSequence.HomologyData.kfSc_X₃, SpectralObject.cokernelIsoCycles_hom_fac_assoc, CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, SpectralObject.cokernelSequenceCyclesE_f, HomologicalComplex.HomologySequence.mapSnakeInput_f₁, CategoryTheory.ShortComplex.ShortExact.comp_extClass, SpectralObject.iCycles_δ, 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, CategoryTheory.ShortComplex.quasiIso_iff_of_zeros, SpectralObject.cokernelSequenceCyclesEIso_inv_τ₁, HomologicalComplex.comp_homologyπ_eq_iff_up_to_refinements, HomologicalComplex.isGrothendieckAbelian, SpectralObject.cokernelSequenceE_exact, SpectralObject.kernelSequenceE_f, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁_assoc, TopCat.Sheaf.sections_exact_of_left_exact, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc, CategoryTheory.ShortComplex.SnakeInput.w₀₂, CategoryTheory.SpectralSequence.pageFunctor_obj, SpectralObject.d_map_fourδ₄Toδ₃, Pseudoelement.zero_morphism_ext', Ext.biprodAddEquiv_apply_fst, CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁, CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj, HomologicalComplex.epi_homologyMap_iff_up_to_refinements, CochainComplex.IsKProjective.Qh_map_bijective, SpectralObject.kernelSequenceCycles_X₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle_mor₂, SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₂, DerivedCategory.isGE_Q_obj_iff, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_H, HomologicalComplex.HomologySequence.δ_naturality_assoc, CategoryTheory.ShortComplex.Exact.comp_descToInjective_assoc, SpectralObject.SpectralSequence.page_X, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_right, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, CochainComplex.isIso_liftCycles_iff, CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc, CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements, HomologicalComplex.cycles_left_exact, CategoryTheory.InjectiveResolution.desc_commutes, CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp, CategoryTheory.ShortComplex.SnakeInput.lift_φ₂_assoc, hasBinaryBiproducts, SpectralObject.dCokernelSequence_X₁, CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p, SpectralObject.kernelSequenceCyclesE_f, SpectralObject.sc₂_X₁, CochainComplex.Lifting.π_f_cochain₁_v_ι_f_assoc, SpectralObject.instEpiGCokernelSequenceCycles, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.InjectiveResolution.desc_commutes_assoc, SpectralObject.SpectralSequence.HomologyData.kfSc_X₂, CategoryTheory.ObjectProperty.prop_X₂_of_exact, SpectralObject.d_map_fourδ₄Toδ₃_assoc, CategoryTheory.ShortComplex.SnakeInput.id_f₁, CategoryTheory.ShortComplex.ShortExact.isIso_δ, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₁, SpectralObject.composableArrows₅_exact, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, CochainComplex.cm5b.instQuasiIsoIntP, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, Ext.covariant_sequence_exact₂', SpectralObject.cokernelSequenceCyclesE_X₂, CategoryTheory.ShortComplex.SnakeInput.op_L₃, SpectralObject.zero₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CochainComplex.mappingCone.quasiIso_descShortComplex, AlgebraicTopology.NormalizedMooreComplex.d_squared, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements, Preradical.shortComplexObj_f, Ext.mk₀_zero, CochainComplex.cm5b.instIsStrictlyGEI, CategoryTheory.InjectiveResolution.iso_hom_naturality_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, SpectralObject.sc₃_X₁, CategoryTheory.ObjectProperty.exists_comp_monoModSerre_eq_zero_iff, CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality_assoc, CategoryTheory.ShortComplex.SnakeInput.functorL₃_map, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, CategoryTheory.ShortComplex.epi_homologyMap_iff_up_to_refinements, CategoryTheory.ShortComplex.Exact.exact_up_to_refinements, SpectralObject.dKernelSequence_g, SpectralObject.shortComplex_f, CochainComplex.cm5b.instMonoFIntI, SpectralObject.leftHomologyDataShortComplex_π, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁_assoc, SpectralObject.cokernelSequenceCyclesE_X₃, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality, CategoryTheory.Functor.instAdditiveOfIsHomological, SpectralObject.dHomologyData_right_ι, CategoryTheory.ShortComplex.ShortExact.δ_comp_assoc, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₃, CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₁, SpectralObject.leftHomologyDataShortComplex_i, SpectralObject.p_opcyclesIso_inv_assoc, CategoryTheory.SpectralSequence.pageHomologyNatIso_inv_app, SpectralObject.shortComplexMap_τ₂, CategoryTheory.InjectiveResolution.instHasInjectiveResolutions, CategoryTheory.ShortComplex.SnakeInput.id_f₀, CategoryTheory.ProjectiveResolution.extMk_zero, HomologicalComplex.HomologySequence.snakeInput_L₀, CategoryTheory.kernelUnopUnop_hom, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, SpectralObject.homologyDataIdId_left_K, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₃, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, SpectralObject.δ_pOpcycles_assoc, CategoryTheory.InjectiveResolution.sub_extMk, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, CategoryTheory.ShortComplex.ShortExact.homology_exact₃, DerivedCategory.triangleOfSES.map_hom₃, HomologicalComplex.liftCycles_comp_homologyπ_eq_iff_up_to_refinements, instAdditiveOppositeFunctorAddCommGrpCatExtFunctor, CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective, Ext.covariant_sequence_exact₁, 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₂, SpectralObject.dHomologyData_right_H, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.kernelCokernelCompSequence.δ_fac, SpectralObject.shortComplexMap_τ₃, DerivedCategory.HomologySequence.exact₁, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc, CategoryTheory.Functor.leftDerived_map_eq, SpectralObject.sc₂_X₂, HomologicalComplex.HomologySequence.snakeInput_L₂, 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, SpectralObject.cokernelIsoCycles_hom_fac, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂_assoc, SpectralObject.exact₃, SpectralObject.δToCycles_cyclesIso_inv, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, HomologicalComplex.shortComplexTruncLE_shortExact, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, CochainComplex.IsKProjective.leftOrthogonal, Preradical.instEpiFunctorGShortComplex, CategoryTheory.SpectralSequence.comp_hom_assoc, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, SpectralObject.cokernelSequenceOpcyclesE_X₁, Preradical.toColon_hom_left_app_colonπ_app_assoc, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₁, SpectralObject.dHomologyData_right_p, CochainComplex.cm5b.instInjectiveXIntI, CategoryTheory.ShortComplex.ShortExact.δ_eq, CochainComplex.cm5b.instMonoIntI, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, AlgebraicGeometry.Scheme.Modules.Hom.add_app, groupCohomology.mapShortComplex₁_exact, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_iso, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, SpectralObject.kernelSequenceOpcycles_g, SpectralObject.dHomologyData_left_K, CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff, HomologicalComplex.shortComplexTruncLE_X₂, CategoryTheory.ShortComplex.cokernelSequence_exact, CategoryTheory.instHasProjectiveDimensionLTBiprod, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, CategoryTheory.InjectiveResolution.mk₀_comp_extMk, 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, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, CategoryTheory.ShortComplex.SnakeInput.comp_f₃, CategoryTheory.InjectiveResolution.extMk_hom, SpectralObject.opcyclesIsoKernel_hom_fac, SpectralObject.SpectralSequence.HomologyData.instMonoFKfSc, SpectralObject.kernelSequenceOpcyclesE_X₂, CategoryTheory.cokernelUnopUnop_hom, CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom, SpectralObject.sc₁_X₃, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₂, CochainComplex.shortComplexTruncLE_shortExact, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.cm5b.i_f_comp, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, CategoryTheory.ShortComplex.SnakeInput.L₂'_exact, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃, HomologicalComplex.HomologySequence.snakeInput_v₁₂, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, HomologicalComplex.exact_of_degreewise_exact, 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, CategoryTheory.ShortComplex.SnakeInput.δ_apply', CategoryTheory.ShortComplex.ShortExact.δ_apply, groupHomology.mapShortComplex₁_exact, CategoryTheory.Functor.homologySequence_exact₁, imageIsoImage_hom_comp_image_ι, CategoryTheory.ShortComplex.exact_iff_image_eq_kernel, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_ι, SpectralObject.rightHomologyDataShortComplex_g', HomologicalComplex.HomologySequence.snakeInput_L₃, CategoryTheory.SpectralSequence.Hom.comm_assoc, HomotopyCategory.mem_subcategoryAcyclic_iff, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁, CategoryTheory.InjectiveResolution.instIsKInjectiveCochainComplex, TopCat.Sheaf.IsFlasque.of_shortExact_of_isFlasque₁₂, Preradical.shortComplexObj_g, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_f, CategoryTheory.ProjectiveResolution.extMk_surjective, SpectralObject.cokernelSequenceE_X₃, 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, SpectralObject.opcyclesIso_hom_δFromOpcycles_assoc, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂, Ext.smul_eq_comp_mk₀, AlgebraicGeometry.tilde.map_add, CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁, CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, SpectralObject.instEpiGDCokernelSequence, Pseudoelement.pseudoZero_aux, Ext.addEquiv₀_symm_apply, CategoryTheory.ShortComplex.SnakeInput.mono_L₂_f, has_cokernels, HomologicalComplex.HomologySequence.composableArrows₅_exact, CategoryTheory.ShortComplex.SnakeInput.δ_apply, AlgebraicTopology.NormalizedMooreComplex.obj_X, coimageIsoImage'_hom, CategoryTheory.ShortComplex.SnakeInput.epi_δ, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃, CategoryTheory.ShortComplex.ShortExact.δ_comp, DerivedCategory.shiftMap_homologyFunctor_map_Q, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, SpectralObject.opcyclesIsoKernel_hom_fac_assoc, CategoryTheory.Functor.rightDerived_map_eq, SpectralObject.ιE_δFromOpcycles, ChainComplex.linearYonedaObj_d, CategoryTheory.categoryWithHomology_of_abelian, SpectralObject.instEpiGCokernelSequenceE, HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g, CategoryTheory.cokernelOpUnop_hom, CategoryTheory.ShortComplex.cokernelSequence_X₁, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, SpectralObject.homologyDataIdId_right_H, Preradical.ι_π_app, CategoryTheory.ShortComplex.quasiIso_iff_evaluation, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, Ext.mk₀_eq_zero_iff, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', CategoryTheory.kernel.ι_op, CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc, HomologicalComplex.HomologySequence.isIso_homologyMap_τ₃, preadditiveCoyonedaObj_map_surjective, HomologicalComplex.HomologySequence.composableArrows₂_exact, CategoryTheory.kernelCokernelCompSequence.φ_π, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_symm_apply, SpectralObject.instEpiGCokernelSequenceOpcycles, CategoryTheory.InjectiveResolution.desc_commutes_zero, HomologicalComplex.exactAt_iff_exact_up_to_refinements, FunctorCategory.coimageObjIso_inv, SpectralObject.shortComplexMap_τ₁, CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernel, SpectralObject.d_d_assoc, image.ι_comp_eq_zero, CochainComplex.Lifting.hasLift, 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₂, SpectralObject.SpectralSequence.pageD_pageD_assoc, SpectralObject.zero₃_assoc, Preradical.shortComplex_f, HomologicalComplex.HomologySequence.δ_naturality, DoldKan.equivalence_functor, CochainComplex.mappingCone.inr_descShortComplex, DerivedCategory.instAdditiveCochainComplexIntQ, CochainComplex.cm5b.I_d, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CategoryTheory.ProjectiveResolution.exact₀, SpectralObject.kernelSequenceCyclesE_exact, SpectralObject.cokernelSequenceOpcycles_g, DerivedCategory.instAdditiveSingleFunctor, SpectralObject.rightHomologyDataShortComplex_Q, SpectralObject.dShortComplex_X₃, SpectralObject.SpectralSequence.HomologyData.kfSc_X₁, AlgebraicGeometry.tilde.map_zero, SpectralObject.kernelSequenceCyclesE_X₂, SpectralObject.shortComplex_X₁, CategoryTheory.IsPushout.exact_shortComplex, CategoryTheory.ShortComplex.SnakeInput.op_L₁, SpectralObject.dCokernelSequence_exact, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd_assoc, CategoryTheory.SpectralSequence.Hom.comm, CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down, SpectralObject.dKernelSequence_X₁, SpectralObject.cokernelSequenceOpcycles_X₁, DerivedCategory.Qh_obj_singleFunctors_obj, CategoryTheory.InjectiveResolution.neg_extMk, FunctorCategory.imageObjIso_hom, CategoryTheory.Functor.IsHomological.exact, Ext.mk₀_linearEquiv₀_apply, CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv, CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc, CochainComplex.mappingCone.inl_v_descShortComplex_f, CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁, Ext.contravariant_sequence_exact₂, SpectralObject.opcyclesMap_opcyclesIso_hom_assoc, CategoryTheory.kernelOpOp_inv, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f, HomologicalComplex.HomologySequence.mapSnakeInput_f₂, SpectralObject.sc₃_X₃, CochainComplex.mappingCone.inr_f_descShortComplex_f, SpectralObject.homologyDataIdId_right_Q, Preradical.instMonoFunctorFShortComplex, CochainComplex.mappingCone.map_descShortComplex, SpectralObject.cyclesMap_Ψ, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, SpectralObject.kernelSequenceCycles_f, DerivedCategory.triangleOfSES.map_hom₂, toIsNormalMonoCategory, CategoryTheory.IsPushout.hom_eq_add_up_to_refinements, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', CategoryTheory.ShortComplex.ShortExact.singleTriangle_obj₃, SpectralObject.shortComplex_X₃, DerivedCategory.exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, SpectralObject.sc₃_X₂, SpectralObject.dKernelSequence_f, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, SpectralObject.rightHomologyDataShortComplex_p, SpectralObject.kernelSequenceOpcycles_X₁, tfae_mono, HomologicalComplex.shortComplexTruncLE_X₁, SpectralObject.kernelSequenceOpcyclesE_f, CategoryTheory.ObjectProperty.instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, Ext.addEquivBiprod_symm_apply, SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₁, SpectralObject.kernelSequenceCycles_X₃, CochainComplex.homologyMap_homologyδOfTriangle, DerivedCategory.triangleOfSES_obj₂, SpectralObject.dHomologyData_left_π, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, Preradical.shortComplex_X₃, LeftResolution.map_chainComplex_d_1_0, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₁, SpectralObject.dHomologyData_iso_hom, DoldKan.comparisonN_hom_app_f, CategoryTheory.ShortComplex.SnakeInput.L₂'_f, CategoryTheory.kernelCokernelCompSequence.inl_φ_assoc, SpectralObject.instEpiGCokernelSequenceCyclesE, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁_assoc, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, FunctorCategory.functor_category_isIso_coimageImageComparison, SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_g, HomologicalComplex.comp_homologyπ_eq_zero_iff_up_to_refinements, SpectralObject.dCokernelSequence_X₃, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, SpectralObject.cokernelSequenceOpcycles_f, CategoryTheory.ProjectiveResolution.instHasProjectiveResolution, SpectralObject.δ_pOpcycles, Preradical.shortComplexObj_X₃, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero, Ext.contravariant_sequence_exact₃', DerivedCategory.instEssSurjCochainComplexIntQ, SpectralObject.cyclesIso_inv_i, CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, SpectralObject.dCokernelSequence_g, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, Ext.linearEquiv₀_symm_apply, DerivedCategory.shiftMap_homologyFunctor_map_Qh, CochainComplex.isKInjective_of_injective_aux, DerivedCategory.triangleOfSES_mor₂, CochainComplex.homologyMap_comp_eq_zero_of_distTriang_assoc, SpectralObject.δ_eq_zero_of_isIso₁, SpectralObject.instMonoFDKernelSequence, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂, SpectralObject.cokernelSequenceE_X₁, CategoryTheory.ShortComplex.ShortExact.homology_exact₁, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₃, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CategoryTheory.ProjectiveResolution.iso_inv_naturality, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁, CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderExtensions, SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₃, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃, SpectralObject.kernelSequenceE_X₂, DerivedCategory.instLinearSingleFunctor, SpectralObject.cokernelSequenceCyclesEIso_inv_τ₂, Preradical.ι_π_app_assoc, Ext.contravariant_sequence_exact₁, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, CategoryTheory.ShortComplex.epi_of_mono_of_epi_of_mono, CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero, CategoryTheory.InjectiveResolution.exact₀, LeftResolution.chainComplexMap_f_succ_succ, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc, Ext.covariant_sequence_exact₂, SpectralObject.dShortComplex_X₂, 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, SpectralObject.cokernelSequenceE_f, HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE, CategoryTheory.kernelOpOp_hom, SpectralObject.cokernelSequenceOpcyclesE_g, SpectralObject.kernelSequenceOpcycles_exact, SpectralObject.sc₁_X₂, CategoryTheory.ShortComplex.mono_of_mono_of_mono_of_mono, LeftResolution.map_chainComplex_d_1_0_assoc, DerivedCategory.instLinearHomotopyCategoryIntUpQh, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₂, CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₃, Ext.addEquivBiprod_apply_snd, CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, SpectralObject.shortComplexMap_comp, CategoryTheory.ShortComplex.SnakeInput.epi_L₁_g, AlgebraicGeometry.tilde.map_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, CategoryTheory.ShortComplex.kernelSequence_X₃, SpectralObject.sc₂_f, CochainComplex.HomComplex.CohomologyClass.equivOfIsKProjective_apply, Pseudoelement.eq_zero_iff, HomologicalComplex.shortExact_iff_degreewise_shortExact, HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero, SpectralObject.kernelSequenceCycles_exact, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality, SpectralObject.exact₁, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.ShortComplex.SnakeInput.comp_f₁, CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, DerivedCategory.HomologySequence.δ_comp_assoc, CategoryTheory.kernelCokernelCompSequence.inl_π, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, SpectralObject.kernelSequenceE_X₃, CochainComplex.Lifting.comp_coe_cocyle₁'_v_eq_zero_assoc, DerivedCategory.HomologySequence.δ_comp, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj, SpectralObject.cokernelSequenceOpcyclesE_f, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel', CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc, DerivedCategory.mem_distTriang_iff, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc, CategoryTheory.ShortComplex.cokernelSequence_X₂, Pseudoelement.pseudo_exact_of_exact, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃, CochainComplex.isKInjective_iff_rightOrthogonal, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, CategoryTheory.ShortComplex.SnakeInput.δ_eq, instIsIsoCoimageImageComparison, SpectralObject.kernelSequenceCycles_X₁, CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, DerivedCategory.mappingCocone_triangle_distinguished, Ext.biprodAddEquiv_symm_apply, CategoryTheory.ProjectiveResolution.neg_extMk, SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_f, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, SpectralObject.sc₃_f, HomologicalComplex.HomologySequence.mono_homologyMap_τ₃, SpectralObject.iCycles_δ_assoc, CategoryTheory.Functor.exact_tfae, DerivedCategory.HomologySequence.exact₃, SpectralObject.zero₁_assoc, CategoryTheory.ProjectiveResolution.iso_inv_naturality_assoc, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, DerivedCategory.Q_map_eq_of_homotopy, Preradical.shortExact_shortComplex, CategoryTheory.SpectralSequence.comp_hom, CochainComplex.Lifting.comp_coe_cocycle₁_comp, CochainComplex.Lifting.coe_cocycle₁'_v_comp_eq_zero_assoc, CategoryTheory.exact_f_d, CategoryTheory.exact_d_f, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CategoryTheory.kernelCokernelCompSequence.φ_snd, SpectralObject.cyclesIso_inv_cyclesMap, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, TopCat.Sheaf.instAdditivePresheafForget, FunctorCategory.coimageObjIso_hom, subobjectIsoSubobjectOp_symm_apply, hasFiniteBiproducts, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, HomologicalComplex.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements, DerivedCategory.isIso_Q_map_iff_quasiIso, SpectralObject.kernelSequenceCyclesE_X₃, DerivedCategory.isIso_Qh_map_iff, CategoryTheory.Functor.map_distinguished_op_exact, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, CategoryTheory.ShortComplex.instMonoFKernelSequence, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel', DerivedCategory.left_fac_of_isStrictlyGE, CategoryTheory.ObjectProperty.prop_iff_of_shortExact, CategoryTheory.Functor.homologySequenceδ_comp, HomologicalComplex.instIsNormalMonoCategory, HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₁, CategoryTheory.InjectiveResolution.iso_inv_naturality, SpectralObject.leftHomologyDataShortComplex_K, Ext.addEquivBiprod_apply_fst, CategoryTheory.ShortComplex.SnakeInput.w₁₃, epiWithInjectiveKernel_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernel, SpectralObject.kernelSequenceOpcyclesEIso_hom_τ₁, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, Ext.contravariant_sequence_exact₃, 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, SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₂, CategoryTheory.ShortComplex.SnakeInput.instMonoFL₀'OfL₁, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, Pseudoelement.zero_apply, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₁, CategoryTheory.ShortComplex.instEpiGCokernelSequence, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.epi_f, HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, CategoryTheory.Functor.reflects_exact_of_faithful, CategoryTheory.cokernel_zero_of_nonzero_to_simple, AlgebraicGeometry.Scheme.Modules.instAdditivePushforward, CochainComplex.cm5b, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₁, Ext.biprodAddEquiv_apply_snd, CategoryTheory.ShortComplex.ShortExact.homology_exact₂, 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.mono_of_epi_of_epi_of_mono, TopCat.Presheaf.sections_exact_of_exact, CategoryTheory.ShortComplex.kernelSequence_X₂, DerivedCategory.homologyFunctorFactors_hom_naturality_assoc, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, SpectralObject.sc₁_g, CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, CategoryTheory.ShortExact.reflects_shortExact_of_faithful, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, has_kernels, SpectralObject.kernelSequenceOpcycles_X₃, SpectralObject.opcyclesMap_opcyclesIso_hom, Preradical.toColon_hom_left_app_colonπ_app, CategoryTheory.kernelCokernelCompSequence.ι_φ_assoc, DerivedCategory.left_fac, AlgebraicTopology.normalizedMooreComplex_obj, SpectralObject.dShortComplex_X₁, SpectralObject.opcyclesMap_threeδ₂Toδ₁_opcyclesToE, CategoryTheory.ShortComplex.ShortExact.extClass_comp, CochainComplex.cm5b.I_X, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc_comp_assoc, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff, HomologicalComplex.mono_homologyMap_iff_up_to_refinements, coimIsoIm_inv_app, CategoryTheory.instIsIsoFromLeftDerivedZero', CategoryTheory.kernelCokernelCompSequence.φ_π_assoc, HomologicalComplex.HomologySequence.mapSnakeInput_f₀, CategoryTheory.SpectralSequence.id_hom, SpectralObject.kernelSequenceOpcyclesE_g, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_f, CategoryTheory.ShortComplex.ShortExact.comp_δ_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, CategoryTheory.ObjectProperty.monoModSerre.isoModSerre_factorThruImage, 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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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.ι coimage.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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.π image.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct 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.AbelianStruct

Definitions

Name	Category	Theorems
cokernelCofork 📖	CompOp	2 math math: imageι_π_assoc, imageι_π
image 📖	CompOp	6 math math: fac, imageι_π_assoc, ι_imageπ_assoc, imageι_π, fac_assoc, ι_imageπ
imageIsCokernel 📖	CompOp	—
imageIsKernel 📖	CompOp	—
imageι 📖	CompOp	4 math math: fac, imageι_π_assoc, imageι_π, fac_assoc
imageπ 📖	CompOp	4 math math: fac, ι_imageπ_assoc, fac_assoc, ι_imageπ
isColimitCokernelCofork 📖	CompOp	—
isLimitKernelFork 📖	CompOp	—
kernelFork 📖	CompOp	2 math math: ι_imageπ_assoc, ι_imageπ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image imageπ imageι	—	—
fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image imageπ imageι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fac
imageι_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms cokernelCofork imageι CategoryTheory.Limits.Cofork.π	—	—
imageι_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct image imageι CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms cokernelCofork CategoryTheory.Limits.Cofork.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageι_π
ι_imageπ 📖	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.Preadditive.preadditiveHasZeroMorphisms kernelFork image CategoryTheory.Limits.Fork.ι imageπ	—	—
ι_imageπ_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 CategoryTheory.Preadditive.preadditiveHasZeroMorphisms kernelFork CategoryTheory.Limits.Fork.ι image imageπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_imageπ

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.Preadditive.preadditiveHasZeroMorphisms	—	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.Preadditive.preadditiveHasZeroMorphisms	—	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