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	13 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_descShortComplex, 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	36 math math: triangle_mor₁, CochainComplex.mappingConeCompTriangle_mor₃, rotateHomotopyEquiv_comm₂_assoc, inl_v_triangle_mor₃_f, inr_triangleδ, DerivedCategory.mappingCone_triangle_distinguished, 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 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	—	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	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 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 HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory	—	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 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 CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd 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 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 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 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 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 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 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 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 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 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 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 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
trianglehMapOfHomotopy_hom₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ HomotopyCategory 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 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 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
trianglehMapOfHomotopy_hom₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ HomotopyCategory 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 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 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

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 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 instCategoryHomotopyCategory hasShift CategoryTheory.Functor.mapHomotopyCategory instCommShiftIntUpMapHomotopyCategory instHasZeroObject instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp	—	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 instHasZeroObject instAdditiveIntUpShiftFunctor CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mappingCone_triangleh_distinguished 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 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	7 math math: distinguished_cocone_triangle, contractible_distinguished, rotate_distinguished_triangle', rotate_distinguished_triangle, invRotate_distinguished_triangle', isomorphic_distinguished, shift_distinguished_triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete_distinguished_triangle_morphism 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 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₁	Quiver.Hom HomotopyCategory 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 CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryHomotopyCategory CategoryTheory.Pretriangulated.Triangle.obj₃ HomotopyCategory.hasShift CategoryTheory.CategoryStruct.comp CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.map	—	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 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 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Pretriangulated.contractibleTriangle HomotopyCategory.instHasZeroObject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomotopyCategory.instPreadditive	—	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 HomotopyCategory.instHasZeroObject AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct HomotopyCategory.isZero_quotient_obj_iff CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.HasZeroObject.from_zero_ext
distinguished_cocone_triangle 📖	mathematical	—	HomotopyCategory 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 Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryHomotopyCategory CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid HomotopyCategory.hasShift CategoryTheory.Pretriangulated.Triangle Set Set.instMembership distinguishedTriangles	—	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 CategoryTheory.Functor.map_surjective HomotopyCategory.instFullHomologicalComplexQuotient
invRotate_distinguished_triangle' 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.invRotate HomotopyCategory.instPreadditive	—	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 isomorphic_distinguished shift_distinguished_triangle rotate_distinguished_triangle' HomotopyCategory.instAdditiveIntUpShiftFunctor
isomorphic_distinguished 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	—	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
rotate_distinguished_triangle 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.rotate HomotopyCategory.instPreadditive	—	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 rotate_distinguished_triangle' isomorphic_distinguished invRotate_distinguished_triangle' HomotopyCategory.instAdditiveIntUpShiftFunctor
rotate_distinguished_triangle' 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.rotate HomotopyCategory.instPreadditive	—	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 CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct AddRightCancelSemigroup.toIsRightCancelAdd
shift_distinguished_triangle 📖	mathematical	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles	CategoryTheory.Pretriangulated.Triangle HomotopyCategory 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 instCategoryHomotopyCategory HomotopyCategory.hasShift Set Set.instMembership distinguishedTriangles CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Pretriangulated.Triangle.shiftFunctor HomotopyCategory.instPreadditive	—	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

---

← Back to Index