Basic

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

Statistics

Metric	Count
Definitions homAddEquiv, coforkOfCokernelCofork, cokernelCoforkOfCofork, compHom, forkOfKernelFork, fullSubcategory, homGroup, inducedCategory, instAddCommGroupEnd, instNegIso, instRingEnd, instSMulUnitsIntIso, instSemiringEnd, isColimitCoforkOfCokernelCofork, isColimitCokernelCoforkOfCofork, isLimitForkOfKernelFork, isLimitKernelForkOfFork, kernelForkOfFork, leftComp, moduleEndRight, preadditiveHasZeroMorphisms, rightComp	22
Theorems homAddEquiv_apply, homAddEquiv_symm_apply_hom, comp_left_eq_zero, comp_right_eq_zero, add_comp, add_comp_assoc, coforkOfCokernelCofork_pt, coforkOfCokernelCofork_π, cokernelCoforkOfCofork_ofπ, cokernelCoforkOfCofork_π, comp_add, comp_add_assoc, comp_neg, comp_neg_assoc, comp_nsmul, comp_sub, comp_sub_assoc, comp_sum, comp_sum_assoc, comp_zsmul, epi_iff_cancel_zero, epi_iff_isZero_cokernel, epi_iff_isZero_cokernel', epi_of_cancel_zero, epi_of_cokernel_iso_zero, epi_of_cokernel_zero, epi_of_isZero_cokernel, epi_of_isZero_cokernel', forkOfKernelFork_pt, forkOfKernelFork_ι, hasCoequalizer_of_hasCokernel, hasCoequalizers_of_hasCokernels, hasCokernel_of_hasCoequalizer, hasEqualizer_of_hasKernel, hasEqualizers_of_hasKernels, hasKernel_of_hasEqualizer, instEpiNegHom, instMonoNegHom, isColimitCoforkOfCokernelCofork_desc, isLimitForkOfKernelFork_lift, kernelForkOfFork_ofι, kernelForkOfFork_ι, mono_iff_cancel_zero, mono_iff_isZero_kernel, mono_iff_isZero_kernel', mono_of_cancel_zero, mono_of_isZero_kernel, mono_of_isZero_kernel', mono_of_kernel_iso_zero, mono_of_kernel_zero, neg_comp, neg_comp_assoc, neg_comp_neg, neg_comp_neg_assoc, neg_iso_hom, neg_iso_inv, nsmul_comp, smul_iso_hom, smul_iso_inv, sub_comp, sub_comp_assoc, sum_comp, sum_comp', sum_comp'_assoc, sum_comp_assoc, zsmul_comp	66
Total	88

CategoryTheory.InducedCategory

Definitions

Name	Category	Theorems
homAddEquiv 📖	CompOp	2 math math: homAddEquiv_symm_apply_hom, homAddEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom CategoryTheory.InducedCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Preadditive.inducedCategory EquivLike.toFunLike AddEquiv.instEquivLike homAddEquiv Hom.hom	—	—
homAddEquiv_symm_apply_hom 📖	mathematical	—	Hom.hom DFunLike.coe AddEquiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.InducedCategory instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Preadditive.inducedCategory EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm homAddEquiv	—	—

CategoryTheory.Preadditive

Definitions

Name	Category	Theorems
coforkOfCokernelCofork 📖	CompOp	3 math math: isColimitCoforkOfCokernelCofork_desc, coforkOfCokernelCofork_π, coforkOfCokernelCofork_pt
cokernelCoforkOfCofork 📖	CompOp	3 math math: isColimitCoforkOfCokernelCofork_desc, cokernelCoforkOfCofork_ofπ, cokernelCoforkOfCofork_π
compHom 📖	CompOp	—
forkOfKernelFork 📖	CompOp	3 math math: forkOfKernelFork_pt, isLimitForkOfKernelFork_lift, forkOfKernelFork_ι
fullSubcategory 📖	CompOp	20 math math: CategoryTheory.Functor.fullSubcategoryInclusionLinear, FDRep.endRingEquiv_symm_comp_ρ, CategoryTheory.Functor.fullSubcategoryInclusion_additive, CategoryTheory.ObjectProperty.instAdditiveFullSubcategoryShiftFunctor, FGModuleCat.instFiniteHom, CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory, FGModuleCat.instAdditiveModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategoryι, FDRep.instHasKernels, FDRep.simple_iff_end_is_rank_one, CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory, FGModuleCat.instLinearModuleCatForget₂LinearMapIdCarrierObjIsFG, CategoryTheory.Functor.instAdditiveFullSubcategoryLift, FDRep.of_ρ, CategoryTheory.ObjectProperty.instIsTriangulatedFullSubcategory, CategoryTheory.instAdditiveAdditiveFunctorFunctorForget, FDRep.endRingEquiv_comp_ρ, FDRep.simple_iff_char_is_norm_one, CategoryTheory.ObjectProperty.isTriangulated_lift, FGModuleCat.instIsIsoCoimageImageComparison
homGroup 📖	CompOp	617 math math: CategoryTheory.ShortComplex.opcyclesMap_smul, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, Rep.resCoindHomEquiv_symm_apply_hom, Rep.resCoindHomEquiv_apply_hom, ext_iff, CategoryTheory.preadditiveCoyonedaObj_map, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, CategoryTheory.sum_whiskerRight, CochainComplex.HomComplex.Cochain.fromSingleMk_neg, CategoryTheory.ShortComplex.homologyMap_smul, CategoryTheory.opHom_apply, hasKernel_of_hasEqualizer, CategoryTheory.ShortComplex.Homotopy.comm₁, CategoryTheory.ShortComplex.Homotopy.comp_h₃, CategoryTheory.linearCoyoneda_map_app, CategoryTheory.Limits.biprod.lift_eq, CategoryTheory.Abelian.Ext.homLinearEquiv_apply, Rep.MonoidalClosed.linearHomEquiv_symm_hom, CochainComplex.HomComplex.Cocycle.fromSingleMk_add, CategoryTheory.ShiftedHom.neg_comp, Action.neg_hom, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p, CategoryTheory.Linear.instMonoHSMulHomOfInvertible, HomologicalComplex.mapBifunctor₁₂.d_eq, CategoryTheory.ShortComplex.homologyMap_add, CategoryTheory.sum_tensor, Action.sum_hom, CategoryTheory.ShortComplex.leftHomologyMap'_sub, CategoryTheory.ShortComplex.Homotopy.sub_h₀, CategoryTheory.Functor.coe_mapLinearMap, prevD_comp_left, CategoryTheory.Idempotents.neg_def, CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH, CategoryTheory.CatCenter.app_sub, CategoryTheory.finrank_hom_simple_simple_le_one, CategoryTheory.ShortComplex.Homotopy.smul_h₁, CategoryTheory.MorphismProperty.LeftFraction₂.map_add, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁, CategoryTheory.ShortComplex.leftHomologyMap_sub, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, CategoryTheory.InducedCategory.homLinearEquiv_apply, CategoryTheory.Abelian.Ext.mk₀_addEquiv₀_apply, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, CategoryTheory.ShortComplex.opcyclesMap_sub, Rep.diagonalHomEquiv_symm_apply, CategoryTheory.ShortComplex.opcyclesMap'_sub, CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ, CategoryTheory.linearYoneda_obj_map, homSelfLinearEquivEndMulOpposite_apply, CategoryTheory.Linear.comp_apply, CategoryTheory.ShiftedHom.opEquiv_symm_add, CategoryTheory.finrank_hom_simple_simple_eq_one_iff, CategoryTheory.ShortComplex.leftHomologyMap'_neg, HomologicalComplex.mapBifunctor₂₃.d₂_eq, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_neg_f, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj, CategoryTheory.Abelian.Ext.smul_hom, sub_comp_assoc, CategoryTheory.Monad.algebraPreadditive_homGroup_sub_f, HomologicalComplex₂.totalAux.d₂_eq, CategoryTheory.ShortComplex.cyclesMap_neg, CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f, CochainComplex.mappingCone.d_snd_v, isColimitCoforkOfCokernelCofork_desc, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, CategoryTheory.MonoidalPreadditive.whiskerLeft_add, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, HomologicalComplex.add_f_apply, CategoryTheory.ShiftedHom.comp_add, AlgebraicGeometry.tilde.map_sub, CochainComplex.HomComplex.Cochain.toSingleMk_neg, HomologicalComplex.mapBifunctor₂₃.d₃_eq, CategoryTheory.leftDistributor_hom, HomologicalComplex₂.D₂_D₁_assoc, CategoryTheory.ShortComplex.cyclesMap_sub, Homotopy.prevD_succ_cochainComplex, CategoryTheory.ProjectiveResolution.sub_extMk, CategoryTheory.ShortComplex.Splitting.id, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, CategoryTheory.ShortComplex.Homotopy.add_h₁, CochainComplex.HomComplex.Cochain.toSingleMk_add, CategoryTheory.Abelian.Ext.mk₀_neg, CategoryTheory.MonoidalPreadditive.add_whiskerRight, CochainComplex.HomComplex.δ_v, CategoryTheory.Idempotents.add_def, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, CategoryTheory.ShortComplex.Homotopy.smul_h₂, CategoryTheory.Subobject.factors_add, CochainComplex.HomComplex.Cochain.neg_v, CochainComplex.HomComplex.Cochain.sub_v, CategoryTheory.Linear.units_smul_comp, CategoryTheory.Linear.leftComp_apply, CochainComplex.mappingCone.liftCochain_v_descCochain_v, CategoryTheory.Functor.Linear.map_smul, CategoryTheory.Limits.IsBilimit.total, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH, HomologicalComplex.mapBifunctorMapHomotopy.comm₁, CategoryTheory.Biprod.unipotentLower_inv, Action.smul_hom, CategoryTheory.ShortComplex.cyclesMap'_sub, CategoryTheory.ShortComplex.homologyMap'_sub, CategoryTheory.ShortComplex.Homotopy.sub_h₁, commGrpEquivalence_functor_obj_grp_mul, CategoryTheory.Limits.IsBilimit.binary_total, CategoryTheory.Idempotents.Karoubi.inclusionHom_apply, CochainComplex.mappingCone.id_X, CategoryTheory.ShortComplex.homologyMap'_add, CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_sub_f, nsmul_comp, CategoryTheory.Localization.Preadditive.add'_map, CategoryTheory.Pretriangulated.Triangle.smul_hom₂, CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f, Rep.MonoidalClosed.linearHomEquivComm_hom, cokernelCoforkOfCofork_ofπ, CategoryTheory.ShortComplex.Homotopy.neg_h₁, CategoryTheory.NatTrans.app_nsmul, HomologicalComplex.sub_f_apply, CochainComplex.mappingCone.d_snd_v'_assoc, comp_neg, CategoryTheory.ShortComplex.add_τ₃, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, CategoryTheory.Monad.algebraPreadditive_homGroup_add_f, FDRep.instFiniteDimensionalHom, CategoryTheory.linearCoyoneda_obj_obj_isAddCommGroup, smul_iso_hom, CategoryTheory.Adjunction.compPreadditiveYonedaIso_inv_app_app_apply, commGrpEquivalence_functor_obj_grp_inv, Rep.coindVEquiv_symm_apply_coe, CategoryTheory.CommSq.shortComplex_f, CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_neg_f, CategoryTheory.Limits.biproduct.matrix_desc_assoc, HomologicalComplex.homologyMap_neg, prevD_eq_toPrev_dTo, neg_iso_hom, CategoryTheory.NatTrans.app_add, CategoryTheory.Abelian.Ext.mk₀_smul, CategoryTheory.ShortComplex.opcyclesMap_add, CategoryTheory.Limits.biprod.decomp_hom_to, CategoryTheory.Biprod.inr_ofComponents, CategoryTheory.Biprod.ofComponents_snd, CategoryTheory.Limits.biproduct.lift_matrix_assoc, CategoryTheory.Limits.biproduct.lift_desc_assoc, Homotopy.dNext_zero_chainComplex, comp_sum_assoc, HomologicalComplex₂.d₁_eq, CategoryTheory.ShortComplex.Homotopy.smul_h₀, Homotopy.prevD_chainComplex, CategoryTheory.ShortComplex.Homotopy.smul_h₃, CochainComplex.HomComplex.Cocycle.toSingleMk_add, CategoryTheory.ShortComplex.cyclesMap_smul, CategoryTheory.CatCenter.app_add, CategoryTheory.Functor.map_add, CategoryTheory.ShortComplex.leftHomologyMap_add, CategoryTheory.InjectiveResolution.add_extMk, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, smul_iso_inv, CategoryTheory.ShortComplex.Homotopy.comm₃, prevD_nat, CategoryTheory.Idempotents.idem_of_id_sub_idem, CategoryTheory.ShortComplex.homologyMap'_neg, CategoryTheory.Functor.map_zsmul, FGModuleCat.instFiniteHom, CategoryTheory.Pretriangulated.Triangle.rotate_mor₃, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_neg_f, neg_comp_neg_assoc, kernelForkOfFork_ofι, neg_comp_neg, CategoryTheory.Pretriangulated.Triangle.sub_hom₁, CochainComplex.HomComplex.Cochain.fromSingleMk_add, CategoryTheory.finrank_endomorphism_eq_one, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum, CategoryTheory.linearYoneda_map_app, CategoryTheory.ShortComplex.Splitting.g_s, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, CategoryTheory.Adjunction.homAddEquiv_sub, forkOfKernelFork_pt, HomologicalComplex.units_smul_f_apply, sum_comp, CategoryTheory.linearYoneda_obj_obj_isAddCommGroup, CochainComplex.HomComplex.Cochain.leftUnshift_v, CategoryTheory.Limits.biprod.decomp_hom_from, CategoryTheory.Functor.map_smul, CategoryTheory.Functor.Additive.map_add, CategoryTheory.Limits.biprod.desc_eq, Homotopy.nullHomotopicMap_f, CategoryTheory.Limits.biproduct.lift_desc, CategoryTheory.MonoidalPreadditive.add_tensor, CategoryTheory.ShortComplex.opcyclesMap_neg, Rep.resIndAdjunction_homEquiv_symm_apply, CategoryTheory.ShortComplex.Homotopy.symm_h₀, CategoryTheory.rightDistributor_inv, Action.nsmul_hom, CategoryTheory.ShortComplex.nullHomotopic_τ₁, HomologicalComplex₂.totalAux.d₂_eq', Rep.coindMap'_hom, CategoryTheory.Functor.map_sub, HomologicalComplex₂.totalAux.d₁_eq, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, CategoryTheory.Abelian.Ext.mk₀_add, prevD_eq, comp_neg_assoc, HomologicalComplex.mapBifunctor.d₂_eq, CategoryTheory.Limits.biprod.total, HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc, CategoryTheory.ProjectiveResolution.add_extMk, Rep.freeLiftLEquiv_apply, CategoryTheory.ShortComplex.rightHomologyMap'_add, HomologicalComplex.zsmul_f_apply, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zsmul_f, instMonoNegHom, HomologicalComplex.homologyMap_add, CategoryTheory.Pretriangulated.Triangle.neg_hom₁, Action.sub_hom, HomologicalComplex.nsmul_f_apply, CategoryTheory.Pretriangulated.Triangle.neg_hom₃, CategoryTheory.Linear.comp_units_smul, prevD_eq_zero, CategoryTheory.finrank_hom_simple_simple_eq_zero_iff, CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso, CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom, Rep.resIndAdjunction_homEquiv_apply, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, cokernelCoforkOfCofork_π, CategoryTheory.ShortComplex.smul_τ₃, CategoryTheory.ShortComplex.homologyMap_neg, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, CochainComplex.mappingCone.decomp_from, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, CategoryTheory.ShortComplex.nullHomotopic_τ₂, HomologicalComplex.homotopyCofiber.d_fstX, CategoryTheory.unop_neg, CategoryTheory.Pretriangulated.Triangle.invRotate_mor₁, CategoryTheory.Biprod.ofComponents_comp, CategoryTheory.ShortComplex.Homotopy.symm_h₃, Rep.leftRegularHomEquiv_symm_apply, CategoryTheory.Adjunction.homAddEquiv_add, CategoryTheory.endomorphism_simple_eq_smul_id, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH, CategoryTheory.ShiftedHom.comp_neg, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, Rep.coindResAdjunction_homEquiv_apply, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, CategoryTheory.Abelian.Ext.homAddEquiv_apply, CategoryTheory.unop_add, kernelForkOfFork_ι, CategoryTheory.ShortComplex.Homotopy.comp_h₁, CategoryTheory.Functor.coe_mapAddHom, CategoryTheory.ShiftedHom.comp_smul, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, CategoryTheory.Abelian.Ext.mk₀_sum, CochainComplex.mappingCone.d_snd_v_assoc, Representation.coind'_apply_apply, CochainComplex.shiftFunctor_map_f, CochainComplex.mappingCone.d_snd_v', CategoryTheory.ShortComplex.Homotopy.sub_h₃, CategoryTheory.ShortComplex.Homotopy.trans_h₂, CategoryTheory.ShortComplex.nullHomotopic_τ₃, HomologicalComplex.mapBifunctor.d_eq, CategoryTheory.Limits.biprod.map_eq, Rep.coindIso_inv_hom_hom, CochainComplex.mappingCone.d_fst_v_assoc, CategoryTheory.tensor_sum, CategoryTheory.unopHom_apply, CategoryTheory.InducedCategory.homAddEquiv_apply, CategoryTheory.Adjunction.compPreadditiveYonedaIso_hom_app_app_apply, CategoryTheory.Abelian.Ext.add_hom, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CategoryTheory.ShortComplex.sub_τ₁, CategoryTheory.Mat_.add_apply, CategoryTheory.Linear.homCongr_apply, CategoryTheory.ShortComplex.Homotopy.add_h₀, dNext_comp_left, CategoryTheory.ShortComplex.cyclesMap'_smul, CategoryTheory.Idempotents.Karoubi.sum_hom, HomologicalComplex.homotopyCofiber.inlX_d, HomologicalComplex.mapBifunctor₂₃.d₁_eq, CochainComplex.HomComplex.Cocycle.fromSingleMk_neg, CategoryTheory.Monad.algebraPreadditive_homGroup_zsmul_f, comp_sum, Representation.linHom.invariantsEquivRepHom_symm_apply_coe, Homotopy.symm_hom, CategoryTheory.Linear.comp_smul, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, comp_zsmul, CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zsmul_f, CategoryTheory.ShiftedHom.mk₀_add, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, add_comp, HomologicalComplex.homologyMap_sub, add_comp_assoc, Homotopy.dNext_succ_chainComplex, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_f, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH, CategoryTheory.ShiftedHom.add_comp, CategoryTheory.Adjunction.homAddEquiv_symm_neg, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_nsmul_f, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, CochainComplex.HomComplex.δ_zero_cochain_v, CochainComplex.HomComplex.Cochain.units_smul_v, HomologicalComplex.smul_f_apply, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, CategoryTheory.NatTrans.app_sum, CategoryTheory.Limits.biproduct.total, coforkOfCokernelCofork_π, CategoryTheory.ShortComplex.rightHomologyMap_sub, CategoryTheory.Functor.map_units_smul, hasCokernel_of_hasCoequalizer, CategoryTheory.Limits.biprod.add_eq_lift_desc_id, CategoryTheory.ShortComplex.Splitting.g_s_assoc, Action.add_hom, CategoryTheory.NatTrans.appHom_apply, CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f, CategoryTheory.Limits.biproduct.matrix_desc, Homotopy.add_hom, CochainComplex.mappingCone.inl_v_d_assoc, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, AlgebraicGeometry.Scheme.Modules.Hom.sub_app, CategoryTheory.InjectiveResolution.sub_extMk, CategoryTheory.ShortComplex.sub_τ₂, CategoryTheory.op_add, CategoryTheory.ShortComplex.Homotopy.trans_h₃, CategoryTheory.ShortComplex.rightHomologyMap'_sub, CategoryTheory.ShortComplex.Homotopy.neg_h₃, CategoryTheory.ShortComplex.homologyMap_sub, CategoryTheory.linearCoyoneda_obj_map, FDRep.simple_iff_end_is_rank_one, CategoryTheory.ShortComplex.Homotopy.trans_h₀, CategoryTheory.ShortComplex.neg_τ₂, CategoryTheory.kernelCokernelCompSequence.δ_fac, CochainComplex.HomComplex.Cochain.smul_v, HomologicalComplex.homotopyCofiber.d_sndX, sum_comp_assoc, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, SimplicialObject.Splitting.decomposition_id, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, CochainComplex.HomComplex.Cochain.fromSingleMk_sub, CategoryTheory.ShortComplex.homologyMap'_smul, Rep.coindResAdjunction_homEquiv_symm_apply, CategoryTheory.Pretriangulated.Triangle.neg_hom₂, CategoryTheory.op_sum, CategoryTheory.Biprod.ofComponents_fst, CategoryTheory.Biprod.unipotentUpper_inv, CategoryTheory.preadditiveYonedaObj_obj_isAddCommGroup, CategoryTheory.ShiftedHom.opEquiv'_symm_add, Rep.coindVEquiv_apply_hom, AlgebraicGeometry.Scheme.Modules.Hom.add_app, AlgebraicTopology.DoldKan.hσ'_eq, HomologicalComplex₂.d₂_eq, CategoryTheory.Monad.algebraPreadditive_homGroup_nsmul_f, CochainComplex.HomComplex.Cocycle.toSingleMk_sub, CategoryTheory.ShortComplex.Homotopy.neg_h₀, HomologicalComplex₂.D₂_D₁, CategoryTheory.Pretriangulated.Triangle.add_hom₂, CategoryTheory.ShortComplex.add_τ₂, CochainComplex.HomComplex.Cocycle.fromSingleMk_sub, CategoryTheory.Pretriangulated.Triangle.add_hom₃, CategoryTheory.CatCenter.app_neg_one_zpow, CategoryTheory.ShortComplex.rightHomologyMap_add, homSelfLinearEquivEndMulOpposite_symm_apply, CochainComplex.mappingCone.decomp_to, CategoryTheory.CommSq.shortComplex'_g, Rep.leftRegularHomEquiv_symm_single, inhomogeneousCochains.d_eq, CategoryTheory.Adjunction.homAddEquiv_symm_apply, CategoryTheory.NatTrans.appLinearMap_apply, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zsmul_f, HomologicalComplex₂.D₁_D₂_assoc, CategoryTheory.Adjunction.homAddEquiv_symm_add, Homotopy.trans_hom, CategoryTheory.Idempotents.Karoubi.complement_p, CategoryTheory.ShiftedHom.map_smul, CochainComplex.mappingCone.lift_desc_f, CategoryTheory.Limits.biproduct.lift_matrix, CategoryTheory.Free.lift_map_single, CategoryTheory.Idempotents.Karoubi.zsmul_hom, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CategoryTheory.ShortComplex.Homotopy.add_h₂, CategoryTheory.Functor.mapAddHom_apply, CategoryTheory.Abelian.Ext.smul_eq_comp_mk₀, CategoryTheory.ShortComplex.Splitting.r_f, AlgebraicGeometry.tilde.map_add, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.mappingCone.desc_f, CochainComplex.mappingCone.d_fst_v'_assoc, comp_add, CategoryTheory.Abelian.Ext.addEquiv₀_symm_apply, dNext_eq_dFrom_fromNext, sum_comp'_assoc, CochainComplex.mappingCone.inl_v_d, CategoryTheory.Linear.homCongr_symm_apply, CategoryTheory.ShortComplex.Homotopy.comp_h₀, CategoryTheory.Adjunction.homAddEquiv_neg, CategoryTheory.Limits.biproduct.desc_eq, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃, CategoryTheory.Limits.biprod.lift_desc_assoc, isLimitForkOfKernelFork_lift, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK, inv_def, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, ChainComplex.linearYonedaObj_d, CategoryTheory.ShortComplex.Homotopy.symm_h₂, Action.zsmul_hom, neg_comp, CategoryTheory.Abelian.Ext.neg_hom, Homotopy.smul_hom, Homotopy.prevD_zero_cochainComplex, CategoryTheory.Pretriangulated.Triangle.add_hom₁, mul_def, Rep.MonoidalClosed.linearHomEquiv_hom, CategoryTheory.ShortComplex.Homotopy.sub_h₂, CategoryTheory.MonoidalLinear.smul_whiskerRight, CategoryTheory.Mat_.comp_apply, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, CategoryTheory.MonoidalLinear.whiskerLeft_smul, CochainComplex.HomComplex.Cocycle.toSingleMk_neg, CochainComplex.mappingCone.d_fst_v', CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Homotopy.comm, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, CategoryTheory.ShortComplex.Homotopy.trans_h₁, HomologicalComplex.mapBifunctor.d₁_eq', CategoryTheory.ShortComplex.Homotopy.comm₂, CategoryTheory.ShortComplex.sub_τ₃, Homotopy.comp_hom, dNext_eq, CategoryTheory.op_zsmul, CochainComplex.shiftFunctor_obj_d', CategoryTheory.Pretriangulated.Triangle.smul_hom₃, AlgebraicTopology.DoldKan.N₂_obj_X_d, CategoryTheory.ShortComplex.RightHomologyMapData.add_φH, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, CategoryTheory.Pretriangulated.Triangle.sub_hom₃, CategoryTheory.ShortComplex.rightHomologyMap_neg, CategoryTheory.Limits.biproduct.lift_eq, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f, HomologicalComplex.mapBifunctor₂₃.d_eq, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ, CategoryTheory.NatTrans.app_smul, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, HomologicalComplex.homotopyCofiber.inlX_d_assoc, HomologicalComplex.homotopyCofiber.desc_f, CategoryTheory.Free.lift_map, CategoryTheory.ShiftedHom.map_add, HomologicalComplex.ι_mapBifunctorFlipIso_hom, CategoryTheory.ShortComplex.rightHomologyMap'_neg, CategoryTheory.InjectiveResolution.neg_extMk, CategoryTheory.Functor.map_neg, CategoryTheory.Abelian.Ext.mk₀_linearEquiv₀_apply, CategoryTheory.Limits.biprod.add_eq_lift_id_desc, CategoryTheory.ShortComplex.Splitting.r_f_assoc, CategoryTheory.leftDistributor_inv, CategoryTheory.Pretriangulated.Triangle.sub_hom₂, CategoryTheory.Linear.instEpiHSMulHomOfInvertible, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, Rep.leftRegularHomEquiv_apply, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_add_f, CategoryTheory.IsPushout.hom_eq_add_up_to_refinements, comp_nsmul, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, forkOfKernelFork_ι, HomologicalComplex.mapBifunctor.d₂_eq', prevD_comp_right, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, HomologicalComplex₂.total_d, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, CategoryTheory.Monad.algebraPreadditive_homGroup_neg_f, CategoryTheory.ShortComplex.Homotopy.comp_h₂, CategoryTheory.unop_zsmul, CategoryTheory.Sheaf.Hom.add_app, CategoryTheory.NatTrans.app_units_zsmul, CategoryTheory.ShortComplex.cyclesMap'_add, CategoryTheory.whiskerLeft_sum, CategoryTheory.ShortComplex.neg_τ₁, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK, CategoryTheory.rightDistributor_hom, ModuleCat.ofHom₂_compr₂, CategoryTheory.ShortComplex.Homotopy.neg_h₂, CategoryTheory.MonoidalPreadditive.tensor_add, CategoryTheory.finrank_endomorphism_simple_eq_one, HomologicalComplex₂.d₂_eq', CategoryTheory.ShortComplex.smul_τ₁, CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂, Homotopy.dNext_cochainComplex, Homotopy.nullHomotopicMap'_f, CategoryTheory.ShortComplex.smul_τ₂, CategoryTheory.Abelian.Ext.linearEquiv₀_symm_apply, CategoryTheory.ShiftedHom.mk₀_neg, Rep.diagonalHomEquiv_apply, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_nsmul_f, dNext_comp_right, CategoryTheory.Adjunction.homAddEquiv_apply, CategoryTheory.Functor.linear_iff, CategoryTheory.ShortComplex.Homotopy.add_h₃, HomologicalComplex₂.d₁_eq', CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_add_f, Rep.freeLiftLEquiv_symm_apply, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum, CategoryTheory.ShortComplex.cyclesMap'_neg, CategoryTheory.op_neg, AlgebraicTopology.DoldKan.decomposition_Q, Rep.MonoidalClosed.linearHomEquivComm_symm_hom, CategoryTheory.ShortComplex.opcyclesMap'_add, CategoryTheory.op_sub, CategoryTheory.ShortComplex.rightHomologyMap'_smul, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, zsmul_comp, CategoryTheory.ShortComplex.neg_τ₃, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, Rep.indResHomEquiv_apply_hom, CategoryTheory.Adjunction.homAddEquiv_symm_sub, HomologicalComplex₂.D₁_totalShift₂XIso_hom, comp_sub_assoc, AlgebraicGeometry.tilde.map_neg, HomologicalComplex.mapBifunctor₁₂.d₁_eq, HomologicalComplex₂.D₂_totalShift₂XIso_hom, CategoryTheory.ShortComplex.rightHomologyMap_smul, CategoryTheory.Abelian.Ext.homLinearEquiv_symm_apply, CategoryTheory.NatTrans.app_zsmul, CategoryTheory.Mat_.comp_def, CategoryTheory.Biprod.inl_ofComponents, CategoryTheory.Limits.biproduct.map_eq, comp_sub, CategoryTheory.Functor.map_nsmul, ContinuousCohomology.MultiInd.d_succ, HomologicalComplex.mapBifunctor₁₂.d₃_eq, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc, CategoryTheory.Linear.toCatCenter_apply_app, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_add_f, CategoryTheory.CatCenter.app_neg, HomologicalComplex.homotopyCofiber.d_sndX_assoc, FDRep.scalar_product_char_eq_finrank_equivariant, dNext_nat, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_sub_f, HomologicalComplex.neg_f_apply, CategoryTheory.ProjectiveResolution.neg_extMk, CategoryTheory.Localization.Preadditive.map_add, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_nsmul_f, HomologicalComplex.mapBifunctor₁₂.d₂_eq, Representation.linHom.invariantsEquivRepHom_apply_hom, CategoryTheory.unop_sub, dNext_eq_zero, CochainComplex.mappingCone.lift_f, HomologicalComplex₂.totalAux.d₁_eq', CategoryTheory.ShortComplex.add_τ₁, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom, HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc, CochainComplex.HomComplex.CohomologyClass.toHom_mk, CochainComplex.HomComplex.Cochain.add_v, comp_add_assoc, Rep.coindIso_hom_hom_hom, CategoryTheory.preadditiveCoyonedaObj_obj_isAddCommGroup, CategoryTheory.ShortComplex.Homotopy.symm_h₁, CategoryTheory.NatTrans.app_sub, AlgebraicTopology.DoldKan.P_add_Q_f, CategoryTheory.ShiftedHom.smul_comp, CategoryTheory.NatTrans.app_neg, AlgebraicTopology.DoldKan.hσ'_eq', sum_comp', HomologicalComplex₂.D₁_D₂, CochainComplex.HomComplex.Cochain.toSingleMk_sub, CategoryTheory.unop_sum, CategoryTheory.ShortComplex.leftHomologyMap'_add, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst, CategoryTheory.Linear.rightComp_apply, CategoryTheory.ShiftedHom.mk₀_smul, CategoryTheory.ShortComplex.opcyclesMap'_neg, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, HomologicalComplex.mapBifunctor.d₁_eq, sub_comp, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, neg_comp_assoc, CategoryTheory.Limits.biprod.lift_desc, instEpiNegHom, neg_iso_inv, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, CategoryTheory.Linear.smul_comp, CategoryTheory.Pretriangulated.Triangle.smul_hom₁, CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ, CategoryTheory.ShortComplex.leftHomologyMap_smul, HomologicalComplex.homotopyCofiber.d_fstX_assoc, CategoryTheory.ShortComplex.opcyclesMap'_smul, HomologicalComplex.Hom.fAddMonoidHom_apply, CochainComplex.shiftFunctor_obj_d, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f, CategoryTheory.ShortComplex.leftHomologyMap'_smul, CategoryTheory.ShortComplex.cyclesMap_add, CochainComplex.mappingCone.d_fst_v, CategoryTheory.ObjectProperty.smul_mem_trW_iff, CategoryTheory.Functor.map_sum, Rep.indResHomEquiv_symm_apply_hom, coforkOfCokernelCofork_pt, HomologicalComplex.ι_mapBifunctorFlipIso_inv, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, CategoryTheory.Functor.mapLinearMap_apply, CategoryTheory.ShortComplex.leftHomologyMap_neg, FDRep.finrank_hom_simple_simple, CategoryTheory.preadditiveYonedaObj_map, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
inducedCategory 📖	CompOp	6 math math: CategoryTheory.InducedCategory.homLinearEquiv_apply, CategoryTheory.Functor.inducedFunctorLinear, CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom, CategoryTheory.InducedCategory.homAddEquiv_apply, CategoryTheory.InducedCategory.homLinearEquiv_symm_apply_hom, CategoryTheory.Functor.inducedFunctor_additive
instAddCommGroupEnd 📖	CompOp	1 math math: CategoryTheory.CatCenter.app_neg
instNegIso 📖	CompOp	2 math math: neg_iso_hom, neg_iso_inv
instRingEnd 📖	CompOp	56 math math: CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d, CategoryTheory.preadditiveCoyonedaObj_map, CategoryTheory.additive_yonedaObj, CategoryTheory.CatCenter.app_sub, FDRep.endRingEquiv_symm_comp_ρ, homSelfLinearEquivEndMulOpposite_apply, CategoryTheory.preadditiveYonedaObj_obj_carrier, ModuleCat.endRingEquiv_symm_apply_hom, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.full, CategoryTheory.HomOrthogonal.matrixDecomposition_id, CategoryTheory.preadditiveYoneda_obj, CategoryTheory.preadditiveYonedaMap_app, CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj, CategoryTheory.CatCenter.app_add, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d, CategoryTheory.Abelian.full_comp_preadditiveCoyonedaObj, CategoryTheory.preadditiveYonedaObj_obj_isModule, CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj', CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesInjectiveObjects, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective, CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective, CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, CategoryTheory.preservesLimits_preadditiveYonedaObj, CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, CategoryTheory.preadditiveYonedaObj_obj_isAddCommGroup, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, CategoryTheory.CatCenter.app_neg_one_zpow, CategoryTheory.CatCenter.localization_zero, homSelfLinearEquivEndMulOpposite_symm_apply, CategoryTheory.isCoseparator_iff_faithful_preadditiveYonedaObj, Rep.Action_ρ_eq_ρ, CategoryTheory.Abelian.preadditiveCoyonedaObj_map_surjective, CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj, FDRep.of_ρ, CategoryTheory.IsGrothendieckAbelian.GabrielPopescu.preservesFiniteLimits, CategoryTheory.preadditiveCoyonedaObj_obj_carrier, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, CategoryTheory.preadditiveCoyonedaObj_obj_isModule, CategoryTheory.preservesLimits_preadditiveCoyonedaObj, ModuleCat.endRingEquiv_apply, CategoryTheory.additive_coyonedaObj, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.ι_d_assoc, Rep.ihom_obj_ρ, CategoryTheory.CommShift₂Setup.int_ε, CategoryTheory.preadditiveCoyoneda_obj, CategoryTheory.preadditiveCoyonedaObj_obj_isAddCommGroup, CategoryTheory.CatCenter.localization_add, FDRep.endRingEquiv_comp_ρ, CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj, CategoryTheory.CommShift₂Setup.int_z, CategoryTheory.preadditiveYonedaObj_map
instSMulUnitsIntIso 📖	CompOp	4 math math: smul_iso_hom, smul_iso_inv, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso
instSemiringEnd 📖	CompOp	14 math math: FDRep.endRingEquiv_symm_comp_ρ, homSelfLinearEquivEndMulOpposite_apply, CategoryTheory.Linear.smulOfRingMorphism_smul_eq', ModuleCat.smul_naturality, CategoryTheory.Linear.smulOfRingMorphism_smul_eq, ModuleCat.smulNatTrans_apply_app, ModuleCat.HasColimit.coconePointSMul_apply, ModuleCat.mkOfSMul_smul, homSelfLinearEquivEndMulOpposite_symm_apply, Rep.Action_ρ_eq_ρ, FDRep.of_ρ, CategoryTheory.Linear.toCatCenter_apply_app, Rep.ihom_obj_ρ, FDRep.endRingEquiv_comp_ρ
isColimitCoforkOfCokernelCofork 📖	CompOp	1 math math: isColimitCoforkOfCokernelCofork_desc
isColimitCokernelCoforkOfCofork 📖	CompOp	—
isLimitForkOfKernelFork 📖	CompOp	1 math math: isLimitForkOfKernelFork_lift
isLimitKernelForkOfFork 📖	CompOp	—
kernelForkOfFork 📖	CompOp	3 math math: kernelForkOfFork_ofι, kernelForkOfFork_ι, isLimitForkOfKernelFork_lift
leftComp 📖	CompOp	—
moduleEndRight 📖	CompOp	2 math math: CategoryTheory.preadditiveYonedaObj_obj_isModule, CategoryTheory.preadditiveYonedaObj_map
preadditiveHasZeroMorphisms 📖	CompOp	2420 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, HomotopyCategory.spectralObjectMappingCone_δ'_app, CategoryTheory.ShortComplex.opcyclesMap_smul, CategoryTheory.InjectiveResolution.Hom.hom'_f, groupHomology.mapShortComplexH2_τ₁, CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, groupCohomology.mapShortComplexH1_τ₂, CategoryTheory.ShortComplex.SnakeInput.epi_L₃_g, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, CochainComplex.triangleOfDegreewiseSplit_obj₁, groupHomology.π_comp_H2Iso_hom_assoc, CategoryTheory.ShortComplex.SnakeInput.L₀'_exact, CategoryTheory.ShortComplex.Homotopy.h₀_f_assoc, CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, HomologicalComplex₂.totalAux.ιMapObj_D₁, CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, TopModuleCat.hom_zero, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂, AlgebraicTopology.DoldKan.P_f_0_eq, CategoryTheory.ShortComplex.Splitting.exact, CategoryTheory.ObjectProperty.isoModSerre_zero_iff, homotopyEquivalences_le_quasiIso, CategoryTheory.ShortComplex.SnakeInput.w₀₂_assoc, CategoryTheory.kernelUnopOp_inv, ModuleCat.biproductIsoPi_inv_comp_π, simple_of_finrank_eq_one, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app', CategoryTheory.Limits.inr_of_isLimit, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, CategoryTheory.ShortComplex.Homotopy.refl_h₀, CategoryTheory.CommSq.shortComplex_g, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, IsIso.comp_left_eq_zero, CochainComplex.HomComplex.Cochain.fromSingleMk_neg, CategoryTheory.ShortComplex.homologyMap_smul, CochainComplex.mappingCone.δ_inl, CochainComplex.mappingCone.inl_v_descCochain_v_assoc, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁, hasKernel_of_hasEqualizer, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, HomologicalComplex.rightUnitor'_inv, CategoryTheory.ShortComplex.Homotopy.comm₁, HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.ShortComplex.Homotopy.comp_h₃, groupCohomology.toCocycles_comp_isoCocycles₁_hom, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, CategoryTheory.ShortComplex.Splitting.op_r, CategoryTheory.Limits.biprod.lift_eq, CategoryTheory.ShortComplex.SnakeInput.op_δ, CategoryTheory.Idempotents.Karoubi.karoubi_hasFiniteBiproducts, DerivedCategory.right_fac, CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc, groupCohomology.isoCocycles₁_hom_comp_i_apply, AddCommGrpCat.biproductIsoPi_inv_comp_π_apply, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, HomologicalComplex₂.totalFlipIso_hom_f_D₁, commGrpEquivalence_functor_obj_grp_one, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p, ModuleCat.cokernel_π_ext, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, groupHomology.mapShortComplexH2_id, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, CategoryTheory.ObjectProperty.instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt, CategoryTheory.ShortComplex.SnakeInput.naturality_δ, CochainComplex.mappingCone.inr_f_d_assoc, CategoryTheory.ShortComplex.SnakeInput.functorL₁_obj, CategoryTheory.ShortComplex.cyclesFunctor_linear, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_K, CategoryTheory.ShortComplex.homologyMap_add, AlgebraicTopology.NormalizedMooreComplex.obj_d, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃, groupHomology.shortComplexH1_f, CategoryTheory.biproduct_ι_comp_rightDistributor_inv, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, CochainComplex.HomComplex.Cochain.δ_single, CategoryTheory.ShortComplex.leftHomologyMap'_sub, CochainComplex.mappingConeCompTriangle_obj₂, groupCohomology.inhomogeneousCochains.d_def, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_obj, CategoryTheory.ShortComplex.Homotopy.sub_h₀, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, AlgebraicTopology.DoldKan.N₁_map_f, CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, CochainComplex.isStrictlyGE_shift, prevD_comp_left, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, CochainComplex.mappingCone.id, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_apply, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH, CategoryTheory.ShortComplex.SnakeInput.L₃_exact, CategoryTheory.Abelian.Pseudoelement.pseudoZero_def, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, CochainComplex.shiftFunctorZero_eq, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₂, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, groupCohomology.cocyclesIso₀_hom_comp_f, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, TopModuleCat.hom_zero_apply, CochainComplex.mappingCone.liftCochain_v_snd_v_assoc, groupCohomology.eq_d₀₁_comp_inv, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂, CochainComplex.mappingCone.inr_f_fst_v, CategoryTheory.ShortComplex.Homotopy.smul_h₁, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, CategoryTheory.indecomposable_of_simple, CategoryTheory.ShortComplex.HomotopyEquiv.trans_hom, groupHomology.mapShortComplexH1_zero, CategoryTheory.ShortComplex.cokernelSequence_f, CochainComplex.HomComplex.Cochain.leftShift_smul, HomologicalComplex.homotopyCofiber.inlX_fstX, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, groupCohomology.π_comp_H1Iso_hom_assoc, CategoryTheory.ShiftedHom.mk₀_zero, Homotopy.homologyMap_eq, HomologicalComplex.homotopyCofiber.inrX_fstX_assoc, CategoryTheory.ShortComplex.leftHomologyMap_sub, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, groupHomology.mapShortComplexH2_zero, groupCohomology.eq_d₁₂_comp_inv, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply, Homotopy.nullHomotopicMap_comp, CategoryTheory.ShortComplex.moduleCatMk_X₁_carrier, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inl, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, groupCohomology.mapCocycles₂_comp_i, CochainComplex.mappingCone.triangle_mor₁, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, groupHomology.H1CoresCoinf_exact, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, AlgebraicTopology.DoldKan.identity_N₂, groupHomology.eq_d₃₂_comp_inv, CategoryTheory.ShortComplex.Splitting.homologyData_right, CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up, HomologicalComplex₂.shiftFunctor₂XXIso_refl, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, CategoryTheory.ShortComplex.Splitting.map_s, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, CategoryTheory.ShortComplex.moduleCatMk_X₁_isAddCommGroup, CategoryTheory.ShortComplex.SnakeInput.L₁_exact, CochainComplex.mappingCone.liftCochain_v_snd_v, CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f', CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, CategoryTheory.Limits.BinaryBicone.ofLimitCone_inl, groupHomology.chainsMap_id, HomologicalComplex.leftUnitor'_inv_comm, CategoryTheory.ShortComplex.instIsNormalEpiCategory, SimplicialObject.Splitting.PInfty_comp_πSummand_id, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, Rep.barComplex.d_def, CategoryTheory.ShortComplex.opcyclesMap_sub, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃, DerivedCategory.HomologySequence.comp_δ, CategoryTheory.ShortComplex.opcyclesMap'_sub, groupCohomology.H0IsoOfIsTrivial_hom, CategoryTheory.rightDistributor_ext₂_right_iff, CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ, CategoryTheory.Functor.mapHomologicalComplex_linear, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, HomotopyCategory.isZero_quotient_obj_iff, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Functor.homologySequence_comp_assoc, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, CategoryTheory.ShortComplex.Homotopy.unop_h₂, CategoryTheory.Functor.mapHomotopyEquiv_inv, AlgebraicTopology.DoldKan.PInfty_idem, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, CategoryTheory.ShortComplex.Splitting.mono_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.ShortComplex.leftHomologyMap'_neg, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_g, CategoryTheory.ShortComplex.ext_mk₀_f_comp_ext_mk₀_g, HomologicalComplex₂.total.mapIso_hom, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂, DoldKan.equivalence_unitIso, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₂, CochainComplex.instLinearIntFunctorSingleFunctors, groupHomology.comp_d₂₁_eq, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, CategoryTheory.ShortComplex.Splitting.s_g, CategoryTheory.ShortComplex.moduleCatMk_X₂_isModule, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, Homotopy.nullHomotopicMap_f_eq_zero, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, CategoryTheory.kernelCokernelCompSequence.inl_π_assoc, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, HomologicalComplex.eq_liftCycles_homologyπ_up_to_refinements, HomologicalComplex₂.totalAux.d₂_eq, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₃, CategoryTheory.ShortComplex.cyclesMap_neg, groupHomology.H1CoresCoinf_X₃, CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f, CochainComplex.mappingCone.d_snd_v, isColimitCoforkOfCokernelCofork_desc, groupCohomology.mapShortComplexH1_τ₃, CochainComplex.HomComplex.Cochain.rightUnshift_neg, HomologicalComplex.instIsNormalEpiCategory, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, CochainComplex.HomComplex.Cochain.δ_fromSingleMk, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₃, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyHomInvId, AlgebraicTopology.DoldKan.QInfty_idem, CochainComplex.HomComplex.Cochain.map_v, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, HomologicalComplex.add_f_apply, CategoryTheory.cokernelUnopUnop_inv, CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive, groupCohomology.cochainsMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, AlgebraicGeometry.Scheme.Modules.Hom.zero_app, CategoryTheory.Functor.map_homogical_complex_additive, CochainComplex.HomComplex.leftHomologyData_K_coe, CochainComplex.mappingConeCompTriangle_mor₃, groupCohomology.comp_d₁₂_eq, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, HomologicalComplex₂.d₁_eq_zero', CochainComplex.HomComplex.Cochain.shift_add, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, HomologicalComplex₂.D₁_D₁_assoc, CategoryTheory.ShortComplex.Homotopy.compLeft_h₂, CategoryTheory.Functor.homologySequence_comp, HomologicalComplex₂.total.mapAux.mapMap_D₁_assoc, CategoryTheory.kernelOpUnop_hom, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₁, CategoryTheory.InjectiveResolution.of_def, Homotopy.extend_hom_eq, CochainComplex.HomComplex.Cochain.comp_id, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_I, DoldKan.equivalence_functor, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁, groupHomology.π_comp_H1Iso_inv, CategoryTheory.ShortComplex.Homotopy.op_h₀, CategoryTheory.ShortComplex.moduleCatMk_g, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, HomologicalComplex.homotopyCofiber.inrX_sndX_assoc, CategoryTheory.ProjectiveResolution.cochainComplex_d, CochainComplex.HomComplex.Cochain.toSingleMk_neg, CategoryTheory.ObjectProperty.prop_biprod, IsIso.comp_right_eq_zero, CochainComplex.HomComplex.Cochain.ofHom_v_comp_d, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_ι_f, groupHomology.isoCycles₁_inv_comp_iCycles_apply, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality, groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_mono₂, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, CochainComplex.HomComplex.Cochain.map_zero, CategoryTheory.InjectiveResolution.instIsLECochainComplexOfNatInt, CochainComplex.cm5b.fac, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃_assoc, groupCohomology.dArrowIso₀₁_inv_right, groupCohomology.map_H0Iso_hom_f_apply, ModuleCat.shortExact_projectiveShortComplex, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₁, CochainComplex.HomComplex.Cochain.toSingleMk_v, groupCohomology.eq_d₂₃_comp_inv_assoc, CategoryTheory.ShortComplex.SnakeInput.op_L₂, CochainComplex.HomComplex.leftHomologyData'_i, CategoryTheory.ShortComplex.HomologyMapData.add_left, CategoryTheory.Limits.HasBiproduct.of_hasProduct, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃, HomologicalComplex₂.D₁_D₁, CochainComplex.IsKInjective.rightOrthogonal, groupCohomology.eq_d₂₃_comp_inv_apply, CategoryTheory.leftDistributor_hom, groupCohomology.eq_d₁₂_comp_inv_apply, groupHomology.mapShortComplexH1_τ₂, HomologicalComplex.homotopyCofiber.desc_f', HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, HomotopyCategory.quotient_inverts_homotopyEquivalences, HomologicalComplex₂.D₂_D₁_assoc, CochainComplex.IsKInjective.Qh_map_bijective, CategoryTheory.ShortComplex.Homotopy.op_h₂, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd, CategoryTheory.ShortComplex.SnakeInput.op_v₁₂, CategoryTheory.ShortComplex.SnakeInput.id_f₂, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, Rep.standardComplex.d_eq, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CochainComplex.HomComplex.Cochain.shift_neg, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.HomologySequence.exact₂, CategoryTheory.ShortComplex.cyclesMap_sub, HomologicalComplex₂.D₂_D₂, CategoryTheory.IsPullback.exact_shortComplex', CategoryTheory.ShortComplex.Homotopy.g_h₃_assoc, CategoryTheory.Pretriangulated.instHasBinaryBiproducts, Homotopy.prevD_succ_cochainComplex, CategoryTheory.Abelian.coim_map, CategoryTheory.biproduct_ι_comp_rightDistributor_hom, HomologicalComplex₂.ιTotalOrZero_map_assoc, CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc, CategoryTheory.ShortComplex.Splitting.id, HomologicalComplex₂.ιTotal_map, CochainComplex.homotopyUnop_hom_eq, CategoryTheory.ShortComplex.Homotopy.add_h₁, CochainComplex.HomComplex.Cochain.toSingleMk_add, CategoryTheory.NatTrans.mapHomotopyCategory_app, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CategoryTheory.Functor.mapProjectiveResolution_π, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂, CochainComplex.mappingCone.inr_f_d, CategoryTheory.instIsIsoToRightDerivedZero', CategoryTheory.instPreservesFiniteBiproductsTensorLeft, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g, groupHomology.H1CoresCoinfOfTrivial_X₁, HomologicalComplex₂.ι_D₁_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, groupHomology.chainsMap_id_f_map_mono, CochainComplex.HomComplex.δ_v, groupCohomology.mapShortComplexH2_comp_assoc, CategoryTheory.rightDistributor_ext₂_left_iff, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, CategoryTheory.Abelian.tfae_epi, CategoryTheory.ShortComplex.SnakeInput.comp_f₀, CategoryTheory.cokernelOpOp_hom, CategoryTheory.ShortComplex.HomologyMapData.neg_left, CochainComplex.HomComplex.Cochain.comp_v, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryProduct, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, groupCohomology.mapCocycles₂_comp_i_apply, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CategoryTheory.ShortComplex.Homotopy.smul_h₂, HomotopyCategory.quotient_map_eq_zero_iff, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, CategoryTheory.Abelian.Pseudoelement.zero_eq_zero', CochainComplex.HomComplex.Cochain.neg_v, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, CochainComplex.HomComplex.Cochain.sub_v, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, groupHomology.d₁₀ArrowIso_hom_left, CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down, CategoryTheory.ShortComplex.SnakeInput.instEpiGL₀', CochainComplex.mappingCone.liftCochain_v_descCochain_v, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, Homotopy.nullHomotopicMap'_f_eq_zero, CategoryTheory.Limits.IsBilimit.total, CochainComplex.mappingCone.lift_f_fst_v, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CategoryTheory.ShortComplex.Splitting.s_g_assoc, HomotopyCategory.instFullHomologicalComplexQuotient, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, HomologicalComplex₂.d₂_eq_zero, CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv_assoc, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, CategoryTheory.Biprod.unipotentLower_inv, CochainComplex.XIsoOfEq_shift, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, CategoryTheory.ShortComplex.cyclesMap'_sub, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_apply, CategoryTheory.ShortComplex.homologyMap'_sub, CategoryTheory.ShortComplex.kernelSequence_exact, CategoryTheory.ShortComplex.Splitting.rightHomologyData_ι, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inl, HomologicalComplex.homotopyCofiber_X, HomologicalComplex₂.ι_totalDesc_assoc, CategoryTheory.ShortComplex.Splitting.map_r, CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff, HomotopyCategory.isoOfHomotopyEquiv_hom, CochainComplex.HomComplex.Cochain.rightUnshift_comp, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₃, CategoryTheory.ShortComplex.Homotopy.sub_h₁, CategoryTheory.ShortComplex.Splitting.leftHomologyData_K, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc, groupCohomology.instMonoModuleCatFH1InfRes, CategoryTheory.Limits.IsBilimit.binary_total, HomologicalComplex.instHasTensorXTensorUnit_1, CochainComplex.mappingCone.inr_triangleδ, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, CategoryTheory.kernelCokernelCompSequence.ι_φ, DoldKan.equivalence_counitIso, ModuleCat.smulShortComplex_X₃_isAddCommGroup, CochainComplex.HomComplex.Cochain.ofHoms_comp, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₂, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom, isSeparator_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality', groupCohomology.mapCocycles₂_comp_i_assoc, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, CategoryTheory.ShortComplex.abToCycles_apply_coe, CochainComplex.HomComplex.leftHomologyData_π_hom_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃_assoc, groupHomology.π_comp_H2Iso_inv_assoc, CategoryTheory.HomOrthogonal.matrixDecomposition_id, CochainComplex.mappingCone.id_X, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, ModuleCat.biprodIsoProd_inv_comp_snd_apply, CategoryTheory.ShortComplex.Homotopy.refl_h₃, CochainComplex.HomComplex.Cochain.single_zero, CategoryTheory.ShortComplex.homologyMap'_add, CochainComplex.mappingCone.inr_descShortComplex_assoc, groupHomology.chainsMap_f_3_comp_chainsIso₃, CategoryTheory.ShortComplex.SnakeInput.δ_L₃_f, CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂RightOrthogonal, CategoryTheory.Abelian.Pseudoelement.pseudoZero_iff, CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex, groupHomology.eq_d₂₁_comp_inv, groupHomology.shortComplexH2_f, HomologicalComplex.instEpiGShortComplexTruncLE, CategoryTheory.kernelCokernelCompSequence.inr_π_assoc, isSeparating_iff, CategoryTheory.ShortComplex.HomotopyEquiv.refl_hom, AlgebraicTopology.DoldKan.QInfty_idem_assoc, CategoryTheory.Abelian.FunctorCategory.coimageImageComparison_app, CategoryTheory.ShortComplex.Homotopy.unop_h₃, DerivedCategory.HomologySequence.mono_homologyMap_mor₁_iff, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, Profinite.NobelingProof.succ_exact, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f, groupCohomology.dArrowIso₀₁_hom_right, HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences, AlgebraicTopology.AlternatingFaceMapComplex.map_f, cokernelCoforkOfCofork_ofπ, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, CategoryTheory.ShortComplex.moduleCat_zero_apply, groupCohomology.toCocycles_comp_isoCocycles₂_hom, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₁, CategoryTheory.ShortComplex.Homotopy.neg_h₁, CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp, CategoryTheory.ShortComplex.opcyclesFunctor_linear, HomologicalComplex.homotopyCofiber.inrX_d_assoc, CategoryTheory.kernelCokernelCompSequence.ι_fst_assoc, HomologicalComplex.sub_f_apply, CochainComplex.mappingCone.d_snd_v'_assoc, AlgebraicTopology.DoldKan.QInfty_f, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, HomotopyCategory.eq_of_homotopy, HomologicalComplex.homotopyCofiber.descSigma_ext_iff, CategoryTheory.Abelian.im_map, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryCoproduct, Homotopy.map_nullHomotopicMap', AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, CategoryTheory.ShortComplex.rightHomologyFunctor_linear, groupHomology.mapCycles₁_comp_i, CategoryTheory.ShortComplex.Splitting.leftHomologyData_H, CochainComplex.HomComplex.Cochain.shift_zero, CategoryTheory.instPreservesFiniteBiproductsTensorRight, CategoryTheory.ShortComplex.add_τ₃, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso, groupCohomology.shortComplexH0_f, CategoryTheory.ShiftedHom.zero_comp, CochainComplex.shiftFunctorZero_inv_app_f, groupCohomology.shortComplexH0_g, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc, CategoryTheory.ShortComplex.Homotopy.refl_h₂, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, CategoryTheory.Functor.mapProjectiveResolution_complex, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse, CategoryTheory.InjectivePresentation.shortExact_shortComplex, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom, AlgebraicTopology.alternatingFaceMapComplex_map_f, CochainComplex.HomComplex.Cochain.leftShift_comp, SimplicialObject.Splitting.nondegComplex_d, AlgebraicTopology.DoldKan.P_f_idem_assoc, groupCohomology.shortComplexH1_f, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.Abelian.toIsNormalEpiCategory, CategoryTheory.ShortComplex.Homotopy.rightHomologyMap'_congr, CochainComplex.triangleOfDegreewiseSplit_obj₂, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, Rep.standardComplex.εToSingle₀_comp_eq, AlgebraicTopology.DoldKan.Γ₀'_obj, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂, CategoryTheory.rightDistributor_inv_comp_biproduct_π, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, groupHomology.inhomogeneousChains.d_def, CategoryTheory.leftDistributor_hom_comp_biproduct_π, CategoryTheory.ShortComplex.SnakeInput.L₂'_g, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv, CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesProductsOfShape, HomologicalComplex.homotopyCofiber.inlX_sndX_assoc, CategoryTheory.ShortComplex.Homotopy.compRight_h₀, CategoryTheory.CommSq.shortComplex_f, CochainComplex.homologyFunctor_shift, CategoryTheory.Idempotents.DoldKan.hε, groupCohomology.comp_d₂₃_eq, CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero, HomologicalComplex.quasiIso_iff_evaluation, CategoryTheory.ShortComplex.Splitting.epi_g, CategoryTheory.Abelian.subobjectIsoSubobjectOp_apply, CategoryTheory.ShortComplex.SnakeInput.functorL₀_map, CategoryTheory.Limits.biproduct.matrix_desc_assoc, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, HomologicalComplex₂.ι_D₂, AlgebraicTopology.DoldKan.QInfty_f_0, CategoryTheory.kernelUnopUnop_inv, HomologicalComplex.homologyMap_neg, AddCommGrpCat.instHasFiniteBiproducts, CategoryTheory.ShortComplex.abLeftHomologyData_π, CategoryTheory.ShortComplex.leftHomologyFunctor_additive, CochainComplex.isKInjective_shift_iff, prevD_eq_toPrev_dTo, ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, groupHomology.H1CoresCoinf_X₁, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, Homotopy.nullHomotopicMap'_comp, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, CategoryTheory.rightDistributor_ext_right_iff, CategoryTheory.ShortComplex.rightHomologyFunctor_additive, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_i, CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryCoproducts, CategoryTheory.ShortComplex.moduleCatMk_X₃_isAddCommGroup, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, AlgebraicTopology.AlternatingFaceMapComplex.d_squared, CategoryTheory.ShortComplex.opcyclesMap_add, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.Limits.biprod.decomp_hom_to, CategoryTheory.Biprod.inr_ofComponents, CategoryTheory.Biprod.ofComponents_snd, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, HomologicalComplex₂.total.mapAux.d₁_mapMap, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact, Module.Flat.iff_rTensor_preserves_shortComplex_exact, CochainComplex.mappingCone.lift_f_fst_v_assoc, CategoryTheory.Limits.biproduct.lift_matrix_assoc, CategoryTheory.Limits.biproduct.lift_desc_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.kernelCokernelCompSequence.ι_fst, CategoryTheory.Mat_.lift_obj, epi_iff_cancel_zero, Homotopy.dNext_zero_chainComplex, CategoryTheory.ShortComplex.Homotopy.compRight_h₁, 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, groupHomology.chainsMap_f_single, HomologicalComplex₂.d₁_eq, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_obj, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f, PresheafOfModules.instIsNormalMonoCategory, CochainComplex.HomComplex.Cochain.leftShift_rightShift, CategoryTheory.ShortComplex.Homotopy.smul_h₀, CochainComplex.HomComplex.Cochain.ofHom_neg, Homotopy.prevD_chainComplex, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_mono₃, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, CategoryTheory.ShortComplex.SnakeInput.mono_L₀_f, ModuleCat.cokernel_π_imageSubobject_ext, groupCohomology.cochainsMap_f_map_epi, groupCohomology.comp_d₀₁_eq, CategoryTheory.ShortComplex.Homotopy.smul_h₃, CategoryTheory.ShortComplex.cyclesMap_smul, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂, CochainComplex.HomComplex.Cochain.zero_v, AlgebraicTopology.DoldKan.map_Hσ, CategoryTheory.ShortComplex.SnakeInput.L₁'_f, DerivedCategory.instLinearCochainComplexIntQ, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inr, CategoryTheory.ShortComplex.leftHomologyMap_add, LinearMap.shortExact_shortComplexKer, CategoryTheory.Limits.BinaryBicone.ofLimitCone_inr, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles, AddCommGrpCat.biprodIsoProd_inv_comp_snd_apply, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, CategoryTheory.Biprod.unipotentUpper_hom, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, Module.Flat.iff_lTensor_preserves_shortComplex_exact, CategoryTheory.ShortComplex.Homotopy.ofEq_h₂, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_assoc, CategoryTheory.ShortComplex.exact_iff_of_hasForget, CategoryTheory.ShortComplex.moduleCatMk_X₃_carrier, CategoryTheory.ShortComplex.Splitting.rightHomologyData_p, groupHomology.mapCycles₂_comp_i, CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂, CategoryTheory.MonoidalPreadditive.whiskerLeft_zero, groupCohomology.map_H0Iso_hom_f, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_zero_iff, HomologicalComplex₂.totalAux.ιMapObj_D₂_assoc, CategoryTheory.ShortComplex.Homotopy.comm₃, prevD_nat, CategoryTheory.Mat_.instHasBiproductιObjEmbeddingXOfAdditive, Rep.barResolution_complex, CategoryTheory.InjectiveResolution.extMk_zero, CategoryTheory.ShortComplex.ab_exact_iff_function_exact, AlgebraicTopology.DoldKan.Γ₀_obj_map, CategoryTheory.ShortComplex.homologyMap'_neg, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂_assoc, groupCohomology.cochainsMap_zero, CategoryTheory.ShortComplex.exact_cokernel, CochainComplex.instAdditiveIntFunctorSingleFunctors, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, CochainComplex.shiftFunctor_obj_X, ModuleCat.smulShortComplex_X₁, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, kernelForkOfFork_ofι, groupCohomology.dArrowIso₀₁_inv_left, groupCohomology.π_comp_H1Iso_hom, HomologicalComplex₂.D₁_shape, CategoryTheory.cokernelUnopOp_hom, HomotopyEquiv.quasiIsoAt_inv, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CategoryTheory.ShortComplex.exact_of_g_is_cokernel, CategoryTheory.Functor.IsHomological.toPreservesZeroMorphisms, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, CategoryTheory.kernelCokernelCompSequence.φ_snd_assoc, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_f, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃_assoc, HomologicalComplex.instMonoFShortComplexTruncLE, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_Q, CochainComplex.HomComplex.Cochain.map_add, CategoryTheory.Mat_.embeddingLiftIso_hom_app, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply, groupHomology.eq_d₃₂_comp_inv_apply, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, CochainComplex.HomComplex.Cochain.fromSingleMk_v, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃, CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, CategoryTheory.ObjectProperty.monoModSerre_zero_iff, CochainComplex.HomComplex.Cochain.fromSingleMk_add, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext, CategoryTheory.Limits.inl_of_isLimit, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, CategoryTheory.ShortComplex.SnakeInput.snd_δ, groupCohomology.H1InfRes_X₂, HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc, CochainComplex.HomComplex.Cochain.shift_smul, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, CategoryTheory.Limits.biproduct.reindex_inv, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, CategoryTheory.ShortComplex.Splitting.g_s, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i, CategoryTheory.ShortComplex.Homotopy.ofEq_h₀, CochainComplex.mappingCone.ext_from_iff, CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map, HomotopyCategory.instEssSurjHomologicalComplexQuotient, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF, CategoryTheory.Limits.preservesBiproduct_of_mono_biproductComparison, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, groupHomology.H1CoresCoinf_g, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_of_epi₁, groupCohomology.cochainsMap_id_comp, DerivedCategory.instIsIsoMapCochainComplexIntQ, HomologicalComplex₂.ι_D₂_assoc, ModuleCat.smulShortComplex_g, CategoryTheory.Biprod.ofComponents_eq, HomologicalComplex.isIso_homologyMap_shortComplexTruncLE_g, forkOfKernelFork_pt, HomotopyCategory.quot_mk_eq_quotient_map, CochainComplex.HomComplex.Cocycle.toSingleMk_zero, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply, HomologicalComplex.units_smul_f_apply, CategoryTheory.simple_of_cosimple, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, groupCohomology.mapShortComplexH2_comp, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, groupCohomology.shortComplexH2_f, HomologicalComplex.homotopyCofiber.inrX_fstX, CochainComplex.HomComplex.Cochain.leftUnshift_v, CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc, CategoryTheory.ShortComplex.Homotopy.homologyMap'_congr, simple_iff_isSimpleModule, DerivedCategory.HomologySequence.comp_δ_assoc, CategoryTheory.cokernel.π_unop, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.Limits.biprod.decomp_hom_from, CategoryTheory.ShortComplex.Splitting.splitMono_f_retraction, CategoryTheory.ShortComplex.opcyclesFunctor_additive, groupHomology.H1CoresCoinfOfTrivial_X₂, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, groupHomology.H1CoresCoinf_X₂, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc, CategoryTheory.ObjectProperty.instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁, HomologicalComplex.leftUnitor'_inv_comm_assoc, CategoryTheory.ShortComplex.Homotopy.compRight_h₂, groupCohomology.cochainsMap_comp_assoc, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, groupHomology.π_comp_H2Iso_hom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, CategoryTheory.Biprod.unipotentLower_hom, CategoryTheory.ShortComplex.Splitting.rightHomologyData_Q, CategoryTheory.Abelian.mono_cokernel_map_of_isPullback, HomologicalComplex₂.totalFunctor_obj, CategoryTheory.Abelian.epi_kernel_map_of_isPushout, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_map, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m, CochainComplex.HomComplex.Cochain.rightShift_leftShift, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, groupHomology.mapCycles₁_comp_i_apply, CategoryTheory.Limits.biprod.desc_eq, groupHomology.chainsMap_f_map_epi, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₃, Homotopy.nullHomotopicMap_f, CategoryTheory.Limits.snd_of_isColimit, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_epi₂, ModuleCat.kernelIsoKer_inv_kernel_ι_apply, CategoryTheory.ShortComplex.kernelSequence_X₁, groupHomology.isoShortComplexH1_hom, CategoryTheory.ShortComplex.Homotopy.compRight_h₃, CategoryTheory.Limits.biproduct.lift_desc, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₃, CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CategoryTheory.ShortComplex.SnakeInput.functorL₀_obj, HomologicalComplex.isSeparator_coproduct_separatingFamily, CochainComplex.HomComplex.Cochain.ofHom_v, CategoryTheory.Functor.homologySequence_exact₂, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, CochainComplex.HomComplex.Cochain.ofHom_sub, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.ShortComplex.SnakeInput.L₀_exact, groupCohomology.isoCocycles₂_hom_comp_i, CategoryTheory.ShortComplex.opcyclesMap_neg, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, CategoryTheory.Pretriangulated.contractible_distinguished₂, CochainComplex.HomComplex.Cochain.leftUnshift_smul, CochainComplex.mappingCone.inr_f_snd_v, CategoryTheory.ShortComplex.Homotopy.symm_h₀, CategoryTheory.rightDistributor_inv, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, CategoryTheory.instHasInjectiveDimensionLTBiprod, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CategoryTheory.ShortComplex.Homotopy.equivSubZero_symm_apply, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryProducts, CategoryTheory.Functor.homologySequenceδ_comp_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles_apply, groupHomology.comp_d₁₀_eq, CochainComplex.HomComplex.Cochain.shiftLinearMap_apply, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁_assoc, CategoryTheory.ProjectiveResolution.of_def, CategoryTheory.ShortComplex.instIsNormalMonoCategory, HomologicalComplex₂.totalAux.d₂_eq', CategoryTheory.Functor.homologySequence_mono_shift_map_mor₁_iff, Homotopy.zero, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₂, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂_assoc, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, CategoryTheory.Limits.preservesBinaryBiproduct_of_mono_biprodComparison, HomologicalComplex₂.totalAux.d₁_eq, CategoryTheory.IsPullback.mono_shortComplex'_f, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc, groupCohomology.dArrowIso₀₁_hom_left, CategoryTheory.Idempotents.zero_def, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex.homotopyCofiber.sndX_inrX_assoc, CategoryTheory.Limits.biproduct.matrix_map_assoc, HomologicalComplex₂.shiftFunctor₁XXIso_refl, AlgebraicTopology.inclusionOfMooreComplex_app, Homotopy.extend.hom_eq_zero₁, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂, CategoryTheory.ShortComplex.Homotopy.leftHomologyMap'_congr, CategoryTheory.kernelCokernelCompSequence.ι_snd, prevD_eq, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, CategoryTheory.ShortComplex.SnakeInput.L₁'_g, AlgebraicTopology.DoldKan.P_f_idem, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, AlgebraicTopology.AlternatingCofaceMapComplex.d_squared, CategoryTheory.Limits.biprod.total, CochainComplex.shiftFunctor_map_f', CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_pt, HomologicalComplex₂.ι_totalDesc, groupCohomology.eq_d₀₁_comp_inv_apply, CochainComplex.mappingCone.ext_to_iff, AlgebraicTopology.DoldKan.PInfty_idem_assoc, CategoryTheory.Triangulated.TStructure.zero, HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, groupCohomology.H1InfRes_X₃, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, simple_of_isSimpleModule, CategoryTheory.Abelian.imageIsoImage_inv, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₂, CategoryTheory.ShortComplex.SnakeInput.op_L₀, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π', CochainComplex.HomComplex.Cochain.rightShift_zero, CategoryTheory.ShortComplex.SnakeInput.functorL₂_obj, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_obj, CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi, CategoryTheory.kernelUnopOp_hom, Homotopy.map_nullHomotopicMap, CategoryTheory.ShortComplex.rightHomologyMap'_add, HomologicalComplex₂.d₁_eq_zero, groupHomology.chainsFunctor_obj, HomologicalComplex.zsmul_f_apply, CategoryTheory.ObjectProperty.epiModSerre_zero_iff, groupCohomology.instMonoModuleCatFShortComplexH0, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_symm_apply, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₁, CategoryTheory.ProjectiveResolution.Hom.hom'_f, HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, CochainComplex.singleFunctor_obj_d, HomologicalComplex₂.instHasTotalFlip, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₂, CategoryTheory.kernelCokernelCompSequence.ι_snd_assoc, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, HomologicalComplex.homologyMap_add, CochainComplex.quasiIso_shift_iff, CategoryTheory.ShortComplex.exact_kernel, ModuleCat.biprodIsoProd_inv_comp_snd, CochainComplex.HomComplex.Cochain.rightUnshift_v, HomotopyCategory.composableArrowsFunctor_obj, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, SimplicialObject.Splitting.nondegComplex_X, CategoryTheory.InjectiveResolution.instHasInjectiveResolution, Rep.instPreservesZeroMorphismsModuleCatInvariantsFunctor, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero, CategoryTheory.cokernel.π_op, HomologicalComplex.nsmul_f_apply, HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE, CochainComplex.shiftFunctorAdd'_inv_app_f', HomologicalComplex.homotopyCofiber.inr_desc, CategoryTheory.Limits.biproduct.matrix_map, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₁, groupHomology.d₁₀ArrowIso_inv_right, CategoryTheory.NatTrans.app_zero, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, CategoryTheory.ShortComplex.SnakeInput.functorL₁_map, CategoryTheory.ShortComplex.Homotopy.refl_h₁, CategoryTheory.instIsIsoIndCoimageImageComparison, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, CategoryTheory.kernelCokernelCompSequence.inl_φ, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', prevD_eq_zero, CategoryTheory.kernelCokernelCompSequence.inr_π, CategoryTheory.ShortComplex.exact_iff_epi_toCycles, CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel, CategoryTheory.Mat_.isoBiproductEmbedding_hom, HomotopyCategory.quotient_obj_surjective, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, CategoryTheory.Pretriangulated.Opposite.contractible_distinguished, groupCohomology.mapShortComplexH2_zero, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂, CochainComplex.mappingCone.map_inr, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff, HomologicalComplex.homotopyCofiber.inr_desc_assoc, CategoryTheory.Functor.homologySequenceComposableArrows₅_exact, CochainComplex.shiftFunctorAdd'_eq, CategoryTheory.cokernelOpUnop_inv, epi_iff_isZero_cokernel, HomologicalComplex.mono_homologyMap_shortComplexTruncLE_g, CochainComplex.shiftFunctorAdd'_inv_app_f, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instEpiSheafAddCommGrpCatGShortComplex, CategoryTheory.HomOrthogonal.matrixDecompositionLinearEquiv_apply, Homotopy.extend.homAux_eq, CategoryTheory.ShortComplex.kernelSequence_f, CochainComplex.mappingCone.liftCochain_v_fst_v, groupHomology.chainsMap_id_f_map_epi, CategoryTheory.ShortComplex.SnakeInput.comp_f₂, cokernelCoforkOfCofork_π, CategoryTheory.Functor.comp_homologySequenceδ, DerivedCategory.HomologySequence.mono_homologyMap_mor₂_iff, HomologicalComplex.homotopyCofiber.inlX_desc_f_assoc, CategoryTheory.Biprod.column_nonzero_of_iso, CategoryTheory.ProjectiveResolution.instIsGECochainComplexOfNatInt, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, CategoryTheory.kernel.ι_unop, CategoryTheory.ShortComplex.smul_τ₃, CochainComplex.HomComplex.Cochain.fromSingleMk_zero, CategoryTheory.ShortComplex.Splitting.unop_r, CategoryTheory.ShortComplex.homologyMap_neg, CochainComplex.mappingCone.decomp_from, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, AlgebraicTopology.DoldKan.map_PInfty_f, HomologicalComplex.instAdditiveHomologyFunctor, AlgebraicTopology.DoldKan.P_succ, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, HomologicalComplex.homotopyCofiber.d_fstX, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_pt, groupCohomology.cochainsMap_id_f_map_mono, CategoryTheory.kernelCokernelCompSequence_exact, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, CochainComplex.mappingConeCompTriangle_mor₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, groupHomology.chainsMap_id_comp, CochainComplex.HomComplex.Cochain.leftShift_zero, CategoryTheory.Biprod.ofComponents_comp, CochainComplex.mappingCone.inl_v_snd_v_assoc, CategoryTheory.ShortComplex.Homotopy.symm_h₃, CategoryTheory.ShortComplex.SnakeInput.w₁₃_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, CategoryTheory.Functor.mapHomotopy_hom, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc, groupHomology.instEpiModuleCatGH1CoresCoinf, CategoryTheory.ShortComplex.SnakeInput.functorP_map, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH, CochainComplex.instLinearIntShiftFunctor, groupCohomology.mapShortComplexH1_id, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, Rep.coinvariantsShortComplex_g, CategoryTheory.ShortComplex.HomotopyEquiv.refl_inv, SimplicialObject.Split.nondegComplexFunctor_map_f, CochainComplex.triangleOfDegreewiseSplit_mor₂, AlgebraicTopology.DoldKan.Γ₀'_map_F, TopModuleCat.comp_cokerπ, HomologicalComplex₂.total.mapAux.mapMap_D₁, groupHomology.mapShortComplexH1_id_comp, groupHomology.mapShortComplexH1_comp, CategoryTheory.Limits.preservesBiproduct_of_epi_biproductComparison', HomologicalComplex.homotopyCofiber.eq_desc, CategoryTheory.ShortComplex.Splitting.ofIso_s, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.F_map, CategoryTheory.Mat_.embeddingLiftIso_inv_app, CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_snd, HomologicalComplex.homotopyCofiber.inrX_desc_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₂, DerivedCategory.isLE_Q_obj_iff, groupHomology.isoCycles₂_hom_comp_i_apply, Homotopy.compRight_hom, CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv, CochainComplex.cm5b.fac_assoc, AlgebraicTopology.DoldKan.Hσ_eq_zero, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, HomologicalComplex.tensor_unit_d₂, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply, AlgebraicTopology.normalizedMooreComplex_objD, CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, Rep.coinvariantsShortComplex_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv, CategoryTheory.rightDistributor_ext_left_iff, PresheafOfModules.instIsNormalEpiCategory, CochainComplex.triangleOfDegreewiseSplit_obj₃, groupCohomology.isoCocycles₂_inv_comp_iCocycles_apply, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f_assoc, CochainComplex.shiftFunctorZero'_hom_app_f, CategoryTheory.ObjectProperty.monoModSerre_iff, CategoryTheory.ProjectiveResolution.lift_commutes_zero, CategoryTheory.ShortComplex.HomotopyEquiv.ext_iff, CategoryTheory.Limits.biprod.ext_to_iff, groupCohomology.isoCocycles₁_inv_comp_iCocycles, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_fst, HomotopyCategory.Pretriangulated.contractible_distinguished, CategoryTheory.biproduct_ι_comp_leftDistributor_hom, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, groupHomology.eq_d₂₁_comp_inv_assoc, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom, HomologicalComplex.quasiIsoAt_shortComplexTruncLE_g, kernelForkOfFork_ι, CategoryTheory.ShortComplex.Homotopy.comp_h₁, HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, CategoryTheory.Abelian.coim_obj, CategoryTheory.Pretriangulated.Triangle.zero_hom₁, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.kernelCokernelCompSequence.instEpiπ, ModuleCat.smulShortComplex_X₃_carrier, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₃, CategoryTheory.ShortComplex.SnakeInput.L₀_g_δ, HomologicalComplex₂.d₂_eq_zero', CategoryTheory.Functor.homologySequence_exact₃, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, CochainComplex.mappingCone.triangle_mor₂, CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, CategoryTheory.ShortComplex.Splitting.leftHomologyData_π, CochainComplex.HomComplex.Cocycle.leftUnshift_coe, CategoryTheory.ShortComplex.SnakeInput.snd_δ_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃, groupCohomology.mapShortComplexH2_τ₁, HomologicalComplex₂.total.mapAux.mapMap_D₂, groupHomology.cyclesIso₀_inv_comp_iCycles, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_assoc, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_eq_zero, AlgebraicTopology.DoldKan.Q_idem_assoc, CochainComplex.mappingCone.d_snd_v_assoc, CategoryTheory.HomOrthogonal.matrixDecomposition_comp, CochainComplex.instAdditiveIntShiftFunctor, AlgebraicTopology.DoldKan.PInfty_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, CochainComplex.shiftFunctor_map_f, CategoryTheory.ObjectProperty.epiModSerre_iff, CochainComplex.quasiIsoAt_shift_iff, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₃, CochainComplex.mappingCone.d_snd_v', HomologicalComplex₂.total.mapIso_inv, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_epi₁, HomologicalComplex.shortComplexTruncLE_f, CochainComplex.instIsKProjectiveObjIntShiftFunctor, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.CommSq.shortComplex'_X₁, CategoryTheory.ShortComplex.Homotopy.sub_h₃, CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, CategoryTheory.instHasFiniteBiproductsInd, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.ShortComplex.Homotopy.trans_h₂, CategoryTheory.Idempotents.DoldKan.N_obj, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, CochainComplex.HomComplex.Cochain.rightShift_smul, AlgebraicTopology.DoldKan.Q_f_0_eq, CategoryTheory.Triangulated.TStructure.zero_of_isLE_of_isGE, CochainComplex.HomComplex.Cochain.map_comp, HomologicalComplex.isGrothendieckAbelian, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₁_assoc, CategoryTheory.ShortComplex.SnakeInput.w₀₂, Homotopy.nullHomotopicMap_f_of_not_rel_right, CategoryTheory.Limits.biprod.map_eq, CochainComplex.homotopyOp_hom_eq, CochainComplex.mappingCone.inr_f_descCochain_v_assoc, CochainComplex.HomComplex.Cochain.map_sub, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, AlgebraicTopology.DoldKan.QInfty_f_naturality, CategoryTheory.Abelian.Pseudoelement.zero_morphism_ext', CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_fst, CochainComplex.HomComplex.Cocycle.homOf_f, HomologicalComplex₂.totalAux.ιMapObj_D₂, CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range, CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁, CategoryTheory.ShortComplex.SnakeInput.functorL₃_obj, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId, Homotopy.ofEq_hom, groupCohomology.mapShortComplexH2_id_comp_assoc, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor, HomologicalComplex₂.D₂_shape, CategoryTheory.ShortComplex.abLeftHomologyData_f', CochainComplex.IsKProjective.Qh_map_bijective, groupHomology.π_comp_H1Iso_hom_apply, CochainComplex.mappingCone.d_fst_v_assoc, HomologicalComplex₂.total.mapAux.mapMap_D₂_assoc, mono_iff_isZero_kernel', CochainComplex.homOfDegreewiseSplit_f, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_inl, groupHomology.mapShortComplexH2_comp, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, isCoseparating_iff, CochainComplex.shiftFunctorAdd_inv_app_f, CategoryTheory.MonoidalPreadditive.tensor_zero, DerivedCategory.isGE_Q_obj_iff, CategoryTheory.AbelianOfAdjunction.hasKernels, CategoryTheory.ShortComplex.Splitting.splitEpi_g_section_, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, CochainComplex.mappingCone.map_id, groupHomology.chainsMap_id_f_hom_eq_mapRange, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, CategoryTheory.Adjunction.homAddEquiv_symm_zero, CategoryTheory.ShortComplex.sub_τ₁, groupHomology.toCycles_comp_isoCycles₂_hom, CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc_apply, CochainComplex.mappingConeCompTriangle_obj₃, groupHomology.mapShortComplexH2_τ₂, HomologicalComplex.homotopyCofiber.inlX_sndX, CategoryTheory.ProjectiveResolution.π'_f_zero, CategoryTheory.ShortComplex.Homotopy.add_h₀, Homotopy.ofExtend_hom, CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc, HomologicalComplex.leftUnitor'_inv, HomologicalComplex₂.totalFlipIso_hom_f_D₂, dNext_comp_left, CategoryTheory.ShortComplex.cyclesMap'_smul, AlgebraicTopology.DoldKan.P_f_naturality_assoc, CochainComplex.mappingCone.inl_v_fst_v, CategoryTheory.biproduct_ι_comp_rightDistributor_hom_assoc, CategoryTheory.InjectiveResolution.desc_commutes, AlgebraicTopology.DoldKan.map_P, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_g, CategoryTheory.Abelian.hasBinaryBiproducts, HomologicalComplex.homotopyCofiber.inlX_d, CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_p, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, Homotopy.comp_nullHomotopicMap, AddCommGrpCat.kernelIsoKer_inv_comp_ι, groupHomology.chainsMap_f_map_mono, CategoryTheory.ShortComplex.SnakeInput.L₁'_exact, CategoryTheory.InjectiveResolution.desc_commutes_assoc, groupHomology.shortComplexH0_f, groupHomology.eq_d₁₀_comp_inv, FDRep.instHasKernels, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, CategoryTheory.ShortComplex.SnakeInput.id_f₁, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, groupHomology.isoShortComplexH1_inv, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, CochainComplex.HomComplex.Cochain.shift_units_smul, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₁, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, groupHomology.eq_d₁₀_comp_inv_assoc, CategoryTheory.ShortComplex.SnakeInput.snake_lemma, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d, Homotopy.symm_hom, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, CochainComplex.shiftFunctorAdd_eq, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, CategoryTheory.rightDistributor_assoc, groupHomology.isoCycles₁_hom_comp_i_apply, CochainComplex.mappingCone.inr_f_descCochain_v, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_ι, groupHomology.mapShortComplexH1_τ₁, CochainComplex.cm5b.instQuasiIsoIntP, SheafOfModules.Presentation.map_relations_I, HomologicalComplex₂.D₁_totalShift₁XIso_hom, ModuleCat.hasCokernels_moduleCat, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, CategoryTheory.Limits.preservesBiproduct_of_preservesCoproduct, HomologicalComplex₂.D₂_totalShift₁XIso_hom, AlgebraicTopology.DoldKan.P_idem, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, CategoryTheory.ShortComplex.exact_iff_surjective_moduleCatToCycles, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, ComplexShape.Embedding.instAdditiveHomologicalComplexRestrictionFunctor, CategoryTheory.ShortComplex.RightHomologyData.exact_iff_mono_g', CategoryTheory.ShortComplex.SnakeInput.op_L₃, HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc, CochainComplex.mappingCone.isZero_X_iff, AlgebraicTopology.NormalizedMooreComplex.d_squared, HomologicalComplex.homologyMap_sub, HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc, Homotopy.comp_nullHomotopicMap', groupCohomology.cochainsMap_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f, AlgebraicTopology.DoldKan.Γ₀.map_app, CategoryTheory.Abelian.Ext.zero_hom, Homotopy.dNext_succ_chainComplex, CategoryTheory.IsPushout.epi_shortComplex_g, HomologicalComplex.homotopyCofiber.shape, groupHomology.chainsMap_comp, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, AlgebraicTopology.DoldKan.natTransP_app, CategoryTheory.ShortComplex.pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH, CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements, CategoryTheory.Abelian.Ext.mk₀_zero, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', ModuleCat.kernelIsoKer_hom_ker_subtype, CochainComplex.cm5b.instIsStrictlyGEI, CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId, ModuleCat.smulShortComplex_f, SheafOfModules.Presentation.mapRelations_mapGenerators, HomologicalComplex₂.total.map_comp, SimplicialObject.Split.nondegComplexFunctor_obj, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, AlgebraicTopology.DoldKan.N₁_obj_X, CategoryTheory.ShortComplex.ab_exact_iff, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc_apply, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃_assoc, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero_assoc, AlgebraicTopology.map_alternatingFaceMapComplex, groupCohomology.cocyclesMk₁_eq, CategoryTheory.ShortComplex.SnakeInput.functorL₃_map, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteCoproducts, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.HomComplex.δ_zero_cochain_v, CochainComplex.HomComplex.Cochain.units_smul_v, CochainComplex.HomComplex.Cochain.δ_toSingleMk, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, HomologicalComplex.smul_f_apply, CochainComplex.cm5b.instMonoFIntI, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₁, CategoryTheory.ShortComplex.HomologyMapData.add_right, CategoryTheory.Limits.biproduct.total, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, coforkOfCokernelCofork_π, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_φ₁_assoc, groupCohomology.H1InfRes_X₁, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, CategoryTheory.ShortComplex.rightHomologyMap_sub, AlgebraicTopology.DoldKan.Γ₀_obj_obj, AlgebraicTopology.DoldKan.Q_is_eventually_constant, CochainComplex.HomComplex.Cochain.fromSingleMk_precomp, groupHomology.shortComplexH0_exact, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, CochainComplex.HomComplex.Cochain.leftUnshift_add, CategoryTheory.ShortComplex.SnakeInput.L₁'_X₃, Homotopy.compLeftId_hom, CochainComplex.HomComplex.Cocycle.fromSingleMk_zero, HomologicalComplex.zero_f_apply, CategoryTheory.ShortComplex.cyclesFunctor_additive, CategoryTheory.InjectiveResolution.instHasInjectiveResolutions, hasCokernel_of_hasCoequalizer, CategoryTheory.Limits.biprod.add_eq_lift_desc_id, CategoryTheory.ShortComplex.Splitting.g_s_assoc, CategoryTheory.ShortComplex.SnakeInput.id_f₀, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, CategoryTheory.ProjectiveResolution.extMk_zero, CategoryTheory.leftDistributor_rightDistributor_assoc, HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, CategoryTheory.ShortComplex.Homotopy.equivSubZero_apply, CategoryTheory.ShortComplex.Splitting.f_r_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom, CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_pt, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, HomologicalComplex.homotopyCofiber.inlX_d'_assoc, CategoryTheory.kernelUnopUnop_hom, CochainComplex.mappingCone.inr_f_fst_v_assoc, CategoryTheory.Limits.biproduct.matrix_desc, CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex, Homotopy.add_hom, groupCohomology.mapCocycles₁_comp_i_assoc, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, HomologicalComplex₂.totalFlipIsoX_hom_D₁, CochainComplex.mappingCone.inl_v_d_assoc, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_π, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, TopModuleCat.instCategoryWithHomology, CochainComplex.HomComplex.Cochain.rightShift_units_smul, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₃, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, groupHomology.eq_d₃₂_comp_inv_assoc, CategoryTheory.Functor.preservesZeroMorphisms_of_additive, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, CategoryTheory.ShortComplex.Homotopy.op_h₃, HomologicalComplex₂.instHasTotalFlip_1, CategoryTheory.ShortComplex.abLeftHomologyData_i, CategoryTheory.ObjectProperty.isColocal_trW, CategoryTheory.ProjectiveResolution.instIsStrictlyLECochainComplexOfNatInt, groupCohomology.cocyclesMap_cocyclesIso₀_hom_f, CategoryTheory.ShortComplex.sub_τ₂, CochainComplex.HomComplex.Cochain.rightUnshift_smul, CategoryTheory.ShortComplex.Homotopy.trans_h₃, HomotopyCategory.composableArrowsFunctor_map, CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv, CategoryTheory.ShortComplex.rightHomologyMap'_sub, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, CategoryTheory.ShortComplex.Homotopy.neg_h₃, groupCohomology.π_comp_H2Iso_hom_assoc, CategoryTheory.CommSq.shortComplex'_X₂, CategoryTheory.ShortComplex.Homotopy.unop_h₁, groupCohomology.H1InfRes_g, AlgebraicTopology.DoldKan.Q_succ, CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective, AlgebraicTopology.DoldKan.natTransPInfty_f_app, CategoryTheory.ShortComplex.homologyMap_sub, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, Rep.standardComplex.d_comp_ε, CategoryTheory.ShortComplex.SnakeInput.op_v₂₃, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₃, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₀, FDRep.simple_iff_end_is_rank_one, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_inr, CategoryTheory.ShortComplex.SnakeInput.comp_f₁_assoc, CategoryTheory.ShortComplex.Splitting.shortExact, CategoryTheory.AbelianOfAdjunction.hasCokernels, CategoryTheory.ShortComplex.SnakeInput.op_v₀₁, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, CategoryTheory.ShortComplex.Homotopy.trans_h₀, CategoryTheory.Abelian.im_obj, CategoryTheory.ShortComplex.neg_τ₂, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₂, AlgebraicTopology.NormalizedMooreComplex.map_f, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.kernelCokernelCompSequence.δ_fac, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_snd, DerivedCategory.HomologySequence.exact₁, groupHomology.shortComplexH2_g, Homotopy.compRightId_hom, mono_iff_isZero_kernel, CategoryTheory.Limits.BinaryBicone.ofLimitCone_snd, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, CategoryTheory.Functor.preservesFiniteLimits_iff_forall_exact_map_and_mono, CochainComplex.HomComplex.Cochain.smul_v, CategoryTheory.Limits.HasBiproduct.of_hasCoproduct, CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, HomologicalComplex₂.D₂_D₂_assoc, groupCohomology.mapShortComplexH1_id_comp, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, CategoryTheory.Pretriangulated.Triangle.isZero₂_iff, CategoryTheory.ShortComplex.moduleCat_exact_iff_ker_sub_range, HomologicalComplex.homotopyCofiber.d_sndX, CategoryTheory.ShortComplex.moduleCat_exact_iff, HomologicalComplex.extendMap_add, CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂LeftOrthogonal, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, CategoryTheory.Abelian.DoldKan.equivalence_inverse, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, CategoryTheory.plusPlusSheaf_preservesZeroMorphisms, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply, groupHomology.isoCycles₂_inv_comp_iCycles_apply, SimplicialObject.Splitting.decomposition_id, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, ModuleCat.range_mkQ_cokernelIsoRangeQuotient_inv_apply, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupCohomology.instPreservesZeroMorphismsRepModuleCatFunctor, CochainComplex.HomComplex.Cochain.fromSingleMk_sub, CategoryTheory.ShortComplex.homologyMap'_smul, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, groupHomology.isoShortComplexH2_hom, HomologicalComplex.shortComplexTruncLE_shortExact, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, CochainComplex.IsKProjective.leftOrthogonal, CategoryTheory.Adjunction.homAddEquiv_zero, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, AddCommGrpCat.biprodIsoProd_inv_comp_desc, HomologicalComplex₂.ιTotalOrZero_map, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality_assoc, ModuleCat.kernelIsoKer_hom_ker_subtype_apply, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_epi₂, HomotopyCategory.quotient_obj_as, CategoryTheory.Limits.biproduct.map_matrix_assoc, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, CategoryTheory.Biprod.ofComponents_fst, CategoryTheory.ShortComplex.Splitting.op_s, CategoryTheory.Biprod.unipotentUpper_inv, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.leftDistributor_ext₂_left_iff, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₁, CochainComplex.cm5b.instInjectiveXIntI, CochainComplex.cm5b.instMonoIntI, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, groupHomology.cyclesMk₂_eq, CategoryTheory.ShortComplex.Homotopy.compLeft_h₃, groupHomology.chainsMap_f_1_comp_chainsIso₁, groupCohomology.mapShortComplexH1_comp, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.kernel_ι_d_comp_d, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, AddCommGrpCat.biprodIsoProd_inv_comp_snd, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, HomologicalComplex.shortComplexTruncLE_X₂, AlgebraicTopology.DoldKan.hσ'_eq, HomologicalComplex₂.d₂_eq, groupHomology.π_comp_H1Iso_hom_assoc, CategoryTheory.ShortComplex.cokernelSequence_exact, CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc, groupHomology.chainsMap_f_2_comp_chainsIso₂, CategoryTheory.instHasProjectiveDimensionLTBiprod, CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc, AlgebraicTopology.DoldKan.MorphComponents.id_a, groupHomology.pOpcycles_comp_opcyclesIso_hom, Homotopy.extend.hom_eq_zero₂, Homotopy.nullHomotopicMap'_f_of_not_rel_left, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, groupHomology.π_comp_H2Iso_inv, HomologicalComplex.homotopyCofiber.inlX_d', CategoryTheory.Limits.preservesBiproductsOfShape_of_preservesCoproductsOfShape, AlgebraicTopology.DoldKan.PInfty_f_0, Homotopy.nullHomotopicMap_f_of_not_rel_left, CategoryTheory.ShortComplex.Homotopy.neg_h₀, CategoryTheory.Limits.biproduct.map_matrix, SheafOfModules.Presentation.of_isIso_relations, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_g, groupCohomology.eq_d₂₃_comp_inv, CochainComplex.isKProjective_iff_leftOrthogonal, HomologicalComplex₂.flip_totalFlipIso, HomologicalComplex.quasiIsoAt_iff_evaluation, groupCohomology.cochainsMap_f_map_mono, CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel, HomologicalComplex₂.D₂_D₁, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, CategoryTheory.Functor.map_distinguished_exact, CategoryTheory.ShortComplex.SnakeInput.comp_f₃, groupCohomology.isoShortComplexH1_hom, groupHomology.mapShortComplexH1_id, AlgebraicTopology.DoldKan.PInfty_f_naturality, HomologicalComplex₂.total.map_comp_assoc, CategoryTheory.InjectiveResolution.cochainComplex_d_assoc, AlgebraicTopology.DoldKan.hσ'_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, CategoryTheory.ShortComplex.add_τ₂, CategoryTheory.Pretriangulated.Triangle.zero_hom₃, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, homotopy_congruence, CategoryTheory.cokernelUnopUnop_hom, groupCohomology.isoCocycles₂_inv_comp_iCocycles, CategoryTheory.MonoidalPreadditive.zero_tensor, CategoryTheory.Limits.fst_of_isColimit, CategoryTheory.IsGrothendieckAbelian.instInjectiveZMonomorphismsRlpMonoMapFactorizationDataRlpOfNatHom, CategoryTheory.ShortComplex.rightHomologyMap_add, HomologicalComplex.homotopyCofiber.inlX_fstX_assoc, CochainComplex.shortComplexTruncLE_shortExact, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.cm5b.i_f_comp, CochainComplex.HomComplex.Cochain.δ_rightUnshift, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsFReduced, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_X, CochainComplex.mappingCone.inr_snd, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, CochainComplex.mappingCone.decomp_to, CategoryTheory.ShortComplex.SnakeInput.L₂'_exact, CategoryTheory.CommSq.shortComplex'_g, CategoryTheory.Biprod.isIso_inl_iff_isZero, AddCommGrpCat.biprodIsoProd_inv_comp_desc_apply, CochainComplex.HomComplex.leftHomologyData_H_coe, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, inhomogeneousCochains.d_eq, CochainComplex.HomComplex.leftHomologyData'_K_coe, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι, CategoryTheory.Abelian.Pseudoelement.zero_eq_zero, CochainComplex.mappingCone.inl_fst, CategoryTheory.ShortComplex.HomotopyEquiv.trans_inv, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, groupHomology.H1CoresCoinfOfTrivial_exact, CategoryTheory.ShortComplex.SnakeInput.mono_v₀₁_τ₁, CategoryTheory.ShortComplex.eq_liftCycles_homologyπ_up_to_refinements, Rep.FiniteCyclicGroup.resolution_complex, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, CategoryTheory.Limits.HasBinaryBiproducts.of_hasBinaryCoproducts, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, groupHomology.chainsFunctor_map, CochainComplex.HomComplex.Cocycle.shift_coe, CategoryTheory.Functor.homologySequence_exact₁, CategoryTheory.Abelian.imageIsoImage_hom_comp_image_ι, HomologicalComplex₂.D₁_D₂_assoc, groupCohomology.cocyclesMk₂_eq, Homotopy.trans_hom, DoldKan.equivalence_inverse, CategoryTheory.ShortComplex.exact_iff_image_eq_kernel, AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, instPreservesHomologyFunctorAddCommGrpCatColim, CategoryTheory.ShortComplex.Splitting.leftHomologyData_i, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, groupCohomology.cochainsMap_id_f_map_epi, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc, CochainComplex.isStrictlyLE_shift, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁, groupHomology.chainsMap_f_hom, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles, CategoryTheory.Limits.biproduct.lift_matrix, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₃₁_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_f, AlgebraicTopology.DoldKan.P_is_eventually_constant, AlgebraicTopology.DoldKan.map_Q, CochainComplex.instFullIntSingleFunctor, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CategoryTheory.ShortComplex.HomologyMapData.neg_right, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, CategoryTheory.ShortComplex.SnakeInput.id_f₃, CategoryTheory.epi_from_simple_zero_of_not_iso, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_obj, CochainComplex.HomComplex.Cochain.δ_rightShift, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, DerivedCategory.right_fac_of_isStrictlyLE, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CategoryTheory.Abelian.coimage.comp_π_eq_zero, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, AlgebraicTopology.DoldKan.PInfty_f_idem, CategoryTheory.ShortComplex.Homotopy.add_h₂, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.ShortComplex.Splitting.r_f, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom, CategoryTheory.Triangulated.TStructure.zero', CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, CochainComplex.HomComplex.Cochain.leftShift_v, groupHomology.cyclesMk₁_eq, CochainComplex.mappingCone.d_fst_v'_assoc, groupHomology.H1CoresCoinfOfTrivial_f, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁, CategoryTheory.ShortComplex.exact_of_f_is_kernel, CochainComplex.HomComplex.Cochain.rightUnshift_add, CategoryTheory.ProjectiveResolution.instHasProjectiveResolutions, CategoryTheory.ShortComplex.Splitting.isSplitEpi_g, AlgebraicTopology.DoldKan.σ_comp_PInfty, CochainComplex.HomComplex.Cochain.toSingleMk_zero, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, groupHomology.mapCycles₂_comp_i_assoc, CategoryTheory.Abelian.Pseudoelement.pseudoZero_aux, CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc, CategoryTheory.ShortComplex.Homotopy.eq_add_nullHomotopic, groupCohomology.isoCocycles₁_hom_comp_i, HomotopyCategory.homologyFunctor_shiftMap_assoc, dNext_eq_dFrom_fromNext, AddCommGrpCat.biproductIsoPi_inv_comp_π, CategoryTheory.ShortComplex.SnakeInput.mono_L₂_f, CategoryTheory.rightDistributor_hom_comp_biproduct_π, HomologicalComplex₂.totalShift₂Iso_hom_naturality, CochainComplex.mappingCone.inl_v_d, CategoryTheory.Abelian.has_cokernels, CategoryTheory.ShortComplex.Homotopy.comp_h₀, CategoryTheory.Mat_.lift_map, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, AlgebraicTopology.NormalizedMooreComplex.obj_X, CategoryTheory.Abelian.coimageIsoImage'_hom, CategoryTheory.Limits.biproduct.desc_eq, CategoryTheory.Functor.mapHomotopyCategory_map, CategoryTheory.Limits.HasBinaryBiproduct.of_hasBinaryProduct, CochainComplex.shiftFunctor_obj_X', CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃, CochainComplex.HomComplex.Cochain.shift_v, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.ShortComplex.HomologyMapData.smul_right, CategoryTheory.Limits.biprod.lift_desc_assoc, isLimitForkOfKernelFork_lift, epi_iff_isZero_cokernel', groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, CategoryTheory.leftDistributor_ext_right_iff, groupCohomology.H1InfRes_exact, AlgebraicTopology.NormalizedMooreComplex.objX_add_one, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK, AlgebraicTopology.DoldKan.N₂_obj_X_X, CochainComplex.mappingCone.inr_f_snd_v_assoc, groupCohomology.mapShortComplexH2_τ₂, groupCohomology.mapCocycles₁_comp_i_apply, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, CategoryTheory.ShortComplex.Homotopy.leftHomologyMap_congr, ComplexShape.Embedding.instAdditiveHomologicalComplexExtendFunctor, ChainComplex.linearYonedaObj_d, CategoryTheory.Limits.preservesBiproduct_of_preservesProduct, Rep.standardComplex.instQuasiIsoNatεToSingle₀, CategoryTheory.categoryWithHomology_of_abelian, CategoryTheory.ShortComplex.Homotopy.symm_h₂, HomologicalComplex.epi_homologyMap_shortComplexTruncLE_g, CategoryTheory.cokernelOpUnop_hom, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, Homotopy.smul_hom, Rep.standardComplex.x_projective, Homotopy.prevD_zero_cochainComplex, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, CategoryTheory.ShortComplex.cokernelSequence_X₁, CategoryTheory.Mat_.isoBiproductEmbedding_inv, CochainComplex.triangleOfDegreewiseSplit_mor₃, CategoryTheory.ShortComplex.moduleCatMk_X₁_isModule, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃, CategoryTheory.GrothendieckTopology.plusFunctor_preservesZeroMorphisms, CochainComplex.HomComplex.Cochain.shiftAddHom_apply, CategoryTheory.ShortComplex.ab_zero_apply, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.ShortComplex.quasiIso_iff_evaluation, HomologicalComplex₂.total.mapAux.d₂_mapMap, CategoryTheory.ShortComplex.Homotopy.sub_h₂, CategoryTheory.Abelian.Ext.mk₀_eq_zero_iff, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', CategoryTheory.Idempotents.isIdempotentComplete_iff_idempotents_have_kernels, HomologicalComplex.homotopyCofiber.inrX_d, CategoryTheory.kernel.ι_op, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc, CochainComplex.HomComplex.Cochain.δ_leftUnshift, HomotopyCategory.spectralObjectMappingCone_ω₁, CategoryTheory.kernelCokernelCompSequence.φ_π, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, CochainComplex.mappingCone.d_fst_v', CategoryTheory.InjectiveResolution.desc_commutes_zero, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK, CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker, Rep.FiniteCyclicGroup.resolution_quasiIso, AddCommGrpCat.biprodIsoProd_inv_comp_fst, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, CochainComplex.shiftFunctorAdd'_hom_app_f', CategoryTheory.Functor.mapHomotopyCategory_obj, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_inv, CochainComplex.mappingCone.inl_v_descCochain_v, CochainComplex.HomComplex.Cochain.leftShift_add, CategoryTheory.Mat_.hasFiniteBiproducts, Homotopy.comm, CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, CategoryTheory.ShortComplex.Homotopy.trans_h₁, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, groupCohomology.cochainsMap_f_hom, CochainComplex.shiftEval_hom_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv, CategoryTheory.ShortComplex.moduleCatMkOfKerLERange_X₁, CategoryTheory.ShortComplex.Homotopy.comm₂, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, CategoryTheory.Abelian.image.ι_comp_eq_zero, CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e, groupHomology.H1CoresCoinfOfTrivial_g, CategoryTheory.ShortComplex.Splitting.s_r, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_fst, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBinaryCoproduct, HomologicalComplex.instHasSeparator, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K, CochainComplex.cm5b.i_f_comp_assoc, CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift, CochainComplex.HomComplex_X, CochainComplex.HomComplex.leftHomologyData'_H_coe, CategoryTheory.ShortComplex.sub_τ₃, AlgebraicTopology.alternatingCofaceMapComplex_map, Homotopy.comp_hom, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, CochainComplex.mappingCone.triangleRotateShortComplex_g, dNext_eq, CategoryTheory.Idempotents.DoldKan.equivalence_functor, CochainComplex.shiftFunctor_obj_d', groupCohomology.mapShortComplexH1_id_comp_assoc, CategoryTheory.ShortComplex.cokernelSequence_X₃, groupCohomology.π_comp_H2Iso_hom_apply, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_obj, groupCohomology.mapShortComplexH1_zero, CategoryTheory.CommSq.shortComplex'_f, CategoryTheory.ShortComplex.SnakeInput.L₂'_X₂, CategoryTheory.ShortComplex.homologyFunctor_linear, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_epi₃, IsSMulRegular.smulShortComplex_shortExact, CategoryTheory.ShortComplex.moduleCatMk_f, AlgebraicTopology.DoldKan.N₂_obj_X_d, HomotopyEquiv.quasiIsoAt_hom, groupCohomology.mapShortComplexH1_comp_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.add_φH, CochainComplex.HomComplex.Cocycle.equivHom_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, CategoryTheory.Triangulated.instNonemptyOctahedron, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, CategoryTheory.ShortComplex.rightHomologyMap_neg, CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₂, groupHomology.isoCycles₁_hom_comp_i_assoc, Rep.coinvariantsShortComplex_X₁, CategoryTheory.Limits.biproduct.lift_eq, CategoryTheory.CommSq.shortComplex'_X₃, CategoryTheory.Endofunctor.algebraPreadditive_homGroup_zero_f, CategoryTheory.Abelian.DoldKan.equivalence_functor, CochainComplex.mappingCone.inr_descShortComplex, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ, DerivedCategory.instAdditiveCochainComplexIntQ, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, groupCohomology.isoShortComplexH2_hom, CochainComplex.cm5b.I_d, CategoryTheory.ProjectiveResolution.exact₀, CategoryTheory.ShortComplex.Homotopy.ofEq_h₁, CochainComplex.triangleOfDegreewiseSplit_mor₁, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, CategoryTheory.Limits.BinaryBicone.ofLimitCone_fst, CategoryTheory.ShortComplex.Homotopy.op_h₁, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, groupCohomology.π_comp_H1Iso_hom_apply, HomologicalComplex.homotopyCofiber.inlX_d_assoc, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, HomologicalComplex.homotopyCofiber_d, CochainComplex.HomComplex.Cochain.d_comp_ofHom_v, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.CommSq.shortComplex_X₃, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_iff_mono₂, CochainComplex.HomComplex.Cochain.leftShift_units_smul, AlgebraicGeometry.tilde.map_zero, HomologicalComplex.homotopyCofiber.desc_f, CategoryTheory.ShortComplex.Splitting.isSplitMono_f, HomotopyCategory.homologyShiftIso_hom_app, CategoryTheory.IsPushout.exact_shortComplex, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, CochainComplex.shiftFunctorAdd_hom_app_f, groupCohomology.mapShortComplexH2_id_comp, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.instMonoSheafAddCommGrpCatFShortComplex, CategoryTheory.ShortComplex.moduleCatMk_X₃_isModule, CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₃, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, CategoryTheory.ShortComplex.SnakeInput.op_L₁, CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP_comp_pullback_snd_assoc, CategoryTheory.ShortComplex.rightHomologyMap'_neg, ModuleCat.biprodIsoProd_inv_comp_fst, CategoryTheory.Limits.BinaryBicone.ofColimitCocone_snd, CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt_1, CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down, CategoryTheory.MonoidalPreadditive.zero_whiskerRight, CategoryTheory.Abelian.FunctorCategory.imageObjIso_hom, CategoryTheory.Idempotents.DoldKan.Γ_map_app, CategoryTheory.Functor.IsHomological.exact, groupHomology.instEpiModuleCatGShortComplexH0, CochainComplex.HomComplex.δ_map, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_apply, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, groupHomology.π_comp_H2Iso_hom_apply, CategoryTheory.Limits.biprod.add_eq_lift_id_desc, CochainComplex.mappingCone.inl_v_descShortComplex_f, CategoryTheory.ShortComplex.QuasiIso.exact_iff, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁, AddCommGrpCat.kernelIsoKer_hom_comp_subtype, HomologicalComplex.homotopyCofiber.sndX_inrX, HomologicalComplex₂.ι_D₁, CategoryTheory.Limits.preservesBinaryBiproduct_of_epi_biprodComparison', CategoryTheory.ShortComplex.Splitting.r_f_assoc, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v, CochainComplex.HomComplex.Cochain.toSingleMk_postcomp, CategoryTheory.kernelOpOp_inv, CategoryTheory.leftDistributor_inv, CochainComplex.HomComplex.Cochain.ofHom_add, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, CategoryTheory.Localization.Preadditive.add'_zero, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, CochainComplex.mappingCone.inr_f_descShortComplex_f, ModuleCat.biproductIsoPi_inv_comp_π_apply, CochainComplex.HomComplex.Cochain.id_comp, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, CategoryTheory.Abelian.toIsNormalMonoCategory, SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero, groupHomology.isoCycles₁_inv_comp_iCycles, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', groupHomology.chainsMap_zero, CochainComplex.HomComplex.Cochain.single_v_eq_zero', CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f, DerivedCategory.exists_iso_Q_obj_of_isLE, groupHomology.H1CoresCoinfOfTrivial_g_epi, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_epi₃, CochainComplex.shiftFunctorAdd'_hom_app_f, forkOfKernelFork_ι, CategoryTheory.Mat_.id_apply, CochainComplex.HomComplex.Cochain.ofHom_zero, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, HomologicalComplex.HomologySequence.composableArrows₃_exact, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, CategoryTheory.ShortComplex.Homotopy.compLeft_h₀, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CochainComplex.HomComplex.leftHomologyData'_π, groupHomology.mapShortComplexH2_id_comp, Homotopy.compLeft_hom, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, groupHomology.isoShortComplexH2_inv, groupHomology.toCycles_comp_isoCycles₁_hom, CategoryTheory.Limits.HasFiniteBiproducts.of_hasFiniteProducts, CategoryTheory.Abelian.tfae_mono, prevD_comp_right, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, HomologicalComplex.shortComplexTruncLE_X₁, CategoryTheory.ShortComplex.Homotopy.g_h₃, CategoryTheory.ShortComplex.exact_iff_mono_fromOpcycles, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁, isCoseparator_iff, CategoryTheory.leftDistributor_inv_comp_biproduct_π_assoc, HomologicalComplex₂.total_d, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_π_f, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, CategoryTheory.Abelian.Ext.addEquivBiprod_symm_apply, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, CochainComplex.HomComplex.Cochain.map_ofHom, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, groupHomology.mapCycles₂_comp_i_apply, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, CategoryTheory.Pretriangulated.Triangle.isZero₃_iff, CategoryTheory.ShortComplex.Homotopy.comp_h₂, CategoryTheory.ShortComplex.Homotopy.ofEq_h₃, groupCohomology.cocyclesIso₀_hom_comp_f_apply, CategoryTheory.ShortComplex.cyclesMap'_add, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, CochainComplex.shiftFunctorComm_hom_app_f, groupCohomology.iCocycles_mk, AlgebraicTopology.DoldKan.QInfty_f_idem, groupHomology.isoCycles₂_hom_comp_i, ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₁, CategoryTheory.ShortComplex.Homotopy.rightHomologyMap_congr, groupHomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, CochainComplex.mappingCone.inl_v_snd_v, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso, CategoryTheory.ShortComplex.neg_τ₁, groupHomology.isoCycles₂_inv_comp_iCycles, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_apply, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, CategoryTheory.ShortComplex.SnakeInput.L₂'_f, HomologicalComplex.unit_tensor_d₁, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal, CategoryTheory.kernelCokernelCompSequence.inl_φ_assoc, CategoryTheory.ShortComplex.Homotopy.homologyMap_congr, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK, CategoryTheory.Idempotents.Karoubi.instHasBinaryBiproductComplement, CategoryTheory.ShortComplex.Splitting.ofIso_r, CategoryTheory.ShortComplex.SnakeInput.Hom.comm₀₁_assoc, CochainComplex.HomComplex.Cochain.rightShift_neg, HomologicalComplex.HomologySequence.composableArrows₃Functor_map, HomologicalComplex₂.totalShift₁Iso_hom_naturality, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison, CategoryTheory.rightDistributor_hom, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, HomotopyCategory.quotient_obj_singleFunctors_obj, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.ShortComplex.Homotopy.neg_h₂, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, CategoryTheory.ProjectiveResolution.instHasProjectiveResolution, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, HomologicalComplex₂.d₂_eq', ModuleCat.hasKernels_moduleCat, CategoryTheory.ShortComplex.smul_τ₁, groupHomology.shortComplexH0_g, DerivedCategory.instEssSurjCochainComplexIntQ, CategoryTheory.ShiftedHom.map_zero, CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero, CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff, CategoryTheory.ShortComplex.Splitting.f_r, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_mono₁, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, ComplexShape.quotient_isLocalization, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, groupCohomology.mapShortComplexH2_id, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, groupHomology.d₁₀ArrowIso_hom_right, Homotopy.dNext_cochainComplex, groupCohomology.shortComplexH0_exact, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, Homotopy.nullHomotopicMap'_f, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, HomologicalComplex₂.totalFlipIsoX_hom_D₂, CategoryTheory.ShortComplex.exact_iff_of_forks, CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyInvHomId, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.f'_eq, CategoryTheory.ShortComplex.smul_τ₂, CochainComplex.shiftEval_inv_app, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, groupHomology.π_comp_H1Iso_inv_apply, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, groupCohomology.isoCocycles₂_hom_comp_i_apply, groupHomology.H1CoresCoinfOfTrivial_X₃, Homotopy.nullHomotopicMap'_f_of_not_rel_right, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_apply, dNext_comp_right, HomologicalComplex.homotopyCofiber.inlX_desc_f, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₃, HomotopyCategory.instAdditiveHomologicalComplexQuotient, CategoryTheory.biproduct_ι_comp_leftDistributor_inv, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc_apply, HomotopyCategory.quotient_map_out, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁, CategoryTheory.ObjectProperty.IsSerreClass.toIsClosedUnderExtensions, SheafOfModules.Presentation.IsFinite.finite_relations, CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₃, CategoryTheory.ShortComplex.Homotopy.add_h₃, HomologicalComplex₂.d₁_eq', HomologicalComplex.instHasTensorXTensorUnit, groupHomology.inhomogeneousChains.d_eq, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker, one_def, groupHomology.eq_d₂₁_comp_inv_apply, CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃, CategoryTheory.Mat_.id_def, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum, CategoryTheory.ShortComplex.Splitting.homologyData_left, CategoryTheory.ShortComplex.cyclesMap'_neg, CategoryTheory.ShortComplex.moduleCatMk_X₂_carrier, groupCohomology.cochainsFunctor_map, CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom, AlgebraicTopology.DoldKan.decomposition_Q, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, CategoryTheory.ShortComplex.opcyclesMap'_add, HomologicalComplex.quasiIsoAt_map_of_preservesHomology, CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, HomologicalComplex.instAdditiveSingle, CategoryTheory.leftDistributor_hom_comp_biproduct_π_assoc, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_apply, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, HomotopyCategory.homologyFunctor_shiftMap, groupCohomology.shortComplexH2_g, CategoryTheory.ShortComplex.rightHomologyMap'_smul, CategoryTheory.ShortComplex.Homotopy.unop_h₀, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, HomologicalComplex.HomologySequence.composableArrows₃Functor_obj, Rep.coinvariantsShortComplex_X₂, CategoryTheory.Pretriangulated.contractible_distinguished, CategoryTheory.ShortComplex.SnakeInput.L₂_exact, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, CategoryTheory.Pretriangulated.Triangle.isZero₁_iff, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₂, CategoryTheory.cokernelUnopOp_inv, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, CochainComplex.mappingCone.lift_f_snd_v, CategoryTheory.ShortComplex.kernelSequence_g, HomologicalComplex₂.ιTotalOrZero_eq_zero, CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₁, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, CochainComplex.isKProjective_shift_iff, CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₁, CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down, HomologicalComplex.opFunctor_additive, ModuleCat.smulShortComplex_X₃_isModule, HomologicalComplex.instQuasiIsoShortComplexTruncLEX₃ToTruncGE, CategoryTheory.ShortComplex.neg_τ₃, HomologicalComplex.eval_additive, CochainComplex.instIsStrictlyLEObjIntSingleFunctor, CochainComplex.mappingCone.triangle_obj₂, CochainComplex.instIsStrictlyGEObjIntSingleFunctor, CategoryTheory.Mat_.id_apply_of_ne, CategoryTheory.kernelOpOp_hom, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, CochainComplex.mappingConeCompTriangle_mor₂, AlgebraicTopology.DoldKan.Q_f_idem_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, AlgebraicTopology.DoldKan.Γ₂N₁_inv, HomologicalComplex₂.D₁_totalShift₂XIso_hom, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, groupHomology.mapShortComplexH1_τ₃, CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₂, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_snd, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_zero, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, CategoryTheory.ShortComplex.SnakeInput.epi_L₁_g, groupCohomology.cocyclesMk₀_eq, CochainComplex.mappingConeCompTriangleh_comm₁, AlgebraicTopology.DoldKan.Q_f_naturality, AlgebraicTopology.DoldKan.Q_zero, CochainComplex.HomComplex.Cocycle.leftShift_coe, groupHomology.lsingle_comp_chainsMap_f_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom, CategoryTheory.ShortComplex.kernelSequence_X₃, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₁, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, CategoryTheory.ShortComplex.rightHomologyMap_smul, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_hom_τ₂, groupCohomology.isoShortComplexH1_inv, CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_iff_mono₁, AlgebraicTopology.DoldKan.identity_N₂_objectwise, CategoryTheory.Abelian.Pseudoelement.eq_zero_iff, HomologicalComplex.shortExact_iff_degreewise_shortExact, HomologicalComplex.shortComplexTruncLE_shortExact_δ_eq_zero, CochainComplex.HomComplex.Cochain.shift_v', CategoryTheory.ShortComplex.Splitting.rightHomologyData_H, CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀.hf, CategoryTheory.Biprod.inl_ofComponents, CategoryTheory.Limits.biproduct.map_eq, HomologicalComplex₂.flip_hasTotal_iff, CategoryTheory.leftDistributor_ext₂_right_iff, AlgebraicTopology.inclusionOfMooreComplexMap_f, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, CategoryTheory.ShortComplex.SnakeInput.comp_f₁, CategoryTheory.Idempotents.DoldKan.hη, CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, DerivedCategory.HomologySequence.δ_comp_assoc, CategoryTheory.CommSq.shortComplex_X₁, CategoryTheory.kernelCokernelCompSequence.inl_π, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc, DerivedCategory.HomologySequence.δ_comp, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, groupHomology.H1CoresCoinf_f, CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁, Homotopy.extend.hom_eq, DerivedCategory.mem_distTriang_iff, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc, TopModuleCat.kerι_comp, HomologicalComplex.homotopyCofiber.d_sndX_assoc, CategoryTheory.ShortComplex.cokernelSequence_X₂, CategoryTheory.ShortComplex.Splitting.unop_s, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, dNext_nat, CochainComplex.isKInjective_iff_rightOrthogonal, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, CategoryTheory.Pretriangulated.preadditiveYoneda_map_distinguished, CategoryTheory.Abelian.instIsIsoCoimageImageComparison, CochainComplex.HomComplex.Cochain.rightShift_add, CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc, CochainComplex.ShiftSequence.shiftIso_inv_app, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, HomologicalComplex.neg_f_apply, groupCohomology.cochainsMap_id_comp_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, CochainComplex.HomComplex.Cochain.diff_v, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_map, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, CategoryTheory.Abelian.Ext.biprodAddEquiv_symm_apply, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, groupCohomology.map_H0Iso_hom_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, CategoryTheory.ShortComplex.Exact.moduleCat_of_range_eq_ker, Homotopy.refl_hom, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, CategoryTheory.Functor.exact_tfae, CochainComplex.isGE_shift, ModuleCat.kernelIsoKer_inv_kernel_ι, DerivedCategory.HomologySequence.exact₃, AlgebraicTopology.DoldKan.map_hσ', AlgebraicTopology.DoldKan.N₂_map_f_f, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, simple_iff_isSimpleModule', CochainComplex.HomComplex.Cochain.ofHoms_zero, groupHomology.shortComplexH1_g, DerivedCategory.Q_map_eq_of_homotopy, Rep.instPreservesZeroMorphismsModuleCatCoinvariantsFunctor, HomologicalComplex₂.totalAux.ιMapObj_D₁_assoc, groupCohomology.eq_d₁₂_comp_inv_assoc, CategoryTheory.exact_f_d, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_pt_p, CochainComplex.mappingCone.triangleRotateShortComplex_f, CategoryTheory.exact_d_f, groupCohomology.H1InfRes_f, CategoryTheory.Pretriangulated.contractible_distinguished₁, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CochainComplex.HomComplex.Cocycle.rightUnshift_coe, CategoryTheory.kernelCokernelCompSequence.φ_snd, DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff, AlgebraicTopology.DoldKan.P_f_naturality, CategoryTheory.Functor.mapHomotopyEquiv_hom, ModuleCat.smulShortComplex_X₂, CategoryTheory.Localization.Preadditive.zero_add', dNext_eq_zero, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, instFreeCarrierX₂ModuleCatProjectiveShortComplex, CategoryTheory.Abelian.FunctorCategory.coimageObjIso_hom, CategoryTheory.Localization.Preadditive.neg'_add'_self, CategoryTheory.Abelian.subobjectIsoSubobjectOp_symm_apply, CategoryTheory.Abelian.hasFiniteBiproducts, CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBinaryProducts, CochainComplex.mappingCone.lift_f, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, HomologicalComplex.homotopyCofiber.inrX_sndX, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, CochainComplex.HomComplex.Cochain.δ_leftShift, HomologicalComplex₂.totalAux.d₁_eq', CategoryTheory.ShortComplex.add_τ₁, DerivedCategory.isIso_Q_map_iff_quasiIso, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Functor.map_distinguished_op_exact, CategoryTheory.Limits.biproduct.reindex_hom, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, CategoryTheory.leftDistributor_assoc, groupCohomology.mapShortComplexH2_τ₃, CochainComplex.HomComplex.CohomologyClass.toHom_mk, AlgebraicTopology.DoldKan.N₁Γ₀_app, HomologicalComplex₂.total.hom_ext_iff, CategoryTheory.ShortComplex.instMonoFKernelSequence, CochainComplex.HomComplex.Cochain.add_v, CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom, groupCohomology.isoShortComplexH2_inv, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, HomotopyCategory.quotient_map_mem_quasiIso_iff, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel', DerivedCategory.left_fac_of_isStrictlyGE, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, groupCohomology.isoCocycles₂_hom_comp_i_assoc, CochainComplex.mappingCone.inl_v_fst_v_assoc, groupHomology.eq_d₁₀_comp_inv_apply, CategoryTheory.ShortComplex.HomologyMapData.smul_left, HomologicalComplex.unopFunctor_additive, Rep.coinvariantsShortComplex_X₃, CategoryTheory.Idempotents.DoldKan.N_map, CategoryTheory.Pretriangulated.instHasFiniteBiproducts, CategoryTheory.Functor.homologySequenceδ_comp, HomologicalComplex.instIsNormalMonoCategory, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, HomologicalComplex.rightUnitor'_inv_comm, CategoryTheory.Abelian.Ext.addEquivBiprod_apply_fst, CategoryTheory.ShortComplex.Homotopy.symm_h₁, CategoryTheory.Limits.BinaryBicone.ofLimitCone_pt, groupHomology.mapShortComplexH2_τ₃, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, CategoryTheory.ShortComplex.SnakeInput.w₁₃, CategoryTheory.ShortComplex.leftHomologyFunctor_linear, CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyInvHomId, CochainComplex.HomComplex.Cochain.leftShift_neg, CategoryTheory.Abelian.epiWithInjectiveKernel_iff, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, groupCohomology.eq_d₀₁_comp_inv_assoc, ModuleCat.toKernelSubobject_arrow, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, HomologicalComplex₂.D₁_D₂, ModuleCat.instHasBinaryBiproducts, HomotopyCategory.isoOfHomotopyEquiv_inv, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CategoryTheory.ShortComplex.Homotopy.compLeft_h₁, CochainComplex.HomComplex.Cochain.toSingleMk_sub, CategoryTheory.ShortComplex.leftHomologyMap'_add, CategoryTheory.kernelCokernelCompSequence.inr_φ_fst, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, HomologicalComplex.shortComplexTruncLE_X₃_isSupportedOutside, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, ModuleCat.smulShortComplex_g_epi, CategoryTheory.ShortComplex.Homotopy.h₀_f, CategoryTheory.ShortComplex.opcyclesMap'_neg, groupCohomology.isoCocycles₁_hom_comp_i_assoc, Rep.coinvariantsShortComplex_shortExact, CategoryTheory.InjectiveResolution.descFOne_zero_comm, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, groupHomology.π_comp_H1Iso_inv_assoc, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, CategoryTheory.Abelian.FunctorCategory.imageObjIso_inv, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, Rep.FiniteCyclicGroup.resolution_π, CategoryTheory.ShortComplex.SnakeInput.functorL₂_map, CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'_assoc, CochainComplex.HomComplex.Cochain.leftUnshift_neg, CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc, mono_iff_cancel_zero, CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂, CochainComplex.isLE_shift, CochainComplex.mappingCone.triangle_obj₁, HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc, groupHomology.mapCycles₁_comp_i_assoc, Homotopy.nullHomotopy'_hom, CategoryTheory.ShortComplex.SnakeInput.instMonoFL₀'OfL₁, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, CategoryTheory.Abelian.Pseudoelement.zero_apply, CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₁, CategoryTheory.Limits.biprod.lift_desc, CategoryTheory.ShortComplex.instEpiGCokernelSequence, CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι_assoc, CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₃, AlgebraicTopology.DoldKan.Γ₀'_map_f, CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff, groupCohomology.mapShortComplexH1_τ₁, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_apply, CochainComplex.mappingCone.lift_f_snd_v_assoc, CategoryTheory.cokernel_zero_of_nonzero_to_simple, ModuleCat.smulShortComplex_exact, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, groupHomology.π_comp_H2Iso_inv_apply, CochainComplex.cm5b, CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₁, CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_snd, Rep.FiniteCyclicGroup.resolution.π_f, CategoryTheory.leftDistributor_inv_comp_biproduct_π, CategoryTheory.ShortComplex.leftHomologyMap_smul, HomologicalComplex.exact_iff_degreewise_exact, CategoryTheory.Functor.comp_homologySequenceδ_assoc, HomologicalComplex.homotopyCofiber.d_fstX_assoc, CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₀, groupCohomology.cochainsFunctor_obj, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₂, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CategoryTheory.kernelCokernelCompSequence.instMonoι, CategoryTheory.Abelian.coimIsoIm_hom_app, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom', CategoryTheory.ShortComplex.opcyclesMap'_smul, CategoryTheory.ShortComplex.ShortExact.ab_exact_iff_function_exact, CategoryTheory.cokernelOpOp_inv, CategoryTheory.ShortComplex.kernelSequence_X₂, CategoryTheory.Pretriangulated.binaryBiproductTriangle_distinguished, CategoryTheory.Limits.binaryBiconeOfIsSplitEpiOfKernel_inr, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.ShortComplex.instPreservesHomologyModuleCatAbForget₂LinearMapIdCarrierAddMonoidHomCarrier, HomologicalComplex.Hom.fAddMonoidHom_apply, CategoryTheory.InjectiveResolution.instInjectiveXIntCochainComplex, CochainComplex.shiftFunctor_obj_d, HomologicalComplex₂.total.map_id, CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π_assoc, CategoryTheory.Comonad.coalgebraPreadditive_homGroup_zero_f, groupCohomology.mapCocycles₁_comp_i, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, CochainComplex.HomComplex.Cochain.toSingleMk_precomp, HomotopyCategory.instLinearHomologicalComplexQuotient, CategoryTheory.ShortComplex.leftHomologyMap'_smul, CochainComplex.HomComplex.Cocycle.rightShift_coe, CategoryTheory.CommSq.shortComplex_X₂, CategoryTheory.ShortComplex.cyclesMap_add, CochainComplex.mappingCone.d_fst_v, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, CategoryTheory.ObjectProperty.isLocal_trW, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, HomologicalComplex₂.total.forget_map, HomologicalComplex.homotopyCofiber.inr_f, HomologicalComplex.homotopyCofiber.inrX_desc_f_assoc, CategoryTheory.Abelian.has_kernels, AlgebraicTopology.DoldKan.Γ₂N₂_inv, HomologicalComplex₂.totalFunctor_map, CochainComplex.HomComplex.Cochain.leftUnshift_zero, FDRep.simple_iff_char_is_norm_one, CategoryTheory.kernelCokernelCompSequence.ι_φ_assoc, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, DerivedCategory.left_fac, groupCohomology.π_comp_H2Iso_hom, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, groupHomology.chainsMap_f_0_comp_chainsIso₀, AlgebraicTopology.normalizedMooreComplex_obj, CategoryTheory.ShortComplex.moduleCatMk_X₂_isAddCommGroup, CochainComplex.mappingCone.triangle_obj₃, AlgebraicTopology.DoldKan.natTransQ_app, coforkOfCokernelCofork_pt, CochainComplex.HomComplex.Cochain.map_neg, CategoryTheory.Pretriangulated.Triangle.zero_hom₂, HomologicalComplex₂.ιTotal_map_assoc, AddCommGrpCat.instHasBinaryBiproducts, CochainComplex.HomComplex_d_hom_apply, CochainComplex.instFaithfulIntSingleFunctor, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel_fst, CategoryTheory.ShortComplex.homologyFunctor_additive, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, CochainComplex.mappingConeCompTriangle_obj₁, CochainComplex.cm5b.I_X, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CategoryTheory.Functor.homologySequence_epi_shift_map_mor₂_iff, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, CategoryTheory.leftDistributor_ext_left_iff, HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc, ModuleCat.instHasFiniteBiproducts, CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, CategoryTheory.Abelian.coimIsoIm_inv_app, CategoryTheory.ShortComplex.Splitting.s_r_assoc, CategoryTheory.instIsIsoFromLeftDerivedZero', CategoryTheory.ShortComplex.leftHomologyMap_neg, CategoryTheory.Limits.biprod.ext_from_iff, CategoryTheory.kernelCokernelCompSequence.φ_π_assoc, CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, CategoryTheory.ShortComplex.Splitting.homologyData_iso, ModuleCat.biprodIsoProd_inv_comp_fst_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_exact, FGModuleCat.instIsIsoCoimageImageComparison, CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_f, groupCohomology.shortComplexH1_g, groupHomology.chainsMap_f, AlgebraicTopology.DoldKan.PInfty_add_QInfty, CochainComplex.ShiftSequence.shiftIso_hom_app, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, AlgebraicTopology.DoldKan.Q_f_idem, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, groupCohomology.cochainsMap_id, CochainComplex.HomComplex.Cochain.single_v_eq_zero, CategoryTheory.InjectiveResolution.cochainComplex_d, CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_inv, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, CochainComplex.mappingCone.map_δ, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv, CochainComplex.HomComplex.Cochain.ofHom_comp, ChainComplex.linearYonedaObj_X, HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology
rightComp 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid homGroup	—	—
add_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' add_comp
coforkOfCokernelCofork_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair coforkOfCokernelCofork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	—
coforkOfCokernelCofork_π 📖	mathematical	—	CategoryTheory.Limits.Cofork.π coforkOfCokernelCofork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	—
cokernelCoforkOfCofork_ofπ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	cokernelCoforkOfCofork CategoryTheory.Limits.Cofork.ofπ CategoryTheory.Limits.CokernelCofork.ofπ preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	—
cokernelCoforkOfCofork_π 📖	mathematical	—	CategoryTheory.Limits.Cofork.π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms cokernelCoforkOfCofork	—	—
comp_add 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid homGroup	—	—
comp_add_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_add
comp_neg 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	map_neg AddMonoidHom.instAddMonoidHomClass
comp_neg_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_neg
comp_nsmul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	map_nsmul AddMonoidHom.instAddMonoidHomClass
comp_sub 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	map_sub AddMonoidHom.instAddMonoidHomClass
comp_sub_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_sub
comp_sum 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommGroup.toAddCommMonoid homGroup	—	map_sum AddMonoidHom.instAddMonoidHomClass
comp_sum_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommGroup.toAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_sum
comp_zsmul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	map_zsmul AddMonoidHom.instAddMonoidHomClass
epi_iff_cancel_zero 📖	mathematical	—	CategoryTheory.Epi Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.zero_of_epi_comp epi_of_cancel_zero
epi_iff_isZero_cokernel 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.IsZero CategoryTheory.Limits.cokernel preadditiveHasZeroMorphisms	—	epi_iff_isZero_cokernel'
epi_iff_isZero_cokernel' 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.IsZero CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi epi_of_isZero_cokernel'
epi_of_cancel_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	CategoryTheory.Epi	—	sub_eq_zero map_sub AddMonoidHom.instAddMonoidHomClass
epi_of_cokernel_iso_zero 📖	mathematical	—	CategoryTheory.Epi	—	epi_of_cokernel_zero CategoryTheory.Limits.zero_of_target_iso_zero
epi_of_cokernel_zero 📖	mathematical	CategoryTheory.Limits.cokernel.π preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Epi	—	epi_of_cancel_zero CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.zero_comp
epi_of_isZero_cokernel 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Limits.cokernel preadditiveHasZeroMorphisms	CategoryTheory.Epi	—	epi_of_isZero_cokernel' CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp
epi_of_isZero_cokernel' 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	CategoryTheory.Epi	—	epi_of_cancel_zero CategoryTheory.Limits.IsZero.eq_of_src CategoryTheory.Limits.comp_zero
forkOfKernelFork_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair forkOfKernelFork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	—
forkOfKernelFork_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι forkOfKernelFork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	—
hasCoequalizer_of_hasCokernel 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizer	—	CategoryTheory.Limits.coequalizer.condition
hasCoequalizers_of_hasCokernels 📖	mathematical	—	CategoryTheory.Limits.HasCoequalizers	—	CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair hasCoequalizer_of_hasCokernel CategoryTheory.Limits.HasCokernels.has_colimit
hasCokernel_of_hasCoequalizer 📖	mathematical	—	CategoryTheory.Limits.HasCokernel preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	—
hasEqualizer_of_hasKernel 📖	mathematical	—	CategoryTheory.Limits.HasEqualizer	—	CategoryTheory.Limits.equalizer.condition
hasEqualizers_of_hasKernels 📖	mathematical	—	CategoryTheory.Limits.HasEqualizers	—	CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair hasEqualizer_of_hasKernel CategoryTheory.Limits.HasKernels.has_limit
hasKernel_of_hasEqualizer 📖	mathematical	—	CategoryTheory.Limits.HasKernel preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	—
instEpiNegHom 📖	mathematical	—	CategoryTheory.Epi Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	CategoryTheory.cancel_epi comp_neg neg_comp
instMonoNegHom 📖	mathematical	—	CategoryTheory.Mono Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	CategoryTheory.cancel_mono neg_comp comp_neg
isColimitCoforkOfCokernelCofork_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair coforkOfCokernelCofork isColimitCoforkOfCokernelCofork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms cokernelCoforkOfCofork	—	—
isLimitForkOfKernelFork_lift 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair forkOfKernelFork isLimitForkOfKernelFork Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms kernelForkOfFork	—	—
kernelForkOfFork_ofι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	kernelForkOfFork CategoryTheory.Limits.Fork.ofι CategoryTheory.Limits.KernelFork.ofι preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	—
kernelForkOfFork_ι 📖	mathematical	—	CategoryTheory.Limits.Fork.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms kernelForkOfFork	—	—
mono_iff_cancel_zero 📖	mathematical	—	CategoryTheory.Mono Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.zero_of_comp_mono mono_of_cancel_zero
mono_iff_isZero_kernel 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.IsZero CategoryTheory.Limits.kernel preadditiveHasZeroMorphisms	—	mono_iff_isZero_kernel'
mono_iff_isZero_kernel' 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Limits.IsZero CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	—	CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono mono_of_isZero_kernel'
mono_of_cancel_zero 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	CategoryTheory.Mono	—	sub_eq_zero map_sub AddMonoidHom.instAddMonoidHomClass
mono_of_isZero_kernel 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Limits.kernel preadditiveHasZeroMorphisms	CategoryTheory.Mono	—	mono_of_isZero_kernel' CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero
mono_of_isZero_kernel' 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero preadditiveHasZeroMorphisms	CategoryTheory.Mono	—	mono_of_cancel_zero CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.zero_comp
mono_of_kernel_iso_zero 📖	mathematical	—	CategoryTheory.Mono	—	mono_of_kernel_zero CategoryTheory.Limits.zero_of_source_iso_zero
mono_of_kernel_zero 📖	mathematical	CategoryTheory.Limits.kernel.ι preadditiveHasZeroMorphisms Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Mono	—	mono_of_cancel_zero CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.comp_zero
neg_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	map_neg AddMonoidHom.instAddMonoidHomClass
neg_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' neg_comp
neg_comp_neg 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	comp_neg neg_comp neg_neg
neg_comp_neg_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' neg_comp_neg
neg_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Iso instNegIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	—
neg_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Iso instNegIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid homGroup	—	—
nsmul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	map_nsmul AddMonoidHom.instAddMonoidHomClass
smul_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom Units Int.instMonoid CategoryTheory.Iso instSMulUnitsIntIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	—
smul_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv Units Int.instMonoid CategoryTheory.Iso instSMulUnitsIntIso Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup Units.instInv	—	—
sub_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	map_sub AddMonoidHom.instAddMonoidHomClass
sub_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sub_comp
sum_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommGroup.toAddCommMonoid homGroup	—	map_sum AddMonoidHom.instAddMonoidHomClass
sum_comp' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommGroup.toAddCommMonoid homGroup	—	sum_comp
sum_comp'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommGroup.toAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sum_comp'
sum_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Finset.sum Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommGroup.toAddCommMonoid homGroup	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sum_comp
zsmul_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup homGroup	—	map_zsmul AddMonoidHom.instAddMonoidHomClass

CategoryTheory.Preadditive.IsIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left_eq_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.IsIso.eq_inv_comp CategoryTheory.Limits.comp_zero
comp_right_eq_zero 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	CategoryTheory.IsIso.eq_comp_inv CategoryTheory.Limits.zero_comp

---

← Back to Index