Documentation Verification Report

Triangulated

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

Statistics

Metric	Count
Definitions `hom`, `homotopyInvHomId`, `inv`, `mappingConeCompHomotopyEquiv`, `mappingConeCompTriangle`, `mappingConeCompTriangleh`	6
Theorems `hom_inv_id`, `hom_inv_id_assoc`, `mappingConeCompHomotopyEquiv_comm₁`, `mappingConeCompHomotopyEquiv_comm₁_assoc`, `mappingConeCompHomotopyEquiv_comm₂`, `mappingConeCompHomotopyEquiv_comm₂_assoc`, `mappingConeCompHomotopyEquiv_hom_inv_id`, `mappingConeCompHomotopyEquiv_hom_inv_id_assoc`, `mappingConeCompTriangle_mor₁`, `mappingConeCompTriangle_mor₂`, `mappingConeCompTriangle_mor₃`, `mappingConeCompTriangle_mor₃_naturality`, `mappingConeCompTriangle_mor₃_naturality_assoc`, `mappingConeCompTriangle_obj₁`, `mappingConeCompTriangle_obj₂`, `mappingConeCompTriangle_obj₃`, `mappingConeCompTriangleh_comm₁`, `mappingConeCompTriangleh_comm₁_assoc`, `instIsTriangulatedIntUp`, `mappingConeCompTriangleh_distinguished`	20
Total	26

CochainComplex

Definitions

Name	Category	Theorems
`mappingConeCompHomotopyEquiv` 📖	CompOp	8 math math: `mappingConeCompTriangleh_comm₁_assoc`, `mappingConeCompHomotopyEquiv_comm₂_assoc`, `mappingConeCompHomotopyEquiv_hom_inv_id`, `mappingConeCompHomotopyEquiv_comm₁`, `mappingConeCompHomotopyEquiv_comm₁_assoc`, `mappingConeCompHomotopyEquiv_comm₂`, `mappingConeCompTriangleh_comm₁`, `mappingConeCompHomotopyEquiv_hom_inv_id_assoc`
`mappingConeCompTriangle` 📖	CompOp	19 math math: `HomotopyCategory.spectralObjectMappingCone_δ'_app`, `mappingConeCompTriangleh_comm₁_assoc`, `mappingConeCompTriangle_obj₂`, `mappingConeCompTriangle_mor₃`, `mappingConeCompHomotopyEquiv_comm₂_assoc`, `mappingConeCompHomotopyEquiv_hom_inv_id`, `MappingConeCompHomotopyEquiv.hom_inv_id_assoc`, `mappingConeCompHomotopyEquiv_comm₁`, `mappingConeCompHomotopyEquiv_comm₁_assoc`, `mappingConeCompTriangle_mor₃_naturality`, `mappingConeCompTriangle_mor₁`, `MappingConeCompHomotopyEquiv.hom_inv_id`, `mappingConeCompTriangle_obj₃`, `mappingConeCompHomotopyEquiv_comm₂`, `mappingConeCompTriangle_mor₃_naturality_assoc`, `mappingConeCompTriangle_mor₂`, `mappingConeCompTriangleh_comm₁`, `mappingConeCompHomotopyEquiv_hom_inv_id_assoc`, `mappingConeCompTriangle_obj₁`
`mappingConeCompTriangleh` 📖	CompOp	3 math math: `mappingConeCompTriangleh_comm₁_assoc`, `mappingConeCompTriangleh_comm₁`, `HomotopyCategory.mappingConeCompTriangleh_distinguished`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mappingConeCompHomotopyEquiv_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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `mappingCone.map` `CategoryTheory.CategoryStruct.id` `mappingCone.inr` `HomotopyEquiv.inv` `CategoryTheory.Pretriangulated.Triangle.obj₁` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `mappingConeCompHomotopyEquiv` `CategoryTheory.Pretriangulated.Triangle.mor₂`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.id_comp` `mappingCone.inr_desc` `mappingCone.desc.congr_simp`
`mappingConeCompHomotopyEquiv_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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `mappingCone.map` `CategoryTheory.CategoryStruct.id` `mappingCone.inr` `HomotopyEquiv.inv` `CategoryTheory.Pretriangulated.Triangle.obj₁` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `mappingConeCompHomotopyEquiv` `CategoryTheory.Pretriangulated.Triangle.mor₂`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mappingConeCompHomotopyEquiv_comm₁`
`mappingConeCompHomotopyEquiv_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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `mappingCone.triangle` `HomotopyEquiv.hom` `mappingConeCompHomotopyEquiv` `CategoryTheory.Pretriangulated.Triangle.mor₃`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.hom_ext` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `add_zero` `mappingCone.lift_f` `CategoryTheory.Preadditive.add_comp` `CategoryTheory.Category.assoc` `mappingCone.inl_v_triangle_mor₃_f` `CategoryTheory.Preadditive.comp_neg` `CategoryTheory.Category.comp_id` `mappingCone.inr_f_triangle_mor₃_f` `CategoryTheory.Limits.comp_zero` `mappingCone.ext_from_iff` `mappingCone.inl_v_descCochain_v` `HomComplex.Cochain.ofHom_v` `mappingCone.inl_v_triangle_mor₃_f_assoc` `CategoryTheory.Preadditive.neg_comp` `CategoryTheory.Category.id_comp` `mappingCone.inr_f_descCochain_v` `neg_zero` `mappingCone.inr_f_triangle_mor₃_f_assoc` `CategoryTheory.Limits.zero_comp`
`mappingConeCompHomotopyEquiv_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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `HomotopyEquiv.hom` `mappingConeCompHomotopyEquiv` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `mappingCone.triangle` `CategoryTheory.Pretriangulated.Triangle.mor₃`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mappingConeCompHomotopyEquiv_comm₂`
`mappingConeCompHomotopyEquiv_hom_inv_id` 📖	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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `HomotopyEquiv.hom` `mappingConeCompHomotopyEquiv` `HomotopyEquiv.inv` `CategoryTheory.CategoryStruct.id`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `MappingConeCompHomotopyEquiv.hom_inv_id`
`mappingConeCompHomotopyEquiv_hom_inv_id_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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `HomotopyEquiv.hom` `mappingConeCompHomotopyEquiv` `HomotopyEquiv.inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `mappingConeCompHomotopyEquiv_hom_inv_id`
`mappingConeCompTriangle_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` `instHasShiftInt` `mappingConeCompTriangle` `mappingCone.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.id`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct`
`mappingConeCompTriangle_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` `instHasShiftInt` `mappingConeCompTriangle` `mappingCone.map` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.id`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct`
`mappingConeCompTriangle_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` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `mappingCone` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `mappingCone.triangle` `CategoryTheory.Functor.map` `mappingCone.inr`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mappingConeCompTriangle_mor₃_naturality` 📖	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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.obj₁` `mappingConeCompTriangle` `mappingCone.map` `CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.ComposableArrows.mk₂` `CategoryTheory.ComposableArrows.naturality'` `CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.map`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.hom_ext` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.ComposableArrows.naturality'` `CategoryTheory.Category.assoc` `mappingCone.inr_f_desc_f` `mappingCone.ext_from_iff` `mappingCone.inl_v_desc_f_assoc` `zero_add` `add_zero` `HomComplex.Cochain.zero_cochain_comp_v` `HomComplex.Cochain.ofHom_v` `mappingCone.inl_v_triangle_mor₃_f_assoc` `CategoryTheory.Preadditive.neg_comp` `CategoryTheory.Category.id_comp` `CategoryTheory.Preadditive.comp_neg` `mappingCone.inr_f_desc_f_assoc` `mappingCone.inr_f_triangle_mor₃_f_assoc` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.comp_zero`
`mappingConeCompTriangle_mor₃_naturality_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` `mappingCone` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `mappingCone.map` `CategoryTheory.NatTrans.app` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `CategoryTheory.ComposableArrows.mk₂` `CategoryTheory.ComposableArrows.naturality'` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.obj₁` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.mor₃` `CategoryTheory.Functor.map`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.ComposableArrows.naturality'` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mappingConeCompTriangle_mor₃_naturality`
`mappingConeCompTriangle_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` `instHasShiftInt` `mappingConeCompTriangle` `mappingCone`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mappingConeCompTriangle_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` `instHasShiftInt` `mappingConeCompTriangle` `mappingCone` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mappingConeCompTriangle_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` `instHasShiftInt` `mappingConeCompTriangle` `mappingCone`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`mappingConeCompTriangleh_comm₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomotopyCategory` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Pretriangulated.Triangle.obj₂` `HomotopyCategory.hasShift` `mappingConeCompTriangleh` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `mappingCone` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.mor₁` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Functor.map` `HomotopyEquiv.hom` `mappingConeCompHomotopyEquiv` `mappingCone.inr`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.cancel_mono` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_inv` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `mappingConeCompHomotopyEquiv_hom_inv_id` `CategoryTheory.Category.comp_id` `mappingConeCompHomotopyEquiv_comm₁` `mappingConeCompTriangle_mor₂`
`mappingConeCompTriangleh_comm₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `HomotopyCategory` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Category.toCategoryStruct` `instCategoryHomotopyCategory` `CategoryTheory.Pretriangulated.Triangle.obj₂` `HomotopyCategory.hasShift` `mappingConeCompTriangleh` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CategoryTheory.Functor.obj` `HomologicalComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `HomologicalComplex.instCategory` `HomotopyCategory.quotient` `mappingCone` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `instHasShiftInt` `mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.mor₁` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Functor.map` `HomotopyEquiv.hom` `mappingConeCompHomotopyEquiv` `mappingCone.inr`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mappingConeCompTriangleh_comm₁`

CochainComplex.MappingConeCompHomotopyEquiv

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	2 math math: `hom_inv_id_assoc`, `hom_inv_id`
`homotopyInvHomId` 📖	CompOp	—
`inv` 📖	CompOp	2 math math: `hom_inv_id_assoc`, `hom_inv_id`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_inv_id` 📖	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.Pretriangulated.Triangle.obj₁` `CochainComplex.instHasShiftInt` `CochainComplex.mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `hom` `inv` `CategoryTheory.CategoryStruct.id`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.hom_ext` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `add_zero` `CochainComplex.mappingCone.lift_desc_f` `CochainComplex.HomComplex.Cochain.zero_cochain_comp_v` `CochainComplex.mappingCone.ext_from_iff` `CategoryTheory.Preadditive.comp_add` `CochainComplex.mappingCone.inl_v_descCochain_v_assoc` `CochainComplex.HomComplex.Cochain.ofHom_v` `CochainComplex.mappingCone.inr_f_snd_v_assoc` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Category.comp_id` `CochainComplex.mappingCone.inr_f_descCochain_v_assoc` `CochainComplex.mappingCone.inr_f_desc_f` `zero_add`
`hom_inv_id_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` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex.instHasShiftInt` `CochainComplex.mappingConeCompTriangle` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CategoryTheory.Pretriangulated.Triangle.mor₁` `hom` `inv`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `hom_inv_id`

HomotopyCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTriangulatedIntUp` 📖	mathematical	—	`CategoryTheory.IsTriangulated` `HomotopyCategory` `ComplexShape.up` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `instCategoryHomotopyCategory` `instPreadditive` `instHasZeroObject` `hasShift` `instAdditiveIntUpShiftFunctor` `instPretriangulatedIntUp`	—	`CategoryTheory.IsTriangulated.mk'` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasZeroObject` `instAdditiveIntUpShiftFunctor` `CategoryTheory.Functor.map_surjective` `instFullHomologicalComplexQuotient` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `mappingCone_triangleh_distinguished` `CategoryTheory.Pretriangulated.TriangleMorphism.comm₂` `CategoryTheory.Pretriangulated.TriangleMorphism.comm₃` `CategoryTheory.Functor.map_id` `CategoryTheory.Pretriangulated.isomorphic_distinguished` `mappingConeCompTriangleh_distinguished` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.map_comp` `CategoryTheory.Functor.commShiftIso_hom_naturality`
`mappingConeCompTriangleh_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.mappingConeCompTriangleh`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CategoryTheory.Category.comp_id` `CategoryTheory.Category.id_comp` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CochainComplex.mappingConeCompTriangleh_comm₁` `CategoryTheory.Functor.map_id` `CategoryTheory.Functor.map_comp_assoc` `CochainComplex.mappingConeCompHomotopyEquiv_comm₂`

---

← Back to Index