CochainComplex

📁 Source: Mathlib/Algebra/Homology/Embedding/CochainComplex.lean

Statistics

Metric	Count
Definitions CochainComplex, IsGE, IsLE, IsStrictlyGE, IsStrictlyLE, shortComplexTruncLE, shortComplexTruncLEX₃ToTruncGE, truncGE, truncGEMap, truncLE, truncLEMap, ιTruncLE, πTruncGE	13
Theorems exactAt_of_isGE, exactAt_of_isLE, exists_iso_single, g_shortComplexTruncLEX₃ToTruncGE, g_shortComplexTruncLEX₃ToTruncGE_assoc, instIsIsoIntιTruncLEOfIsStrictlyLE, instIsIsoIntπTruncGEOfIsStrictlyGE, instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, instIsStrictlyGEObjHomologicalComplexIntUpSingle, instIsStrictlyGEObjIntSingleFunctor, instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, instIsStrictlyLEObjHomologicalComplexIntUpSingle, instIsStrictlyLEObjIntSingleFunctor, instQuasiIsoIntιTruncLEOfIsLE, instQuasiIsoIntπTruncGEOfIsGE, isGE_iff, isGE_of_ge, isGE_of_iso, isGE_shift, isIso_ιTruncLE_iff, isIso_πTruncGE_iff, isLE_iff, isLE_of_iso, isLE_of_le, isLE_shift, isStrictlyGE_iff, isStrictlyGE_of_ge, isStrictlyGE_of_iso, isStrictlyGE_shift, isStrictlyLE_iff, isStrictlyLE_of_iso, isStrictlyLE_of_le, isStrictlyLE_shift, isZero_of_isGE, isZero_of_isLE, isZero_of_isStrictlyGE, isZero_of_isStrictlyLE, quasiIso_truncGEMap_iff, quasiIso_truncLEMap_iff, quasiIso_ιTruncLE_iff, quasiIso_πTruncGE_iff, shortComplexTruncLE_shortExact, ιTruncLE_naturality, ιTruncLE_naturality_assoc, πTruncGE_naturality, πTruncGE_naturality_assoc	46
Total	59

CochainComplex

Definitions

Name	Category	Theorems
IsGE 📖	MathDef	7 math math: CategoryTheory.ProjectiveResolution.instIsGECochainComplexOfNatInt, isGE_of_iso, isGE_of_ge, DerivedCategory.isGE_Q_obj_iff, quasiIso_πTruncGE_iff, isGE_iff, isGE_shift
IsLE 📖	MathDef	7 math math: CategoryTheory.InjectiveResolution.instIsLECochainComplexOfNatInt, DerivedCategory.isLE_Q_obj_iff, isLE_iff, isLE_of_iso, isLE_of_le, quasiIso_ιTruncLE_iff, isLE_shift
IsStrictlyGE 📖	MathDef	12 math math: isStrictlyGE_shift, isStrictlyGE_of_ge, instIsStrictlyGEObjHomologicalComplexIntUpSingle, isStrictlyGE_iff, isIso_πTruncGE_iff, isStrictlyGE_of_iso, cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, cm5b.instIsStrictlyGEI, instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt_1, CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt, instIsStrictlyGEObjIntSingleFunctor
IsStrictlyLE 📖	MathDef	9 math math: isStrictlyLE_iff, instIsStrictlyLEObjHomologicalComplexIntUpSingle, instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, isStrictlyLE_of_le, isStrictlyLE_of_iso, CategoryTheory.ProjectiveResolution.instIsStrictlyLECochainComplexOfNatInt, isStrictlyLE_shift, isIso_ιTruncLE_iff, instIsStrictlyLEObjIntSingleFunctor
shortComplexTruncLE 📖	CompOp	3 math math: g_shortComplexTruncLEX₃ToTruncGE, shortComplexTruncLE_shortExact, g_shortComplexTruncLEX₃ToTruncGE_assoc
shortComplexTruncLEX₃ToTruncGE 📖	CompOp	2 math math: g_shortComplexTruncLEX₃ToTruncGE, g_shortComplexTruncLEX₃ToTruncGE_assoc
truncGE 📖	CompOp	9 math math: instIsIsoIntπTruncGEOfIsStrictlyGE, πTruncGE_naturality, g_shortComplexTruncLEX₃ToTruncGE, isIso_πTruncGE_iff, quasiIso_truncGEMap_iff, quasiIso_πTruncGE_iff, g_shortComplexTruncLEX₃ToTruncGE_assoc, πTruncGE_naturality_assoc, instQuasiIsoIntπTruncGEOfIsGE
truncGEMap 📖	CompOp	3 math math: πTruncGE_naturality, quasiIso_truncGEMap_iff, πTruncGE_naturality_assoc
truncLE 📖	CompOp	7 math math: quasiIso_truncLEMap_iff, ιTruncLE_naturality_assoc, instQuasiIsoIntιTruncLEOfIsLE, instIsIsoIntιTruncLEOfIsStrictlyLE, quasiIso_ιTruncLE_iff, ιTruncLE_naturality, isIso_ιTruncLE_iff
truncLEMap 📖	CompOp	3 math math: quasiIso_truncLEMap_iff, ιTruncLE_naturality_assoc, ιTruncLE_naturality
ιTruncLE 📖	CompOp	6 math math: ιTruncLE_naturality_assoc, instQuasiIsoIntιTruncLEOfIsLE, instIsIsoIntιTruncLEOfIsStrictlyLE, quasiIso_ιTruncLE_iff, ιTruncLE_naturality, isIso_ιTruncLE_iff
πTruncGE 📖	CompOp	8 math math: instIsIsoIntπTruncGEOfIsStrictlyGE, πTruncGE_naturality, g_shortComplexTruncLEX₃ToTruncGE, isIso_πTruncGE_iff, quasiIso_πTruncGE_iff, g_shortComplexTruncLEX₃ToTruncGE_assoc, πTruncGE_naturality_assoc, instQuasiIsoIntπTruncGEOfIsGE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exactAt_of_isGE 📖	mathematical	—	HomologicalComplex.ExactAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	HomologicalComplex.exactAt_of_isSupported AddRightCancelSemigroup.toIsRightCancelAdd
exactAt_of_isLE 📖	mathematical	—	HomologicalComplex.ExactAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	HomologicalComplex.exactAt_of_isSupported AddRightCancelSemigroup.toIsRightCancelAdd
exists_iso_single 📖	mathematical	—	CategoryTheory.Iso CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.single	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.IsZero.eq_of_src isZero_of_isStrictlyGE CategoryTheory.Limits.IsZero.eq_of_tgt isZero_of_isStrictlyLE HomologicalComplex.hom_ext lt_trichotomy HomologicalComplex.mkHomToSingle_f CategoryTheory.Category.id_comp HomologicalComplex.mkHomFromSingle_f CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id HomologicalComplex.from_single_hom_ext CategoryTheory.Iso.hom_inv_id
g_shortComplexTruncLEX₃ToTruncGE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.X₂ HomologicalComplex.instHasZeroMorphisms shortComplexTruncLE CategoryTheory.ShortComplex.X₃ truncGE CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc CategoryTheory.ShortComplex.g shortComplexTruncLEX₃ToTruncGE πTruncGE	—	HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE ComplexShape.Embedding.embeddingUpInt_areComplementary
g_shortComplexTruncLEX₃ToTruncGE_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.ShortComplex.X₂ HomologicalComplex.instHasZeroMorphisms shortComplexTruncLE CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g truncGE CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.sc shortComplexTruncLEX₃ToTruncGE πTruncGE	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' g_shortComplexTruncLEX₃ToTruncGE
instIsIsoIntιTruncLEOfIsStrictlyLE 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.IsIso CochainComplex HomologicalComplex.instCategory truncLE ιTruncLE	—	AddRightCancelSemigroup.toIsRightCancelAdd ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE HomologicalComplex.instIsIsoιTruncLEOfIsStrictlySupported
instIsIsoIntπTruncGEOfIsStrictlyGE 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.IsIso CochainComplex HomologicalComplex.instCategory truncGE πTruncGE	—	AddRightCancelSemigroup.toIsRightCancelAdd ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE HomologicalComplex.instIsIsoπTruncGEOfIsStrictlySupported
instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat 📖	mathematical	—	IsStrictlyGE HomologicalComplex.extend ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.embeddingUpNat	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isZero_extend_X zero_add
instIsStrictlyGEObjHomologicalComplexIntUpSingle 📖	mathematical	—	IsStrictlyGE CategoryTheory.Functor.obj HomologicalComplex ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.single	—	AddRightCancelSemigroup.toIsRightCancelAdd isStrictlyGE_iff HomologicalComplex.isZero_single_obj_X
instIsStrictlyGEObjIntSingleFunctor 📖	mathematical	—	IsStrictlyGE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsStrictlyGEObjHomologicalComplexIntUpSingle
instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat 📖	mathematical	—	IsStrictlyLE HomologicalComplex.extend ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne ComplexShape.up AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing ComplexShape.embeddingDownNat	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isZero_extend_X zero_sub
instIsStrictlyLEObjHomologicalComplexIntUpSingle 📖	mathematical	—	IsStrictlyLE CategoryTheory.Functor.obj HomologicalComplex ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.single	—	AddRightCancelSemigroup.toIsRightCancelAdd isStrictlyLE_iff HomologicalComplex.isZero_single_obj_X
instIsStrictlyLEObjIntSingleFunctor 📖	mathematical	—	IsStrictlyLE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd instIsStrictlyLEObjHomologicalComplexIntUpSingle
instQuasiIsoIntιTruncLEOfIsLE 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	QuasiIso truncLE ιTruncLE HomologicalComplex.instHasHomologyTruncLE ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ComplexShape.embeddingUpIntLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasHomologyTruncLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE quasiIso_ιTruncLE_iff
instQuasiIsoIntπTruncGEOfIsGE 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	QuasiIso truncGE πTruncGE HomologicalComplex.truncGE.instHasHomology AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ComplexShape.embeddingUpIntGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.truncGE.instHasHomology ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE quasiIso_πTruncGE_iff
isGE_iff 📖	mathematical	—	IsGE HomologicalComplex.ExactAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AddRightCancelSemigroup.toIsRightCancelAdd exactAt_of_isGE ComplexShape.notMem_range_embeddingUpIntGE_iff
isGE_of_ge 📖	mathematical	—	IsGE	—	AddRightCancelSemigroup.toIsRightCancelAdd isGE_iff exactAt_of_isGE
isGE_of_iso 📖	mathematical	—	IsGE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isSupported_of_iso
isGE_shift 📖	mathematical	—	IsGE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd isGE_iff CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.exactAt_iff_isZero_homology CategoryTheory.Limits.IsZero.of_iso isZero_of_isGE
isIso_ιTruncLE_iff 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.IsIso CochainComplex HomologicalComplex.instCategory truncLE ιTruncLE IsStrictlyLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isIso_ιTruncLE_iff ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE
isIso_πTruncGE_iff 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.IsIso CochainComplex HomologicalComplex.instCategory truncGE πTruncGE IsStrictlyGE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isIso_πTruncGE_iff ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE
isLE_iff 📖	mathematical	—	IsLE HomologicalComplex.ExactAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AddRightCancelSemigroup.toIsRightCancelAdd exactAt_of_isLE ComplexShape.notMem_range_embeddingUpIntLE_iff
isLE_of_iso 📖	mathematical	—	IsLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isSupported_of_iso
isLE_of_le 📖	mathematical	—	IsLE	—	AddRightCancelSemigroup.toIsRightCancelAdd isLE_iff exactAt_of_isLE
isLE_shift 📖	mathematical	—	IsLE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd isLE_iff CategoryTheory.CategoryWithHomology.hasHomology HomologicalComplex.exactAt_iff_isZero_homology CategoryTheory.Limits.IsZero.of_iso isZero_of_isLE
isStrictlyGE_iff 📖	mathematical	—	IsStrictlyGE CategoryTheory.Limits.IsZero HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AddRightCancelSemigroup.toIsRightCancelAdd isZero_of_isStrictlyGE ComplexShape.notMem_range_embeddingUpIntGE_iff
isStrictlyGE_of_ge 📖	mathematical	—	IsStrictlyGE	—	AddRightCancelSemigroup.toIsRightCancelAdd isStrictlyGE_iff isZero_of_isStrictlyGE
isStrictlyGE_of_iso 📖	mathematical	—	IsStrictlyGE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isStrictlySupported_of_iso
isStrictlyGE_shift 📖	mathematical	—	IsStrictlyGE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd isStrictlyGE_iff CategoryTheory.Limits.IsZero.of_iso isZero_of_isStrictlyGE
isStrictlyLE_iff 📖	mathematical	—	IsStrictlyLE CategoryTheory.Limits.IsZero HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AddRightCancelSemigroup.toIsRightCancelAdd isZero_of_isStrictlyLE ComplexShape.notMem_range_embeddingUpIntLE_iff
isStrictlyLE_of_iso 📖	mathematical	—	IsStrictlyLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.isStrictlySupported_of_iso
isStrictlyLE_of_le 📖	mathematical	—	IsStrictlyLE	—	AddRightCancelSemigroup.toIsRightCancelAdd isStrictlyLE_iff isZero_of_isStrictlyLE
isStrictlyLE_shift 📖	mathematical	—	IsStrictlyLE CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Functor.obj CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.shiftFunctor Int.instAddMonoid instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd isStrictlyLE_iff CategoryTheory.Limits.IsZero.of_iso isZero_of_isStrictlyLE
isZero_of_isGE 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex.homology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.ExactAt.isZero_homology exactAt_of_isGE
isZero_of_isLE 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex.homology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.ExactAt.isZero_homology exactAt_of_isLE
isZero_of_isStrictlyGE 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	HomologicalComplex.isZero_X_of_isStrictlySupported AddRightCancelSemigroup.toIsRightCancelAdd
isZero_of_isStrictlyLE 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	—	HomologicalComplex.isZero_X_of_isStrictlySupported AddRightCancelSemigroup.toIsRightCancelAdd
quasiIso_truncGEMap_iff 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	QuasiIso truncGE truncGEMap HomologicalComplex.truncGE.instHasHomology AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ComplexShape.embeddingUpIntGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE QuasiIsoAt	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.truncGE.instHasHomology ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE HomologicalComplex.quasiIso_truncGEMap_iff
quasiIso_truncLEMap_iff 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	QuasiIso truncLE truncLEMap HomologicalComplex.instHasHomologyTruncLE ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ComplexShape.embeddingUpIntLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE QuasiIsoAt	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasHomologyTruncLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE HomologicalComplex.quasiIso_truncLEMap_iff
quasiIso_ιTruncLE_iff 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	QuasiIso truncLE ιTruncLE HomologicalComplex.instHasHomologyTruncLE ComplexShape.down AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ComplexShape.embeddingUpIntLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE IsLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.quasiIso_ιTruncLE_iff_isSupported ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE
quasiIso_πTruncGE_iff 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	QuasiIso truncGE πTruncGE HomologicalComplex.truncGE.instHasHomology AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne ComplexShape.embeddingUpIntGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE IsGE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.quasiIso_πTruncGE_iff_isSupported ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE
shortComplexTruncLE_shortExact 📖	mathematical	—	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasZeroMorphisms shortComplexTruncLE	—	HomologicalComplex.shortComplexTruncLE_shortExact ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE
ιTruncLE_naturality 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory truncLE truncLEMap ιTruncLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.ιTruncLE_naturality ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE
ιTruncLE_naturality_assoc 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory truncLE truncLEMap ιTruncLE	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιTruncLE_naturality
πTruncGE_naturality 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory truncGE πTruncGE truncGEMap	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.πTruncGE_naturality ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE
πTruncGE_naturality_assoc 📖	mathematical	HomologicalComplex.HasHomology ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory truncGE πTruncGE truncGEMap	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πTruncGE_naturality

(root)

Definitions

Name	Category	Theorems
CochainComplex 📖	CompOp	454 math math: HomotopyCategory.spectralObjectMappingCone_δ'_app, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CochainComplex.acyclic_op, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, CochainComplex.triangleOfDegreewiseSplit_obj₁, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, CochainComplex.HomComplex.Cochain.fromSingleMk_neg, CochainComplex.mappingCone.δ_inl, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, DerivedCategory.right_fac, CochainComplex.HomComplex.Cocycle.fromSingleMk_add, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, CochainComplex.mappingConeCompTriangle_obj₂, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, CochainComplex.isStrictlyGE_shift, CochainComplex.mappingCone.id, CochainComplex.shiftFunctorZero_eq, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CochainComplex.augmentTruncate_inv_f_zero, CochainComplex.HomComplex.Cochain.leftShift_smul, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, CochainComplex.mappingCone.triangle_mor₁, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, CategoryTheory.InjectiveResolution.self_ι, CochainComplex.exactAt_op, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, CochainComplex.instLinearIntFunctorSingleFunctors, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, CochainComplex.HomComplex.Cochain.rightUnshift_neg, CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, CochainComplex.truncate_obj_X, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app, CochainComplex.ConnectData.map_comp_map, groupCohomology.cochainsMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, CochainComplex.mappingConeCompTriangle_mor₃, CochainComplex.HomComplex.Cochain.shift_add, CategoryTheory.InjectiveResolution.of_def, CochainComplex.HomComplex.Cochain.comp_id, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, CochainComplex.HomComplex.Cochain.toSingleMk_neg, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, CochainComplex.cm5b.fac, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CochainComplex.HomComplex.Cochain.toSingleMk_v, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, CochainComplex.HomComplex.Cochain.shift_neg, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, CochainComplex.homotopyUnop_hom_eq, CochainComplex.HomComplex.Cochain.toSingleMk_add, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CochainComplex.fromSingle₀Equiv_apply_coe, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CochainComplex.XIsoOfEq_shift, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, CochainComplex.ιTruncLE_naturality_assoc, CochainComplex.HomComplex.Cochain.rightUnshift_comp, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, CochainComplex.mappingCone.inr_triangleδ, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, CochainComplex.πTruncGE_naturality, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.mappingCone.inr_descShortComplex_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk, CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp, CochainComplex.HomComplex.Cochain.shift_zero, CochainComplex.shiftFunctorZero_inv_app_f, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, CochainComplex.HomComplex.Cochain.leftShift_comp, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, CochainComplex.triangleOfDegreewiseSplit_obj₂, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CategoryTheory.InjectiveResolution.ι_f_succ, CochainComplex.isKInjective_shift_iff, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, CochainComplex.HomComplex.Cochain.leftShift_rightShift, CochainComplex.HomComplex.Cochain.ofHom_neg, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, CochainComplex.HomComplex.Cocycle.toSingleMk_add, DerivedCategory.instLinearCochainComplexIntQ, groupCohomology.cochainsMap_zero, CochainComplex.instAdditiveIntFunctorSingleFunctors, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, CochainComplex.exactAt_succ_single_obj, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, 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.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.isIso_πTruncGE_iff, CochainComplex.HomComplex.Cochain.leftUnshift_v, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, groupCohomology.cochainsMap_comp_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, CochainComplex.HomComplex.Cochain.rightShift_leftShift, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, CochainComplex.HomComplex.Cochain.ofHom_sub, CochainComplex.HomComplex.Cochain.leftUnshift_smul, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CochainComplex.HomComplex.Cochain.shiftLinearMap_apply, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CochainComplex.HomComplex.Cocycle.toSingleMk_coe, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CochainComplex.shiftFunctor_map_f', CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π', CochainComplex.HomComplex.Cochain.rightShift_zero, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CochainComplex.singleFunctor_obj_d, CochainComplex.HomComplex.Cochain.rightUnshift_v, HomotopyCategory.composableArrowsFunctor_obj, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, CochainComplex.shiftFunctorAdd'_inv_app_f', CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, CochainComplex.shiftFunctorAdd'_eq, CochainComplex.shiftFunctorAdd'_inv_app_f, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk, CochainComplex.truncateAugment_inv_f, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, CochainComplex.HomComplex.Cochain.fromSingleMk_zero, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, CochainComplex.mappingConeCompTriangle_mor₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, CochainComplex.HomComplex.Cochain.leftShift_zero, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc, CochainComplex.instLinearIntShiftFunctor, CochainComplex.triangleOfDegreewiseSplit_mor₂, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CochainComplex.HomComplex.Cocycle.fromSingleMk_coe, DerivedCategory.isLE_Q_obj_iff, CochainComplex.cm5b.fac_assoc, CochainComplex.triangleOfDegreewiseSplit_obj₃, CochainComplex.shiftFunctorZero'_hom_app_f, CategoryTheory.InjectiveResolution.self_cocomplex, CochainComplex.mappingCone.triangle_mor₂, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, CochainComplex.HomComplex.Cocycle.leftUnshift_coe, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, CochainComplex.instAdditiveIntShiftFunctor, CochainComplex.shiftFunctor_map_f, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, CochainComplex.instIsKProjectiveObjIntShiftFunctor, CochainComplex.HomComplex.Cochain.rightShift_smul, CochainComplex.homotopyOp_hom_eq, CochainComplex.homOfDegreewiseSplit_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, CochainComplex.shiftFunctorAdd_inv_app_f, DerivedCategory.isGE_Q_obj_iff, CochainComplex.truncate_map_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, CochainComplex.mappingCone.map_id, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app, CochainComplex.mappingConeCompTriangle_obj₃, CategoryTheory.ProjectiveResolution.π'_f_zero, CategoryTheory.InjectiveResolution.desc_commutes, CochainComplex.HomComplex.Cocycle.fromSingleMk_neg, CategoryTheory.InjectiveResolution.desc_commutes_assoc, CochainComplex.exists_iso_single, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, CochainComplex.HomComplex.Cochain.shift_units_smul, CochainComplex.shiftFunctorAdd_eq, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, CochainComplex.cm5b.instQuasiIsoIntP, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.HomComplex.Cochain.δ_toSingleMk, CochainComplex.cm5b.instMonoFIntI, CochainComplex.HomComplex.Cochain.fromSingleMk_precomp, CochainComplex.HomComplex.Cochain.leftUnshift_add, CochainComplex.HomComplex.Cocycle.fromSingleMk_zero, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, CochainComplex.HomComplex.Cochain.rightShift_units_smul, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, CochainComplex.HomComplex.Cochain.rightUnshift_smul, HomotopyCategory.composableArrowsFunctor_map, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, 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, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app, CochainComplex.cm5b.instMonoIntI, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, CochainComplex.HomComplex.Cocycle.toSingleMk_sub, CategoryTheory.InjectiveResolution.extMk_hom, CochainComplex.HomComplex.Cocycle.fromSingleMk_sub, 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.HomComplex.Cochain.leftUnshift_units_smul, CochainComplex.mappingCone.inl_fst, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, CochainComplex.HomComplex.Cocycle.shift_coe, CochainComplex.isStrictlyLE_shift, CochainComplex.instFullIntSingleFunctor, CochainComplex.HomComplex.Cochain.δ_rightShift, DerivedCategory.right_fac_of_isStrictlyLE, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CochainComplex.ConnectData.map_id, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_add, CochainComplex.HomComplex.Cochain.toSingleMk_zero, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, HomotopyCategory.homologyFunctor_shiftMap_assoc, CochainComplex.augmentTruncate_inv_f_succ, CochainComplex.shiftFunctor_obj_X', CochainComplex.HomComplex.Cochain.shift_v, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, CochainComplex.triangleOfDegreewiseSplit_mor₃, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, CochainComplex.HomComplex.Cochain.shiftAddHom_apply, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', CochainComplex.HomComplex.Cochain.δ_leftUnshift, HomotopyCategory.spectralObjectMappingCone_ω₁, CochainComplex.HomComplex.Cocycle.toSingleMk_neg, CategoryTheory.InjectiveResolution.desc_commutes_zero, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, CochainComplex.shiftFunctorAdd'_hom_app_f', 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, CochainComplex.shiftEval_hom_app, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, CochainComplex.cm5b.i_f_comp_assoc, AlgebraicTopology.alternatingCofaceMapComplex_map, CochainComplex.mappingCone.triangleRotateShortComplex_g, CochainComplex.shiftFunctor_obj_d', CochainComplex.instHasMapBifunctorObjIntShiftFunctor, CochainComplex.ιTruncLE_naturality, CochainComplex.HomComplex.Cocycle.equivHom_apply, CochainComplex.mappingCone.inr_descShortComplex, DerivedCategory.instAdditiveCochainComplexIntQ, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, CochainComplex.triangleOfDegreewiseSplit_mor₁, CochainComplex.fromSingle₀Equiv_symm_apply_f_zero, CochainComplex.HomComplex.Cochain.leftShift_units_smul, CochainComplex.shiftFunctorAdd_hom_app_f, CochainComplex.truncateAugment_hom_f, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, CochainComplex.mappingCone.inl_v_descShortComplex_f, CochainComplex.isIso_ιTruncLE_iff, 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π', DerivedCategory.exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, CochainComplex.shiftFunctorAdd'_hom_app_f, CochainComplex.HomComplex.Cochain.ofHom_zero, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, CochainComplex.shiftFunctorComm_hom_app_f, groupCohomology.map_cochainsFunctor_shortExact, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, CochainComplex.HomComplex.Cochain.rightShift_neg, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, HomotopyCategory.quotient_obj_singleFunctors_obj, CategoryTheory.InjectiveResolution.instMonoFNatι, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, DerivedCategory.instEssSurjCochainComplexIntQ, CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, CochainComplex.shiftEval_inv_app, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff, groupCohomology.cochainsFunctor_map, CategoryTheory.InjectiveResolution.exact₀, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, HomotopyCategory.homologyFunctor_shiftMap, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, CochainComplex.isKProjective_shift_iff, CochainComplex.instIsStrictlyLEObjIntSingleFunctor, CochainComplex.mappingCone.triangle_obj₂, CochainComplex.instIsStrictlyGEObjIntSingleFunctor, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, CochainComplex.mappingConeCompTriangle_mor₂, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_zero, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp, CochainComplex.HomComplex.Cocycle.leftShift_coe, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, CochainComplex.single₀_obj_zero, CochainComplex.HomComplex.Cochain.shift_v', CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, DerivedCategory.mem_distTriang_iff, CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex, CochainComplex.HomComplex.Cochain.rightShift_add, CochainComplex.ShiftSequence.shiftIso_inv_app, groupCohomology.cochainsMap_id_comp_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, CochainComplex.isGE_shift, CochainComplex.truncate_obj_d, DerivedCategory.Q_map_eq_of_homotopy, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app, CochainComplex.mappingCone.triangleRotateShortComplex_f, CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp, CochainComplex.HomComplex.Cocycle.rightUnshift_coe, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, CochainComplex.HomComplex.Cochain.δ_leftShift, DerivedCategory.isIso_Q_map_iff_quasiIso, CochainComplex.HomComplex.Cocycle.toSingleMk_precomp, CochainComplex.HomComplex.CohomologyClass.toHom_mk, CochainComplex.πTruncGE_naturality_assoc, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, DerivedCategory.left_fac_of_isStrictlyGE, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, CochainComplex.augmentTruncate_hom_f_zero, CategoryTheory.InjectiveResolution.quasiIso, CochainComplex.HomComplex.Cochain.leftShift_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CochainComplex.HomComplex.Cochain.toSingleMk_sub, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, CochainComplex.HomComplex.Cochain.leftUnshift_neg, CochainComplex.isLE_shift, CochainComplex.mappingCone.triangle_obj₁, CochainComplex.cm5b, groupCohomology.cochainsFunctor_obj, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom', CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, CochainComplex.shiftFunctor_obj_d, CochainComplex.HomComplex.Cochain.toSingleMk_precomp, CochainComplex.HomComplex.Cocycle.rightShift_coe, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, CochainComplex.HomComplex.Cochain.leftUnshift_zero, DerivedCategory.left_fac, CochainComplex.mappingCone.triangle_obj₃, CochainComplex.instFaithfulIntSingleFunctor, CochainComplex.mappingConeCompTriangle_obj₁, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f, CochainComplex.ShiftSequence.shiftIso_hom_app, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, groupCohomology.cochainsMap_id, CochainComplex.mappingCone.map_δ, CochainComplex.HomComplex.Cochain.ofHom_comp

---

← Back to Index