ComplexShape

📁 Source: Mathlib/Algebra/Homology/ComplexShape.lean

Statistics

Metric	Count
Definitions ComplexShape, down, down', instDecidableRelRelDown, instDecidableRelRelDown', instDecidableRelRelUp, instDecidableRelRelUp', next, prev, refl, trans, up, up'	13
Theorems down'_Rel, down'_mk, down_Rel, down_mk, ext, ext_iff, next_eq, next_eq', next_eq_self, next_eq_self', prev_eq, prev_eq', prev_eq_self, prev_eq_self', refl_Rel, subsingleton_next, subsingleton_prev, symm_Rel, symm_bijective, symm_symm, up'_Rel, up_Rel	22
Total	35

ComplexShape

Definitions

Name	Category	Theorems
down 📖	CompOp	472 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, embeddingUpIntDownInt_f, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, AlgebraicTopology.DoldKan.P_f_0_eq, ChainComplex.truncate_map_f, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, instHasNoLoopNatDown, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, AlgebraicTopology.NormalizedMooreComplex.obj_d, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, CategoryTheory.ProjectiveResolution.quasiIso, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d, CochainComplex.quasiIso_truncLEMap_iff, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', eulerCharSignsDownNat_χ, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, AlgebraicTopology.DoldKan.identity_N₂, groupHomology.eq_d₃₂_comp_inv, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, instIsTruncLENatIntEmbeddingUpIntLE, CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, groupHomology.chainsMap_id, SimplicialObject.Splitting.PInfty_comp_πSummand_id, Rep.barComplex.d_def, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp, ChainComplex.mk'_X_0, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Abelian.LeftResolution.chainComplexMap_id, instIsRelIffNatIntEmbeddingUpIntLE, AlgebraicTopology.DoldKan.PInfty_idem, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, groupHomology.comp_d₂₁_eq, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, AlgebraicTopology.DoldKan.QInfty_idem, ChainComplex.isoHomologyι₀_inv_naturality_assoc, ChainComplex.mk_X_2, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.Preadditive.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.self_π, CategoryTheory.ProjectiveResolution.cochainComplex_d, instHasNoLoopIntDown, Embedding.embeddingUpInt_areComplementary, Rep.standardComplex.d_eq, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CochainComplex.homotopyUnop_hom_eq, CategoryTheory.Functor.mapProjectiveResolution_π, ChainComplex.next, groupHomology.chainsMap_id_f_map_mono, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, groupHomology.d₁₀ArrowIso_hom_left, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, groupHomology.chainsMap_f_3_comp_chainsIso₃, ChainComplex.single₀ObjXSelf, groupHomology.eq_d₂₁_comp_inv, AlgebraicTopology.DoldKan.QInfty_idem_assoc, ε_down_ℕ, AlgebraicTopology.AlternatingFaceMapComplex.map_f, AlgebraicTopology.DoldKan.QInfty_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, ChainComplex.toSingle₀Equiv_apply_coe, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, CategoryTheory.Functor.mapProjectiveResolution_complex, AlgebraicTopology.alternatingFaceMapComplex_map_f, SimplicialObject.Splitting.nondegComplex_d, AlgebraicTopology.DoldKan.P_f_idem_assoc, Rep.standardComplex.εToSingle₀_comp_eq, AlgebraicTopology.DoldKan.Γ₀'_obj, groupHomology.inhomogeneousChains.d_def, ChainComplex.exactAt_succ_single_obj, ChainComplex.mk_d_1_0, CategoryTheory.Idempotents.DoldKan.hε, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, AlgebraicTopology.DoldKan.QInfty_f_0, CochainComplex.ConnectData.d_negSucc, ChainComplex.next_nat_succ, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc, Homotopy.dNext_zero_chainComplex, groupHomology.chainsMap_f_single, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc, Homotopy.prevD_chainComplex, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, ChainComplex.prev, AlgebraicTopology.DoldKan.map_Hσ, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, AlgebraicTopology.DoldKan.Γ₀_obj_map, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, down_Rel, groupHomology.map_chainsFunctor_shortExact, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, groupHomology.eq_d₃₂_comp_inv_apply, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, ChainComplex.augmentTruncate_inv_f_succ, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, ChainComplex.quasiIsoAt₀_iff, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, groupHomology.chainsMap_f_map_epi, CochainComplex.ConnectData.d_sub_two_sub_one, groupHomology.isoShortComplexH1_hom, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, groupHomology.comp_d₁₀_eq, CategoryTheory.ProjectiveResolution.of_def, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.ProjectiveResolution.π_f_succ, AlgebraicTopology.inclusionOfMooreComplex_app, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, AlgebraicTopology.DoldKan.P_f_idem, AlgebraicTopology.DoldKan.PInfty_idem_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, CochainComplex.ConnectData.restrictionLEIso_inv_f, groupHomology.chainsFunctor_obj, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, CategoryTheory.ProjectiveResolution.Hom.hom'_f, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, SimplicialObject.Splitting.nondegComplex_X, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, instIsRelIffNatIntEmbeddingDownNat, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, groupHomology.d₁₀ArrowIso_inv_right, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, ChainComplex.mk_X_0, groupHomology.chainsMap_id_f_map_epi, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, AlgebraicTopology.DoldKan.map_PInfty_f, AlgebraicTopology.DoldKan.P_succ, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, groupHomology.chainsMap_id_comp, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, SimplicialObject.Split.nondegComplexFunctor_map_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, eulerCharSignsDownInt_χ, AlgebraicTopology.DoldKan.Hσ_eq_zero, CochainComplex.ConnectData.d₀_comp, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, AlgebraicTopology.normalizedMooreComplex_objD, CategoryTheory.ProjectiveResolution.lift_commutes_zero, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, groupHomology.eq_d₂₁_comp_inv_assoc, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, instIsRelIffIntEmbeddingDownIntUpInt, CategoryTheory.ProjectiveResolution.leftDerived_app_eq, groupHomology.cyclesIso₀_inv_comp_iCycles, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, AlgebraicTopology.DoldKan.Q_idem_assoc, AlgebraicTopology.DoldKan.PInfty_f, ChainComplex.isoHomologyι₀_inv_naturality, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, AlgebraicTopology.DoldKan.Q_f_0_eq, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, CochainComplex.homotopyOp_hom_eq, AlgebraicTopology.DoldKan.QInfty_f_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, CochainComplex.instQuasiIsoIntιTruncLEOfIsLE, ChainComplex.next_nat_zero, ChainComplex.augmentTruncate_hom_f_succ, groupHomology.chainsMap_id_f_hom_eq_mapRange, groupHomology.toCycles_comp_isoCycles₂_hom, CategoryTheory.ProjectiveResolution.exact_succ, CategoryTheory.ProjectiveResolution.π'_f_zero, AlgebraicTopology.DoldKan.P_f_naturality_assoc, AlgebraicTopology.DoldKan.map_P, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, groupHomology.chainsMap_f_map_mono, groupHomology.eq_d₁₀_comp_inv, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, groupHomology.isoShortComplexH1_inv, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, groupHomology.eq_d₁₀_comp_inv_assoc, CochainComplex.ConnectData.restrictionLEIso_hom_f, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, groupHomology.lsingle_comp_chainsMap_f, AlgebraicTopology.DoldKan.P_idem, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, CategoryTheory.ProjectiveResolution.complex_d_succ_comp, AlgebraicTopology.DoldKan.Γ₀.map_app, Homotopy.dNext_succ_chainComplex, groupHomology.chainsMap_comp, AlgebraicTopology.DoldKan.natTransP_app, SimplicialObject.Split.nondegComplexFunctor_obj, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, AlgebraicTopology.DoldKan.N₁_obj_X, AlgebraicTopology.map_alternatingFaceMapComplex, CategoryTheory.ProjectiveResolution.hasHomology, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_obj, AlgebraicTopology.DoldKan.Q_is_eventually_constant, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, CategoryTheory.ProjectiveResolution.extMk_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, ChainComplex.mk'_d, CategoryTheory.ProjectiveResolution.self_complex, groupHomology.eq_d₃₂_comp_inv_assoc, AlgebraicTopology.DoldKan.Q_succ, AlgebraicTopology.DoldKan.natTransPInfty_f_app, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, Rep.standardComplex.d_comp_ε, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, AlgebraicTopology.NormalizedMooreComplex.map_f, down_mk, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, CochainComplex.ConnectData.X_negOne, CategoryTheory.Abelian.DoldKan.equivalence_inverse, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupHomology.isoShortComplexH2_hom, ChainComplex.augmentTruncate_hom_f_zero, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, CochainComplex.ConnectData.X_negSucc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, AlgebraicTopology.DoldKan.hσ'_eq, groupHomology.chainsMap_f_2_comp_chainsIso₂, AlgebraicTopology.DoldKan.MorphComponents.id_a, groupHomology.pOpcycles_comp_opcyclesIso_hom, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, ChainComplex.instHasHomologyNatObjAlternatingConst, AlgebraicTopology.DoldKan.PInfty_f_0, ChainComplex.ofHom_f, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, AlgebraicTopology.DoldKan.PInfty_f_naturality, AlgebraicTopology.DoldKan.hσ'_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, CochainComplex.quasiIso_ιTruncLE_iff, ChainComplex.isIso_homologyι₀, ChainComplex.truncate_obj_d, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, Rep.FiniteCyclicGroup.resolution_complex, groupHomology.chainsFunctor_map, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, instQFactorsThroughHomotopyDown, embeddingUpIntLE_f, groupHomology.chainsMap_f_hom, AlgebraicTopology.DoldKan.P_is_eventually_constant, AlgebraicTopology.DoldKan.map_Q, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, CochainComplex.ConnectData.map_id, AlgebraicTopology.DoldKan.PInfty_f_idem, AlgebraicTopology.DoldKan.N₂_obj_p_f, groupHomology.cyclesMk₁_eq, AlgebraicTopology.DoldKan.σ_comp_PInfty, embeddingDownNat_f, AlgebraicTopology.NormalizedMooreComplex.obj_X, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, AlgebraicTopology.DoldKan.N₂_obj_X_X, hasNoLoop_down, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, ChainComplex.linearYonedaObj_d, Rep.standardComplex.instQuasiIsoNatεToSingle₀, Rep.standardComplex.x_projective, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, CochainComplex.ConnectData.d₀_comp_assoc, ChainComplex.fromSingle₀Equiv_apply, Rep.FiniteCyclicGroup.resolution_quasiIso, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, ChainComplex.chainComplex_d_succ_succ_zero, CategoryTheory.Idempotents.DoldKan.equivalence_functor, AlgebraicTopology.DoldKan.N₂_obj_X_d, groupHomology.isoCycles₁_hom_comp_i_assoc, CategoryTheory.Abelian.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.exact₀, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CochainComplex.ConnectData.comp_d₀, ChainComplex.augmentTruncate_inv_f_zero, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, instIsTruncLENatIntEmbeddingDownNat, ChainComplex.of_x, CategoryTheory.Idempotents.DoldKan.Γ_map_app, CategoryTheory.ProjectiveResolution.projective, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, ChainComplex.alternatingConst_exactAt, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.chainsMap_zero, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, groupHomology.isoShortComplexH2_inv, groupHomology.toCycles_comp_isoCycles₁_hom, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, AlgebraicTopology.DoldKan.QInfty_f_idem, groupHomology.isoCycles₂_hom_comp_i, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, groupHomology.isoCycles₂_inv_comp_iCycles, ChainComplex.mk'_X_1, ChainComplex.mk_d, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, CochainComplex.ConnectData.comp_d₀_assoc, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, groupHomology.d₁₀ArrowIso_hom_right, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, ChainComplex.mk'_d_1_0, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, groupHomology.inhomogeneousChains.d_eq, groupHomology.eq_d₂₁_comp_inv_apply, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.decomposition_Q, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, embeddingDownIntUpInt_f, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, AlgebraicTopology.DoldKan.Q_f_idem_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, AlgebraicTopology.DoldKan.Γ₂N₁_inv, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, AlgebraicTopology.DoldKan.Q_f_naturality, AlgebraicTopology.DoldKan.Q_zero, groupHomology.lsingle_comp_chainsMap_f_assoc, ChainComplex.of_d, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, ChainComplex.truncate_obj_X, AlgebraicTopology.DoldKan.identity_N₂_objectwise, AlgebraicTopology.inclusionOfMooreComplexMap_f, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, CategoryTheory.Idempotents.DoldKan.hη, CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', dNext_nat, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, CategoryTheory.ProjectiveResolution.ofComplex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, AlgebraicTopology.DoldKan.map_hσ', AlgebraicTopology.DoldKan.N₂_map_f_f, AlgebraicTopology.DoldKan.P_f_naturality, instIsRelIffIntEmbeddingUpIntDownInt, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, AlgebraicTopology.DoldKan.N₁Γ₀_app, groupHomology.eq_d₁₀_comp_inv_apply, ChainComplex.alternatingConst_map_f, CategoryTheory.Idempotents.DoldKan.N_map, ChainComplex.single₀_obj_zero, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, ChainComplex.of_d_ne, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, ChainComplex.single₀_map_f_zero, ChainComplex.alternatingConst_obj, ChainComplex.mk_d_2_1, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, AlgebraicTopology.DoldKan.Γ₀'_map_f, boundaryLE_embeddingUpIntLE_iff, Rep.FiniteCyclicGroup.resolution.π_f, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀, AlgebraicTopology.DoldKan.Γ₂N₂_inv, groupHomology.isoCycles₂_hom_comp_i_assoc, groupHomology.comp_d₃₂_eq, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, groupHomology.chainsMap_f_0_comp_chainsIso₀, AlgebraicTopology.normalizedMooreComplex_obj, AlgebraicTopology.DoldKan.natTransQ_app, CategoryTheory.ProjectiveResolution.complex_exactAt_succ, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, ChainComplex.map_chain_complex_of, CategoryTheory.instIsIsoFromLeftDerivedZero', ChainComplex.mk_X_1, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.chainsMap_f, AlgebraicTopology.DoldKan.PInfty_add_QInfty, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, AlgebraicTopology.DoldKan.Q_f_idem, ChainComplex.linearYonedaObj_X
down' 📖	CompOp	6 math math: instIsTruncLEEmbeddingDown'Add, embeddingDown'Add_f, down'_Rel, hasNoLoop_down', down'_mk, instIsRelIffEmbeddingDown'Add
instDecidableRelRelDown 📖	CompOp	5 math math: Rep.FiniteCyclicGroup.chainComplexFunctor_obj, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, ChainComplex.alternatingConst_map_f, ChainComplex.alternatingConst_obj, Rep.FiniteCyclicGroup.resolution.π_f
instDecidableRelRelDown' 📖	CompOp	—
instDecidableRelRelUp 📖	CompOp	—
instDecidableRelRelUp' 📖	CompOp	—
next 📖	CompOp	21 math math: CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, ChainComplex.next, HomologicalComplex.mapBifunctorMapHomotopy.comm₁, ChainComplex.next_nat_succ, HomologicalComplex.shortComplexFunctor_map_τ₁, HomologicalComplex.shortComplexFunctor_map_τ₃, ChainComplex.next_nat_zero, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, CochainComplex.next, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, next_π₁, HomologicalComplex.shortComplexFunctor_map_τ₂, HomologicalComplex.shortComplexFunctor_obj_g, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, next_eq_self', CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, next_π₂, next_eq', HomologicalComplex.shortComplexFunctor_obj_X₃
prev 📖	CompOp	20 math math: CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, HomologicalComplex.mapBifunctorMapHomotopy.comm₁, ChainComplex.prev, HomologicalComplex.shortComplexFunctor_map_τ₁, HomologicalComplex.shortComplexFunctor_map_τ₃, HomologicalComplex.shortComplexFunctor_obj_f, prev_eq', CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, CochainComplex.prev_nat_succ, HomologicalComplex.shortComplexFunctor_obj_X₁, prev_eq_self', prev_π₁, HomologicalComplex.shortComplexFunctor_map_τ₂, CochainComplex.prev, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, CochainComplex.prev_nat_zero, prev_π₂
refl 📖	CompOp	1 math math: refl_Rel
trans 📖	CompOp	—
up 📖	CompOp	754 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, CategoryTheory.InjectiveResolution.injective, CategoryTheory.InjectiveResolution.Hom.hom'_f, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, embeddingUpIntDownInt_f, CochainComplex.triangleOfDegreewiseSplit_obj₁, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, CochainComplex.HomComplex.Cochain.fromSingleMk_neg, CochainComplex.mappingCone.δ_inl, CochainComplex.mappingCone.inl_v_descCochain_v_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, groupCohomology.toCocycles_comp_isoCocycles₁_hom, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, DerivedCategory.right_fac, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_id, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, CochainComplex.mappingCone.inr_f_d_assoc, CochainComplex.HomComplex.Cochain.δ_single, CochainComplex.mappingConeCompTriangle_obj₂, groupCohomology.inhomogeneousCochains.d_def, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, CochainComplex.isStrictlyGE_shift, CochainComplex.mappingCone.id, CochainComplex.shiftFunctorZero_eq, groupCohomology.cocyclesIso₀_hom_comp_f, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CochainComplex.mappingCone.liftCochain_v_snd_v_assoc, CochainComplex.augmentTruncate_inv_f_zero, groupCohomology.eq_d₀₁_comp_inv, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.isStrictlyLE_iff, CochainComplex.HomComplex.Cochain.leftShift_smul, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, groupCohomology.eq_d₁₂_comp_inv, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, CochainComplex.mappingCone.triangle_mor₁, HomologicalComplex₂.shiftFunctor₂XXIso_refl, CochainComplex.mappingCone.liftCochain_v_snd_v, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, instIsTruncLENatIntEmbeddingUpIntLE, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle, CategoryTheory.InjectiveResolution.self_ι, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CochainComplex.mk'_X_0, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, instIsRelIffNatIntEmbeddingUpIntLE, CochainComplex.isoHomologyπ₀_inv_naturality_assoc, CochainComplex.instLinearIntFunctorSingleFunctors, CochainComplex.ConnectData.d_ofNat, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, CochainComplex.mappingCone.d_snd_v, CochainComplex.HomComplex.Cochain.rightUnshift_neg, CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CochainComplex.HomComplex.Cochain.map_v, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, CochainComplex.truncate_obj_X, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app, groupCohomology.cochainsMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, CochainComplex.HomComplex.leftHomologyData_K_coe, CochainComplex.mappingConeCompTriangle_mor₃, groupCohomology.comp_d₁₂_eq, CochainComplex.HomComplex.Cochain.shift_add, CategoryTheory.InjectiveResolution.of_def, CochainComplex.HomComplex.Cochain.comp_id, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.ProjectiveResolution.cochainComplex_d, CochainComplex.HomComplex.Cochain.toSingleMk_neg, CochainComplex.HomComplex.Cochain.ofHom_v_comp_d, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, CochainComplex.HomComplex.Cochain.map_zero, CochainComplex.cm5b.fac, groupCohomology.dArrowIso₀₁_inv_right, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, CochainComplex.ConnectData.d_zero_one, CochainComplex.HomComplex.Cochain.toSingleMk_v, groupCohomology.eq_d₂₃_comp_inv_assoc, CochainComplex.HomComplex.leftHomologyData'_i, CochainComplex.IsKInjective.rightOrthogonal, groupCohomology.eq_d₂₃_comp_inv_apply, CategoryTheory.InjectiveResolution.complex_d_comp, groupCohomology.eq_d₁₂_comp_inv_apply, CochainComplex.ConnectData.cochainComplex_X, CochainComplex.IsKInjective.Qh_map_bijective, Embedding.embeddingUpInt_areComplementary, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, CochainComplex.HomComplex.Cochain.shift_neg, HomotopyCategory.instIsHomologicalIntUpHomologyFunctor, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, Homotopy.prevD_succ_cochainComplex, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, CochainComplex.homotopyUnop_hom_eq, CochainComplex.HomComplex.Cochain.toSingleMk_add, CochainComplex.mappingCone.inr_f_d, CategoryTheory.instIsIsoToRightDerivedZero', CochainComplex.HomComplex.δ_v, CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle, CochainComplex.HomComplex.Cochain.comp_v, CochainComplex.fromSingle₀Equiv_apply_coe, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, CochainComplex.HomComplex.Cochain.neg_v, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, CochainComplex.HomComplex.Cochain.sub_v, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, CochainComplex.of_d, CochainComplex.mappingCone.liftCochain_v_descCochain_v, CochainComplex.mappingCone.lift_f_fst_v, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CochainComplex.XIsoOfEq_shift, CochainComplex.HomComplex.Cochain.rightUnshift_comp, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, eulerCharSignsUpInt_χ, CochainComplex.mappingCone.inr_triangleδ, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, CochainComplex.HomComplex.Cochain.ofHoms_comp, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CochainComplex.HomComplex.leftHomologyData_π_hom_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, CochainComplex.mappingCone.id_X, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CochainComplex.HomComplex.Cochain.single_zero, CochainComplex.mappingCone.inr_descShortComplex_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, groupCohomology.dArrowIso₀₁_hom_right, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, groupCohomology.toCocycles_comp_isoCocycles₂_hom, HomotopyCategory.instAdditiveIntUpShiftFunctor, CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp, CochainComplex.mappingCone.d_snd_v'_assoc, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, CochainComplex.HomComplex.Cochain.shift_zero, CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CochainComplex.shiftFunctorZero_inv_app_f, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.HomComplex.Cochain.leftShift_comp, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, CochainComplex.triangleOfDegreewiseSplit_obj₂, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, CochainComplex.homologyFunctor_shift, CochainComplex.of_d_ne, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, groupCohomology.comp_d₂₃_eq, CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CategoryTheory.InjectiveResolution.ι_f_succ, CochainComplex.isKInjective_shift_iff, CochainComplex.isStrictlyGE_iff, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, CochainComplex.mappingCone.lift_f_fst_v_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, CochainComplex.HomComplex.Cochain.leftShift_rightShift, embeddingUpNat_f, CochainComplex.HomComplex.Cochain.ofHom_neg, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, groupCohomology.cochainsMap_f_map_epi, groupCohomology.comp_d₀₁_eq, CochainComplex.HomComplex.Cochain.zero_v, DerivedCategory.instLinearCochainComplexIntQ, instIsTruncGENatIntEmbeddingUpIntGE, CochainComplex.isZero_of_isStrictlyLE, CochainComplex.mk_d_2_0, prevD_nat, CategoryTheory.InjectiveResolution.extMk_zero, CochainComplex.isoHomologyπ₀_inv_naturality, groupCohomology.cochainsMap_zero, CochainComplex.instAdditiveIntFunctorSingleFunctors, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, groupCohomology.dArrowIso₀₁_inv_left, CochainComplex.exactAt_succ_single_obj, HomotopyCategory.mappingCone_triangleh_distinguished, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, CochainComplex.mk'_X_1, CochainComplex.HomComplex.Cochain.map_add, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.ProjectiveResolution.extMk_hom, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, CochainComplex.HomComplex.Cochain.fromSingleMk_v, CochainComplex.HomComplex.Cochain.fromSingleMk_add, CochainComplex.single₀_map_f_zero, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, CochainComplex.HomComplex.Cochain.shift_smul, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, CochainComplex.HomComplex.Cochain.ofHomotopy_refl, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, CochainComplex.mappingCone.ext_from_iff, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, groupCohomology.cochainsMap_id_comp, DerivedCategory.instIsIsoMapCochainComplexIntQ, CochainComplex.HomComplex.Cocycle.toSingleMk_zero, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, CochainComplex.HomComplex.Cochain.leftUnshift_v, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, groupCohomology.cochainsMap_comp_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, up_Rel, CochainComplex.HomComplex.Cochain.rightShift_leftShift, instQFactorsThroughHomotopyIntUp, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.HomComplex.Cochain.ofHom_sub, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, DerivedCategory.instAdditiveHomotopyCategoryIntUpQh, groupCohomology.isoCocycles₂_hom_comp_i, CochainComplex.HomComplex.Cochain.leftUnshift_smul, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CochainComplex.HomComplex.Cochain.shiftLinearMap_apply, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso, groupCohomology.dArrowIso₀₁_hom_left, HomologicalComplex₂.shiftFunctor₁XXIso_refl, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp_assoc, CochainComplex.shiftFunctor_map_f', groupCohomology.eq_d₀₁_comp_inv_apply, CochainComplex.mappingCone.ext_to_iff, CochainComplex.ConnectData.restrictionLEIso_inv_f, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π', CochainComplex.HomComplex.Cochain.rightShift_zero, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.ProjectiveResolution.Hom.hom'_f, CochainComplex.singleFunctor_obj_d, CochainComplex.quasiIso_shift_iff, CochainComplex.HomComplex.Cochain.rightUnshift_v, HomotopyCategory.composableArrowsFunctor_obj, instIsRelIffNatIntEmbeddingDownNat, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, CochainComplex.shiftFunctorAdd'_inv_app_f', CochainComplex.exactAt_of_isLE, DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, CochainComplex.mappingCone.map_inr, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, CochainComplex.shiftFunctorAdd'_eq, CochainComplex.shiftFunctorAdd'_inv_app_f, HomotopyCategory.instLinearIntUpShiftFunctor, CochainComplex.mappingCone.liftCochain_v_fst_v, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, CochainComplex.HomComplex.Cochain.fromSingleMk_zero, CochainComplex.mappingCone.decomp_from, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, CochainComplex.ConnectData.X_zero, HomotopyCategory.Pretriangulated.distinguished_cocone_triangle, groupCohomology.cochainsMap_id_f_map_mono, CochainComplex.mappingConeCompTriangle_mor₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, CochainComplex.of_x, CochainComplex.HomComplex.Cochain.leftShift_zero, CochainComplex.mappingCone.inl_v_snd_v_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc, CochainComplex.instLinearIntShiftFunctor, CochainComplex.triangleOfDegreewiseSplit_mor₂, HomotopyCategory.instLinearIntUpSingleFunctor, CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, DerivedCategory.isLE_Q_obj_iff, CochainComplex.cm5b.fac_assoc, CochainComplex.ConnectData.d₀_comp, HomotopyCategory.instAdditiveIntUpSingleFunctor, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv, CochainComplex.triangleOfDegreewiseSplit_obj₃, CochainComplex.shiftFunctorZero'_hom_app_f, CategoryTheory.InjectiveResolution.self_cocomplex, groupCohomology.isoCocycles₁_inv_comp_iCocycles, HomotopyCategory.Pretriangulated.contractible_distinguished, instIsRelIffNatIntEmbeddingUpIntGE, instIsRelIffIntEmbeddingDownIntUpInt, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, CochainComplex.mappingCone.triangle_mor₂, CochainComplex.HomComplex.Cocycle.leftUnshift_coe, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, CochainComplex.mappingCone.d_snd_v_assoc, CochainComplex.instAdditiveIntShiftFunctor, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, CochainComplex.shiftFunctor_map_f, CochainComplex.quasiIsoAt_shift_iff, CochainComplex.mappingCone.d_snd_v', CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, CochainComplex.instIsKProjectiveObjIntShiftFunctor, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, CochainComplex.HomComplex.Cochain.rightShift_smul, CochainComplex.HomComplex.Cochain.map_comp, CochainComplex.ConnectData.X_ofNat, CochainComplex.homotopyOp_hom_eq, CochainComplex.mappingCone.inr_f_descCochain_v_assoc, CochainComplex.HomComplex.Cochain.map_sub, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, CochainComplex.HomComplex.Cocycle.homOf_f, CochainComplex.IsKProjective.Qh_map_bijective, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.homOfDegreewiseSplit_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, CochainComplex.shiftFunctorAdd_inv_app_f, boundaryGE_embeddingUpIntGE_iff, DerivedCategory.isGE_Q_obj_iff, CochainComplex.truncate_map_f, CochainComplex.mappingCone.map_id, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app, CochainComplex.prev_nat_succ, CochainComplex.mappingConeCompTriangle_obj₃, DerivedCategory.instEssSurjHomotopyCategoryIntUpQh, CategoryTheory.ProjectiveResolution.π'_f_zero, CochainComplex.mappingCone.inl_v_fst_v, CategoryTheory.InjectiveResolution.desc_commutes, CochainComplex.isLE_iff, CochainComplex.ConnectData.cochainComplex_d, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, CategoryTheory.InjectiveResolution.desc_commutes_assoc, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, CochainComplex.exists_iso_single, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, CochainComplex.HomComplex.Cochain.shift_units_smul, HomotopyCategory.instIsTriangulatedIntUp, CochainComplex.ConnectData.restrictionLEIso_hom_f, CochainComplex.exactAt_of_isGE, CochainComplex.shiftFunctorAdd_eq, DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, CochainComplex.mappingCone.inr_f_descCochain_v, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, CochainComplex.cm5b.instQuasiIsoIntP, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CochainComplex.mappingCone.isZero_X_iff, groupCohomology.cochainsMap_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc, groupCohomology.cocyclesMk₁_eq, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.HomComplex.δ_zero_cochain_v, CochainComplex.HomComplex.Cochain.units_smul_v, CochainComplex.HomComplex.Cochain.δ_toSingleMk, CochainComplex.cm5b.instMonoFIntI, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, CochainComplex.HomComplex.Cochain.fromSingleMk_precomp, CochainComplex.HomComplex.Cochain.leftUnshift_add, CochainComplex.isGE_iff, CochainComplex.HomComplex.Cocycle.fromSingleMk_zero, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, hasNoLoop_up, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom, CochainComplex.mappingCone.inr_f_fst_v_assoc, CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, CochainComplex.mappingCone.inl_v_d_assoc, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, CochainComplex.HomComplex.Cochain.rightShift_units_smul, CochainComplex.isZero_of_isStrictlyGE, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, CochainComplex.next, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory, CochainComplex.HomComplex.Cochain.rightUnshift_smul, HomotopyCategory.composableArrowsFunctor_map, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc, CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CochainComplex.HomComplex.Cochain.smul_v, CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, CochainComplex.HomComplex.Cochain.fromSingleMk_sub, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, CochainComplex.IsKProjective.leftOrthogonal, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app, CochainComplex.cm5b.instInjectiveXIntI, CochainComplex.cm5b.instMonoIntI, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, instIsRelIffNatIntEmbeddingUpNat, CategoryTheory.NatTrans.rightDerivedToHomotopyCategory_comp, groupCohomology.eq_d₂₃_comp_inv, CochainComplex.isKProjective_iff_leftOrthogonal, groupCohomology.cochainsMap_f_map_mono, groupCohomology.isoShortComplexH1_hom, CategoryTheory.InjectiveResolution.cochainComplex_d_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles, eulerCharSignsUpNat_χ, CochainComplex.shortComplexTruncLE_shortExact, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.cm5b.i_f_comp, CochainComplex.HomComplex.Cochain.δ_rightUnshift, CochainComplex.mappingCone.inr_snd, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, CochainComplex.mappingCone.decomp_to, CochainComplex.HomComplex.leftHomologyData_H_coe, inhomogeneousCochains.d_eq, CochainComplex.HomComplex.leftHomologyData'_K_coe, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, CochainComplex.mappingCone.inl_fst, CochainComplex.quasiIsoAt₀_iff, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, CochainComplex.HomComplex.Cocycle.shift_coe, groupCohomology.cocyclesMk₂_eq, embeddingUpIntLE_f, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, groupCohomology.cochainsMap_id_f_map_epi, HomotopyCategory.mem_subcategoryAcyclic_iff, CochainComplex.isStrictlyLE_shift, CochainComplex.ConnectData.restrictionGEIso_inv_f, CochainComplex.instFullIntSingleFunctor, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.HomComplex.Cochain.δ_rightShift, DerivedCategory.right_fac_of_isStrictlyLE, CochainComplex.ConnectData.map_id, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.mappingCone.d_fst_v'_assoc, CochainComplex.HomComplex.Cochain.rightUnshift_add, CochainComplex.HomComplex.Cochain.toSingleMk_zero, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, embeddingDownNat_f, groupCohomology.isoCocycles₁_hom_comp_i, HomotopyCategory.homologyFunctor_shiftMap_assoc, CochainComplex.augmentTruncate_inv_f_succ, CochainComplex.mappingCone.inl_v_d, CochainComplex.isZero_of_isGE, CochainComplex.shiftFunctor_obj_X', HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, CochainComplex.HomComplex.Cochain.shift_v, σ_def, CochainComplex.shiftFunctorZero_hom_app_f, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, CochainComplex.mappingCone.inr_f_snd_v_assoc, ChainComplex.linearYonedaObj_d, CochainComplex.mk_X_2, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, Homotopy.prevD_zero_cochainComplex, CochainComplex.triangleOfDegreewiseSplit_mor₃, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, CochainComplex.HomComplex.Cochain.shiftAddHom_apply, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, CochainComplex.HomComplex.Cochain.δ_leftUnshift, HomotopyCategory.spectralObjectMappingCone_ω₁, CochainComplex.ConnectData.d₀_comp_assoc, CochainComplex.mappingCone.d_fst_v', CategoryTheory.InjectiveResolution.desc_commutes_zero, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, CochainComplex.shiftFunctorAdd'_hom_app_f', CochainComplex.mappingCone.inl_v_descCochain_v, CochainComplex.HomComplex.Cochain.leftShift_add, CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, CochainComplex.augmentTruncate_hom_f_succ, groupCohomology.cochainsMap_f_hom, CochainComplex.shiftEval_hom_app, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, CochainComplex.cm5b.i_f_comp_assoc, CochainComplex.HomComplex_X, CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, CochainComplex.HomComplex.leftHomologyData'_H_coe, AlgebraicTopology.alternatingCofaceMapComplex_map, CochainComplex.mappingCone.triangleRotateShortComplex_g, CochainComplex.shiftFunctor_obj_d', CochainComplex.instHasMapBifunctorObjIntShiftFunctor, CochainComplex.HomComplex.Cocycle.equivHom_apply, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, CochainComplex.mappingCone.inr_descShortComplex, DerivedCategory.instAdditiveCochainComplexIntQ, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, groupCohomology.isoShortComplexH2_hom, CochainComplex.cm5b.I_d, CochainComplex.triangleOfDegreewiseSplit_mor₁, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, CategoryTheory.InjectiveResolution.hasHomology, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, CochainComplex.HomComplex.Cochain.d_comp_ofHom_v, CochainComplex.HomComplex.Cochain.leftShift_units_smul, CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe, CochainComplex.ConnectData.comp_d₀, HomotopyCategory.homologyShiftIso_hom_app, CochainComplex.shiftFunctorAdd_hom_app_f, instIsTruncLENatIntEmbeddingDownNat, DerivedCategory.Qh_obj_singleFunctors_obj, CochainComplex.HomComplex.δ_map, CochainComplex.ofHom_f, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, CochainComplex.mappingCone.inl_v_descShortComplex_f, CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v, CochainComplex.HomComplex.Cochain.toSingleMk_postcomp, CochainComplex.HomComplex.Cochain.ofHom_add, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, CochainComplex.mappingCone.inr_f_descShortComplex_f, CochainComplex.toSingle₀Equiv_apply, CochainComplex.HomComplex.Cochain.id_comp, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', CochainComplex.HomComplex.Cochain.single_v_eq_zero', DerivedCategory.exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, CochainComplex.shiftFunctorAdd'_hom_app_f, DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh, CochainComplex.HomComplex.Cochain.ofHom_zero, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CochainComplex.HomComplex.leftHomologyData'_π, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, CochainComplex.cochainComplex_d_succ_succ_zero, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, CochainComplex.HomComplex.Cochain.map_ofHom, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, CochainComplex.shiftFunctorComm_hom_app_f, groupCohomology.iCocycles_mk, CochainComplex.mappingCone.inl_v_snd_v, groupCohomology.map_cochainsFunctor_shortExact, instHasNoLoopIntUp, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, HomotopyCategory.Pretriangulated.rotate_distinguished_triangle, CochainComplex.HomComplex.Cochain.rightShift_neg, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, CategoryTheory.InjectiveResolution.exact_succ, HomotopyCategory.quotient_obj_singleFunctors_obj, CochainComplex.ConnectData.comp_d₀_assoc, CategoryTheory.InjectiveResolution.instMonoFNatι, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, DerivedCategory.instEssSurjCochainComplexIntQ, CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, Homotopy.dNext_cochainComplex, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, CochainComplex.mk'_d_1_0, CochainComplex.prev, CochainComplex.shiftEval_inv_app, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, instHasNoLoopNatUp, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, groupCohomology.cochainsFunctor_map, CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom, ε_up_ℤ, CategoryTheory.InjectiveResolution.exact₀, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, HomotopyCategory.homologyFunctor_shiftMap, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, CochainComplex.mappingCone.lift_f_snd_v, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, CochainComplex.isKProjective_shift_iff, embeddingDownIntUpInt_f, CochainComplex.instIsStrictlyLEObjIntSingleFunctor, embeddingUpIntGE_f, CochainComplex.mappingCone.triangle_obj₂, CochainComplex.instIsStrictlyGEObjIntSingleFunctor, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, CochainComplex.mappingConeCompTriangle_mor₂, DerivedCategory.instLinearHomotopyCategoryIntUpQh, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_zero, groupCohomology.cocyclesMk₀_eq, CochainComplex.mappingConeCompTriangleh_comm₁, CochainComplex.HomComplex.Cocycle.leftShift_coe, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, groupCohomology.isoShortComplexH1_inv, CochainComplex.single₀_obj_zero, CochainComplex.HomComplex.Cochain.shift_v', CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, CategoryTheory.InjectiveResolution.ofCocomplex_exactAt_succ, DerivedCategory.mem_distTriang_iff, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc, CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex, CochainComplex.isKInjective_iff_rightOrthogonal, CochainComplex.HomComplex.Cochain.rightShift_add, CochainComplex.ShiftSequence.shiftIso_inv_app, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, groupCohomology.cochainsMap_id_comp_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, CochainComplex.HomComplex.Cochain.diff_v, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, CochainComplex.isGE_shift, CochainComplex.truncate_obj_d, CochainComplex.HomComplex.δ_neg_one_cochain, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, CochainComplex.HomComplex.Cochain.ofHoms_zero, DerivedCategory.Q_map_eq_of_homotopy, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app, groupCohomology.eq_d₁₂_comp_inv_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_f, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CochainComplex.HomComplex.Cocycle.rightUnshift_coe, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, instIsRelIffIntEmbeddingUpIntDownInt, CochainComplex.mappingCone.lift_f, CochainComplex.HomComplex.Cochain.δ_leftShift, DerivedCategory.isIso_Q_map_iff_quasiIso, DerivedCategory.isIso_Qh_map_iff, CochainComplex.HomComplex.CohomologyClass.toHom_mk, CochainComplex.isIso_homologyπ₀, CochainComplex.HomComplex.Cochain.add_v, groupCohomology.isoShortComplexH2_inv, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, DerivedCategory.left_fac_of_isStrictlyGE, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, groupCohomology.isoCocycles₂_hom_comp_i_assoc, CochainComplex.augmentTruncate_hom_f_zero, CochainComplex.mappingCone.inl_v_fst_v_assoc, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, CategoryTheory.InjectiveResolution.quasiIso, CochainComplex.mk_d_1_0, HomotopyCategory.mappingConeCompTriangleh_distinguished, CochainComplex.HomComplex.Cochain.leftShift_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, groupCohomology.eq_d₀₁_comp_inv_assoc, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CochainComplex.HomComplex.Cochain.toSingleMk_sub, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom, groupCohomology.isoCocycles₁_hom_comp_i_assoc, CategoryTheory.InjectiveResolution.descFOne_zero_comm, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, CochainComplex.HomComplex.Cochain.leftUnshift_neg, CochainComplex.isLE_shift, CochainComplex.mappingCone.triangle_obj₁, HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic, CochainComplex.mappingCone.lift_f_snd_v_assoc, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, boundaryLE_embeddingUpIntLE_iff, CochainComplex.cm5b, groupCohomology.cochainsFunctor_obj, CategoryTheory.InjectiveResolution.rightDerived_app_eq, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom', CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, CategoryTheory.InjectiveResolution.instInjectiveXIntCochainComplex, CochainComplex.shiftFunctor_obj_d, CochainComplex.HomComplex.Cochain.toSingleMk_precomp, CochainComplex.HomComplex.Cocycle.rightShift_coe, CochainComplex.mappingCone.d_fst_v, CochainComplex.single₀ObjXSelf, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, CochainComplex.prev_nat_zero, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, CochainComplex.HomComplex.Cochain.leftUnshift_zero, CochainComplex.mk_X_0, DerivedCategory.left_fac, CochainComplex.mappingCone.triangle_obj₃, CochainComplex.HomComplex.Cochain.map_neg, CochainComplex.isZero_of_isLE, CochainComplex.HomComplex_d_hom_apply, CochainComplex.instFaithfulIntSingleFunctor, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, CochainComplex.mappingConeCompTriangle_obj₁, CochainComplex.cm5b.I_X, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor, instIsTruncGENatIntEmbeddingUpNat, CochainComplex.mk_X_1, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f, CochainComplex.ShiftSequence.shiftIso_hom_app, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, groupCohomology.cochainsMap_id, CochainComplex.HomComplex.Cochain.single_v_eq_zero, CategoryTheory.InjectiveResolution.cochainComplex_d, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, CochainComplex.mappingCone.map_δ, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic, CochainComplex.HomComplex.Cochain.ofHom_comp, CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq, ChainComplex.linearYonedaObj_X, CochainComplex.ConnectData.restrictionGEIso_hom_f, DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso
up' 📖	CompOp	21 math math: HomologicalComplex.dgoToHomologicalComplex_obj_d, HomologicalComplex.dgoEquivHomologicalComplex_unitIso, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f, HomologicalComplex.dgoEquivHomologicalComplex_functor, HomologicalComplex.dgoToHomologicalComplex_obj_X, embeddingUp'Add_f, HomologicalComplex.dgoEquivHomologicalComplex_counitIso, HomologicalComplex.homologicalComplexToDGO_map_f, instIsTruncGEEmbeddingUp'Add, HomologicalComplex.dgoToHomologicalComplex_map_f, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, HomologicalComplex.homologicalComplexToDGO_obj_d, HomologicalComplex.d_eqToHom_assoc, instIsRelIffEmbeddingUp'Add, HomologicalComplex.homologicalComplexToDGO_obj_obj, hasNoLoop_up', HomologicalComplex.dgoEquivHomologicalComplex_inverse, HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f, HomologicalComplex.d_eqToHom, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, up'_Rel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
down'_Rel 📖	mathematical	—	Rel down'	—	—
down'_mk 📖	mathematical	—	Rel down'	—	—
down_Rel 📖	mathematical	—	Rel down	—	—
down_mk 📖	mathematical	—	Rel down	—	—
ext 📖	—	Rel	—	—	—
ext_iff 📖	mathematical	—	Rel	—	ext
next_eq 📖	—	Rel	—	—	—
next_eq' 📖	mathematical	Rel	next	—	next_eq next.eq_1
next_eq_self 📖	—	Rel next	—	—	next_eq_self' next_eq'
next_eq_self' 📖	mathematical	Rel	next	—	—
prev_eq 📖	—	Rel	—	—	—
prev_eq' 📖	mathematical	Rel	prev	—	prev_eq prev.eq_1
prev_eq_self 📖	—	Rel prev	—	—	prev_eq_self' prev_eq'
prev_eq_self' 📖	mathematical	Rel	prev	—	—
refl_Rel 📖	mathematical	—	Rel refl	—	—
subsingleton_next 📖	mathematical	—	Rel	—	next_eq
subsingleton_prev 📖	mathematical	—	Rel	—	prev_eq
symm_Rel 📖	mathematical	—	Rel symm	—	—
symm_bijective 📖	mathematical	—	Function.Bijective ComplexShape symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	—
up'_Rel 📖	mathematical	—	Rel up'	—	—
up_Rel 📖	mathematical	—	Rel up	—	—

(root)

Definitions

Name	Category	Theorems
ComplexShape 📖	CompData	1 math math: ComplexShape.symm_bijective

---

← Back to Index