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, instQuasiIsoAtIntιTruncLE, instQuasiIsoAtIntπTruncGE, 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, quasiIsoAt_ιTruncLE, quasiIsoAt_πTruncGE, quasiIso_truncGEMap_iff, quasiIso_truncLEMap_iff, quasiIso_ιTruncLE_iff, quasiIso_πTruncGE_iff, shortComplexTruncLE_shortExact, ιTruncLE_naturality, ιTruncLE_naturality_assoc, πTruncGE_naturality, πTruncGE_naturality_assoc	50
Total	63

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	19 math math: isStrictlyGE_shift, isStrictlyGE_of_ge, instIsStrictlyGEObjHomologicalComplexIntUpSingle, isStrictlyGE_iff, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, isIso_πTruncGE_iff, isStrictlyGE_of_iso, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, cm5b.instIsStrictlyGEI, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, DerivedCategory.exists_iso_Q_obj_of_isGE, plus_iff, instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat, CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt_1, CategoryTheory.InjectiveResolution.instIsStrictlyGECochainComplexOfNatInt, instIsStrictlyGEObjIntSingleFunctor, DerivedCategory.left_fac_of_isStrictlyGE, cm5b
IsStrictlyLE 📖	MathDef	14 math math: isStrictlyLE_iff, instIsStrictlyLEObjHomologicalComplexIntUpSingle, instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, isStrictlyLE_of_le, isStrictlyLE_of_iso, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, CategoryTheory.ProjectiveResolution.instIsStrictlyLECochainComplexOfNatInt, isStrictlyLE_shift, DerivedCategory.right_fac_of_isStrictlyLE, isIso_ιTruncLE_iff, DerivedCategory.exists_iso_Q_obj_of_isLE, 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	11 math math: quasiIsoAt_πTruncGE, instQuasiIsoAtIntπTruncGE, 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	9 math math: quasiIso_truncLEMap_iff, ιTruncLE_naturality_assoc, instQuasiIsoAtIntιTruncLE, quasiIsoAt_ιTruncLE, 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	8 math math: ιTruncLE_naturality_assoc, instQuasiIsoAtIntιTruncLE, quasiIsoAt_ιTruncLE, instQuasiIsoIntιTruncLEOfIsLE, instIsIsoIntιTruncLEOfIsStrictlyLE, quasiIso_ιTruncLE_iff, ιTruncLE_naturality, isIso_ιTruncLE_iff
πTruncGE 📖	CompOp	10 math math: quasiIsoAt_πTruncGE, instQuasiIsoAtIntπTruncGE, 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 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 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 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 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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.single	—	instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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	—	—
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 instIsRightCancelAddOfAddRightReflectLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt contravariant_swap_add_of_contravariant_add Preorder.toLE PartialOrder.toPreorder Int.instAddCommSemigroup IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Int.instAddCommMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instLinearOrder Int.instAddLeftMono AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.single	—	instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing contravariant_lt_of_covariant_le Int.instAddLeftMono 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	—	—
instQuasiIsoAtIntιTruncLE 📖	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	QuasiIsoAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing truncLE ιTruncLE HomologicalComplex.instHasHomologyTruncLE ComplexShape.down Nat.instOne ComplexShape.embeddingUpIntLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE	—	AddRightCancelSemigroup.toIsRightCancelAdd quasiIsoAt_ιTruncLE
instQuasiIsoAtIntπTruncGE 📖	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	QuasiIsoAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing truncGE πTruncGE HomologicalComplex.truncGE.instHasHomology Nat.instOne ComplexShape.embeddingUpIntGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE	—	AddRightCancelSemigroup.toIsRightCancelAdd quasiIsoAt_πTruncGE
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 ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing 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 ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing 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 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 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 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 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
quasiIsoAt_ιTruncLE 📖	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	QuasiIsoAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing truncLE ιTruncLE HomologicalComplex.instHasHomologyTruncLE ComplexShape.down Nat.instOne ComplexShape.embeddingUpIntLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instHasHomologyTruncLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE HomologicalComplex.quasiIsoAt_ιTruncLE add_sub_cancel_right
quasiIsoAt_πTruncGE 📖	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	QuasiIsoAt ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing truncGE πTruncGE HomologicalComplex.truncGE.instHasHomology Nat.instOne ComplexShape.embeddingUpIntGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.truncGE.instHasHomology ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE HomologicalComplex.quasiIsoAt_πTruncGE
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 ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing 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 ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing 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 ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing 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 ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing 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 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 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 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 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 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 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 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 truncGE πTruncGE truncGEMap	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πTruncGE_naturality

(root)

Definitions

Name	Category	Theorems
CochainComplex 📖	CompOp	519 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.mappingCone.inr_desc_assoc, 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.homologyMap_homologyδOfTriangle_assoc, CochainComplex.mappingCone.homologySequenceδ_triangleh, 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, CochainComplex.Plus.mono_iff, 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, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj_assoc, DerivedCategory.homologyFunctorFactors_hom_naturality, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, CochainComplex.homotopyUnop_hom_eq, CochainComplex.HomComplex.Cochain.toSingleMk_add, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CochainComplex.mappingCocone.lift_fst, 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, DerivedCategory.shiftMap_homologyFunctor_map_Q_assoc, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc, CochainComplex.πTruncGE_naturality, DerivedCategory.triangleOfSES_mor₁, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.mappingCone.inr_descShortComplex_assoc, DerivedCategory.mappingCone_triangle_distinguished, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, CochainComplex.homologyδOfTriangle_homologyMap_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.mappingCocone.triangle_obj₂, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_X, CochainComplex.homologyδOfTriangle_homologyMap, CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CategoryTheory.InjectiveResolution.ι_f_succ, CochainComplex.isKInjective_shift_iff, CochainComplex.homologyMap_comp_eq_zero_of_distTriang, 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.mappingCocone.triangle_obj₃, CochainComplex.HomComplex.Cochain.leftShift_rightShift, DerivedCategory.instIsIsoMapCochainComplexIntQOfQuasiIso, CochainComplex.HomComplex.Cochain.ofHom_neg, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, CochainComplex.HomComplex.Cocycle.toSingleMk_add, DerivedCategory.triangleOfSES_obj₃, CochainComplex.homologyMap_exact₃_of_distTriang, DerivedCategory.instLinearCochainComplexIntQ, CochainComplex.homologyMap_exact₂_of_distTriang, groupCohomology.cochainsMap_zero, CochainComplex.instAdditiveIntFunctorSingleFunctors, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, CochainComplex.mappingCone.triangleMap_hom₂, 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.homologyMap_exact₁_of_distTriang, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, groupCohomology.cochainsMap_id_comp, CochainComplex.mappingCocone.triangle_mor₁, 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.Plus.instHasFiniteLimits, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CochainComplex.Plus.instHasTwoOutOfThreePropertyQuasiIso, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, groupCohomology.cochainsMap_comp_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, CochainComplex.HomComplex.Cochain.rightShift_leftShift, DerivedCategory.triangleOfSES.map_hom₁, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f, CochainComplex.HomComplex.Cochain.ofHom_sub, CochainComplex.HomComplex.Cochain.leftUnshift_smul, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CochainComplex.instIsClosedUnderIsomorphismsIntPlus, CochainComplex.HomComplex.Cochain.shiftLinearMap_apply, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CochainComplex.HomComplex.Cocycle.toSingleMk_coe, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step, 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.Plus.instIsClosedUnderLimitsOfShapeIntPlusOfFinCategoryOfHasLimitsOfShape, 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, CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f, DerivedCategory.triangleOfSES_obj₁, 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.mappingCocone.triangle_mor₂, 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.mappingCone.inr_desc, 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₁, CochainComplex.mappingCone.quasiIso_descShortComplex, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CochainComplex.mappingCocone.lift_fst_assoc, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.HomComplex.Cochain.δ_toSingleMk, CochainComplex.cm5b.instMonoFIntI, CochainComplex.HomComplex.Cochain.fromSingleMk_precomp, CochainComplex.HomComplex.Cochain.leftUnshift_add, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun, 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, DerivedCategory.triangleOfSES.map_hom₃, CochainComplex.HomComplex.Cochain.rightUnshift_smul, HomotopyCategory.composableArrowsFunctor_map, CochainComplex.mappingCone.map_comp_assoc, 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, CochainComplex.Plus.instHasFiniteColimits, 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, CochainComplex.mappingCone.map_comp, DerivedCategory.homologyFunctorFactorsh_hom_app_quotient_obj, CategoryTheory.InjectiveResolution.extMk_hom, CochainComplex.HomComplex.Cocycle.fromSingleMk_sub, CochainComplex.shortComplexTruncLE_shortExact, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.Plus.instIsClosedUnderColimitsOfShapeIntPlusOfFinCategoryOfHasColimitsOfShape, 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', HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit, CochainComplex.HomComplex.Cochain.shift_v, CochainComplex.shiftFunctorZero_hom_app_f, DerivedCategory.shiftMap_homologyFunctor_map_Q, 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, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, CochainComplex.augmentTruncate_hom_f_succ, CochainComplex.shiftEval_hom_app, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, CochainComplex.Lifting.hasLift, 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.mappingCocone.triangle_obj₁, 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.mappingCone.map_descShortComplex, CochainComplex.toSingle₀Equiv_apply, DerivedCategory.triangleOfSES.map_hom₂, 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, CochainComplex.mappingCone.triangleMap_hom₁, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, CochainComplex.homologyMap_homologyδOfTriangle, DerivedCategory.triangleOfSES_obj₂, 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₁, DerivedCategory.triangleOfSES_mor₂, CochainComplex.homologyMap_comp_eq_zero_of_distTriang_assoc, 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.mappingCone.triangleMap_hom₃, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, CategoryTheory.Functor.mapCochainComplexPlus_obj_obj_d, CochainComplex.mappingConeCompTriangle_mor₂, DerivedCategory.homologyFunctorFactorsh_inv_app_quotient_obj_assoc, 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.homologyFunctorFactorsh_inv_app_quotient_obj, 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, DerivedCategory.mappingCocone_triangle_distinguished, 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, CochainComplex.liftCycles_shift_homologyπ_assoc, CategoryTheory.InjectiveResolution.quasiIso, CochainComplex.HomComplex.Cochain.leftShift_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CochainComplex.homologyFunctorFactors_hom_app_homologyδOfTriangle, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CochainComplex.HomComplex.Cochain.toSingleMk_sub, CochainComplex.Plus.instIsStableUnderShiftIntPlus, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f, CochainComplex.HomComplex.Cochain.leftUnshift_neg, CochainComplex.isLE_shift, CochainComplex.mappingCone.triangle_obj₁, CochainComplex.cm5b, groupCohomology.cochainsFunctor_obj, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom', DerivedCategory.homologyFunctorFactors_hom_naturality_assoc, 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.Plus.instIsStableUnderRetractsQuasiIso, CochainComplex.liftCycles_shift_homologyπ, 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