Pretriangulated

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

Statistics

Metric	Count
Definitions homotopyToZeroOfId, map, mapOfHomotopy, mapTriangleIso, mapTrianglehIso, rotateHomotopyEquiv, rotateHomotopyEquivComm₂Homotopy, rotateTrianglehIso, shiftIso, shiftTriangleIso, shiftTrianglehIso, triangle, triangleMap, triangleh, trianglehMapOfHomotopy, distinguishedTriangles, instPretriangulatedIntUp	17
Theorems inl_v_triangle_mor₃_f, inl_v_triangle_mor₃_f_assoc, inr_f_triangle_mor₃_f, inr_f_triangle_mor₃_f_assoc, inr_triangleδ, inr_triangleδ_assoc, map_comp, map_comp_assoc, map_eq_mapOfHomotopy, map_id, map_δ, rotateHomotopyEquiv_comm₂, rotateHomotopyEquiv_comm₂_assoc, rotateHomotopyEquiv_comm₃, rotateHomotopyEquiv_comm₃_assoc, triangleMapOfHomotopy_comm₂, triangleMapOfHomotopy_comm₂_assoc, triangleMapOfHomotopy_comm₃, triangleMapOfHomotopy_comm₃_assoc, triangleMap_hom₁, triangleMap_hom₂, triangleMap_hom₃, triangle_mor₁, triangle_mor₂, triangle_obj₁, triangle_obj₂, triangle_obj₃, trianglehMapOfHomotopy_hom₁, trianglehMapOfHomotopy_hom₂, trianglehMapOfHomotopy_hom₃, complete_distinguished_triangle_morphism, contractible_distinguished, distinguished_cocone_triangle, invRotate_distinguished_triangle', isomorphic_distinguished, rotate_distinguished_triangle, rotate_distinguished_triangle', shift_distinguished_triangle, instIsTriangulatedIntUpMapHomotopyCategory, mappingCone_triangleh_distinguished	40
Total	57

CochainComplex.mappingCone

Definitions

Name	Category	Theorems
homotopyToZeroOfId 📖	CompOp	—
map 📖	CompOp	12 math math: CochainComplex.mappingConeCompHomotopyEquiv_comm₁, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CochainComplex.mappingConeCompTriangle_mor₁, map_id, HomotopyCategory.composableArrowsFunctor_map, map_comp_assoc, map_comp, map_eq_mapOfHomotopy, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, triangleMap_hom₃, CochainComplex.mappingConeCompTriangle_mor₂
mapOfHomotopy 📖	CompOp	6 math math: triangleMapOfHomotopy_comm₂, triangleMapOfHomotopy_comm₂_assoc, trianglehMapOfHomotopy_hom₃, triangleMapOfHomotopy_comm₃_assoc, map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₃
mapTriangleIso 📖	CompOp	—
mapTrianglehIso 📖	CompOp	—
rotateHomotopyEquiv 📖	CompOp	4 math math: rotateHomotopyEquiv_comm₂_assoc, rotateHomotopyEquiv_comm₂, rotateHomotopyEquiv_comm₃_assoc, rotateHomotopyEquiv_comm₃
rotateHomotopyEquivComm₂Homotopy 📖	CompOp	—
rotateTrianglehIso 📖	CompOp	—
shiftIso 📖	CompOp	—
shiftTriangleIso 📖	CompOp	—
shiftTrianglehIso 📖	CompOp	—
triangle 📖	CompOp	35 math math: triangle_mor₁, CochainComplex.mappingConeCompTriangle_mor₃, rotateHomotopyEquiv_comm₂_assoc, inl_v_triangle_mor₃_f, inr_triangleδ, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, triangleMap_hom₂, rotateHomotopyEquiv_comm₂, triangleRotateShortComplex_X₂, triangleRotateShortComplex_X₃, triangleRotateShortComplex_X₁, inl_v_triangle_mor₃_f_assoc, inr_triangleδ_assoc, inr_f_triangle_mor₃_f, triangle_mor₂, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, rotateHomotopyEquiv_comm₃_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, trianglehMapOfHomotopy_hom₃, trianglehMapOfHomotopy_hom₁, trianglehMapOfHomotopy_hom₂, triangleMapOfHomotopy_comm₃_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, triangleRotateShortComplex_g, inr_f_triangle_mor₃_f_assoc, triangleMap_hom₁, triangleMapOfHomotopy_comm₃, triangle_obj₂, triangleMap_hom₃, DerivedCategory.mem_distTriang_iff, triangleRotateShortComplex_f, rotateHomotopyEquiv_comm₃, triangle_obj₁, triangle_obj₃, map_δ
triangleMap 📖	CompOp	3 math math: triangleMap_hom₂, triangleMap_hom₁, triangleMap_hom₃
triangleh 📖	CompOp	5 math math: homologySequenceδ_triangleh, HomotopyCategory.mappingCone_triangleh_distinguished, trianglehMapOfHomotopy_hom₃, trianglehMapOfHomotopy_hom₁, trianglehMapOfHomotopy_hom₂
trianglehMapOfHomotopy 📖	CompOp	3 math math: trianglehMapOfHomotopy_hom₃, trianglehMapOfHomotopy_hom₁, trianglehMapOfHomotopy_hom₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inl_v_triangle_mor₃_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CochainComplex.shiftFunctor NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct zero_add add_zero CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.rightShift_neg CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Preadditive.comp_neg inl_v_fst_v_assoc
inl_v_triangle_mor₃_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CochainComplex.HomComplex.Cochain.v inl CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle HomologicalComplex.Hom.f CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CochainComplex.shiftFunctor NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.Iso.inv CochainComplex.shiftFunctorObjXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_triangle_mor₃_f
inr_f_triangle_mor₃_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle HomologicalComplex.Hom.f inr CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.rightShift_neg add_zero CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CategoryTheory.Preadditive.comp_neg inr_f_fst_v neg_zero
inr_f_triangle_mor₃_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.Hom.f inr CategoryTheory.Functor.obj CochainComplex HomologicalComplex.instCategory CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_f_triangle_mor₃_f
inr_triangleδ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle inr CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct inr_f_triangle_mor₃_f
inr_triangleδ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instZeroHom_1	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_triangleδ
map_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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	map CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct zero_add CategoryTheory.Category.assoc CochainComplex.HomComplex.Cochain.ofHom_comp CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain desc.congr_simp ext_from_iff inl_v_desc_f add_zero CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v inl_v_desc_f_assoc inr_f_desc_f inr_f_desc_f_assoc
map_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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	CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X map	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_eq_mapOfHomotopy 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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	map mapOfHomotopy Homotopy.ofEq HomologicalComplex	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CochainComplex.HomComplex.Cochain.zero_comp add_zero desc.congr_simp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.id_comp CochainComplex.HomComplex.Cochain.id_comp desc.congr_simp ext_from_iff inl_v_desc_f CategoryTheory.Category.comp_id inr_f_desc_f
map_δ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex.instHasShiftInt triangle CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.comp CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.CommShift.commShiftIso CategoryTheory.Functor.commShiftMapCochainComplex CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X mapHomologicalComplexIso	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CategoryTheory.Functor.preservesZeroMorphisms_of_additive CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct mapHomologicalComplexXIso_eq mapHomologicalComplexXIso'_hom CategoryTheory.Category.comp_id CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc inl_v_triangle_mor₃_f CategoryTheory.Preadditive.comp_neg inr_f_triangle_mor₃_f CategoryTheory.Limits.comp_zero add_zero CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Functor.map_neg
rotateHomotopyEquiv_comm₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopyCategory 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.Category.toCategoryStruct instCategoryHomotopyCategory CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex CochainComplex.instHasShiftInt triangle CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ HomotopyEquiv.hom rotateHomotopyEquiv	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Functor.map_comp HomotopyCategory.eq_of_homotopy
rotateHomotopyEquiv_comm₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomotopyCategory 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.Category.toCategoryStruct instCategoryHomotopyCategory CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex CochainComplex.instHasShiftInt triangle CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Functor.map CategoryTheory.Pretriangulated.Triangle.mor₃ CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr HomotopyEquiv.hom rotateHomotopyEquiv	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rotateHomotopyEquiv_comm₂
rotateHomotopyEquiv_comm₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr CochainComplex CategoryTheory.Pretriangulated.Triangle.obj₁ triangle HomotopyEquiv.hom rotateHomotopyEquiv CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instNegHom CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct add_zero lift_f zero_add CochainComplex.HomComplex.Cochain.leftShift_v mul_one sub_self MulZeroClass.mul_zero CochainComplex.HomComplex.Cochain.ofHom_v CategoryTheory.Category.id_comp Units.neg_smul one_smul neg_neg CategoryTheory.Preadditive.neg_comp CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc inl_v_triangle_mor₃_f CategoryTheory.Preadditive.comp_neg CategoryTheory.Category.comp_id inr_f_triangle_mor₃_f CategoryTheory.Limits.comp_zero neg_zero
rotateHomotopyEquiv_comm₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr HomotopyEquiv.hom rotateHomotopyEquiv CochainComplex CategoryTheory.Pretriangulated.Triangle.obj₁ triangle CategoryTheory.Pretriangulated.Triangle.mor₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.instNegHom CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rotateHomotopyEquiv_comm₃
triangleMapOfHomotopy_comm₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr mapOfHomotopy	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct inr_desc
triangleMapOfHomotopy_comm₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X inr mapOfHomotopy	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' triangleMapOfHomotopy_comm₂
triangleMapOfHomotopy_comm₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle mapOfHomotopy CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.rightShift_neg CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CategoryTheory.Preadditive.comp_neg CategoryTheory.Preadditive.neg_comp ext_from_iff inl_v_desc_f_assoc zero_add add_zero CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc inl_v_fst_v inr_f_fst_v CategoryTheory.Limits.comp_zero inl_v_fst_v_assoc inr_f_desc_f_assoc neg_zero inr_f_fst_v_assoc CategoryTheory.Limits.zero_comp
triangleMapOfHomotopy_comm₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.mappingCone CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomologicalComplex.X mapOfHomotopy CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.Triangle.obj₁ triangle CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' triangleMapOfHomotopy_comm₃
triangleMap_hom₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Pretriangulated.TriangleMorphism.hom₁ CochainComplex.instHasShiftInt triangle triangleMap	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleMap_hom₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Pretriangulated.TriangleMorphism.hom₂ CochainComplex.instHasShiftInt triangle triangleMap	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleMap_hom₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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.Pretriangulated.TriangleMorphism.hom₃ CochainComplex.instHasShiftInt triangle triangleMap map	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct
triangle_mor₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.mor₁ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_mor₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.mor₂ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.instHasShiftInt triangle inr	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_obj₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.obj₁ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_obj₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.obj₂ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_obj₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms 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 CochainComplex.instHasShiftInt triangle CochainComplex.mappingCone	—	AddRightCancelSemigroup.toIsRightCancelAdd
trianglehMapOfHomotopy_hom₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift triangleh trianglehMapOfHomotopy CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.Pretriangulated.Triangle.obj₁ CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
trianglehMapOfHomotopy_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift triangleh trianglehMapOfHomotopy CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.Pretriangulated.Triangle.obj₂ CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
trianglehMapOfHomotopy_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift triangleh trianglehMapOfHomotopy CategoryTheory.Functor.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex.instHasShiftInt triangle mapOfHomotopy	—	AddRightCancelSemigroup.toIsRightCancelAdd

HomotopyCategory

Definitions

Name	Category	Theorems
instPretriangulatedIntUp 📖	CompOp	12 math math: spectralObjectMappingCone_δ'_app, instIsHomologicalIntUpHomologyFunctor, DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh, mappingCone_triangleh_distinguished, instIsTriangulatedIntUpSubcategoryAcyclic, instIsTriangulatedIntUp, instIsTriangulatedIntUpMapHomotopyCategory, quasiIso_eq_subcategoryAcyclic_W, distinguished_iff_iso_trianglehOfDegreewiseSplit, spectralObjectMappingCone_ω₁, mappingConeCompTriangleh_distinguished, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTriangulatedIntUpMapHomotopyCategory 📖	mathematical	—	CategoryTheory.Functor.IsTriangulated HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory hasShift CategoryTheory.Functor.mapHomotopyCategory instCommShiftIntUpMapHomotopyCategory instHasZeroObject instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instAdditiveIntUpShiftFunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mappingCone_triangleh_distinguished 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory hasShift Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles instHasZeroObject instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp CochainComplex.mappingCone.triangleh	—	AddRightCancelSemigroup.toIsRightCancelAdd

HomotopyCategory.Pretriangulated

Definitions

Name	Category	Theorems
distinguishedTriangles 📖	CompOp	3 math math: distinguished_cocone_triangle, contractible_distinguished, rotate_distinguished_triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete_distinguished_triangle_morphism 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₁	CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient CategoryTheory.Pretriangulated.TriangleMorphism.comm₁ CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ CategoryTheory.Pretriangulated.TriangleMorphism.comm₃ CategoryTheory.Pretriangulated.TriangleMorphism.comm₂_assoc CategoryTheory.Iso.hom_inv_id_triangle_hom₂ CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id_triangle_hom₂_assoc CategoryTheory.Iso.hom_inv_id_triangle_hom₁ CategoryTheory.Iso.hom_inv_id_triangle_hom₁_assoc
contractible_distinguished 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Pretriangulated.contractibleTriangle HomotopyCategory.instHasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory.instPreadditive	—	AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.instHasZeroObject CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomotopyCategory.isZero_quotient_obj_iff CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.HasZeroObject.from_zero_ext
distinguished_cocone_triangle 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient
invRotate_distinguished_triangle' 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.invRotate HomotopyCategory.instPreadditive	—	AddRightCancelSemigroup.toIsRightCancelAdd isomorphic_distinguished shift_distinguished_triangle rotate_distinguished_triangle' HomotopyCategory.instAdditiveIntUpShiftFunctor
isomorphic_distinguished 📖	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	—	—	AddRightCancelSemigroup.toIsRightCancelAdd
rotate_distinguished_triangle 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.rotate HomotopyCategory.instPreadditive	—	AddRightCancelSemigroup.toIsRightCancelAdd rotate_distinguished_triangle' isomorphic_distinguished invRotate_distinguished_triangle' HomotopyCategory.instAdditiveIntUpShiftFunctor
rotate_distinguished_triangle' 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle.rotate HomotopyCategory.instPreadditive	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct
shift_distinguished_triangle 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Triangle.shiftFunctor HomotopyCategory.instPreadditive	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index