Documentation Verification Report

DegreewiseSplit

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

Statistics

Metric	Count
Definitions `cocycleOfDegreewiseSplit`, `homOfDegreewiseSplit`, `triangleRotateIsoTriangleOfDegreewiseSplit`, `triangleRotateShortComplex`, `triangleRotateShortComplexSplitting`, `trianglehRotateIsoTrianglehOfDegreewiseSplit`, `mappingConeHomOfDegreewiseSplitIso`, `mappingConeHomOfDegreewiseSplitXIso`, `triangleOfDegreewiseSplit`, `triangleOfDegreewiseSplitRotateRotateIso`, `trianglehOfDegreewiseSplit`, `trianglehOfDegreewiseSplitRotateRotateIso`	12
Theorems `homOfDegreewiseSplit_f`, `cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v`, `triangleRotateShortComplexSplitting_r`, `triangleRotateShortComplexSplitting_s`, `triangleRotateShortComplex_X₁`, `triangleRotateShortComplex_X₂`, `triangleRotateShortComplex_X₃`, `triangleRotateShortComplex_f`, `triangleRotateShortComplex_g`, `mappingConeHomOfDegreewiseSplitIso_hom_f`, `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃`, `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc`, `mappingConeHomOfDegreewiseSplitIso_inv_f`, `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv`, `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc`, `triangleOfDegreewiseSplit_mor₁`, `triangleOfDegreewiseSplit_mor₂`, `triangleOfDegreewiseSplit_mor₃`, `triangleOfDegreewiseSplit_obj₁`, `triangleOfDegreewiseSplit_obj₂`, `triangleOfDegreewiseSplit_obj₃`, `distinguished_iff_iso_trianglehOfDegreewiseSplit`	22
Total	34

CochainComplex

Definitions

Name	Category	Theorems
`cocycleOfDegreewiseSplit` 📖	CompOp	2 math math: `homOfDegreewiseSplit_f`, `mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v`
`homOfDegreewiseSplit` 📖	CompOp	8 math math: `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv`, `homOfDegreewiseSplit_f`, `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc`, `triangleOfDegreewiseSplit_mor₃`, `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc`, `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃`, `mappingConeHomOfDegreewiseSplitIso_inv_f`, `mappingConeHomOfDegreewiseSplitIso_hom_f`
`mappingConeHomOfDegreewiseSplitIso` 📖	CompOp	6 math math: `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv`, `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc`, `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc`, `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃`, `mappingConeHomOfDegreewiseSplitIso_inv_f`, `mappingConeHomOfDegreewiseSplitIso_hom_f`
`mappingConeHomOfDegreewiseSplitXIso` 📖	CompOp	2 math math: `mappingConeHomOfDegreewiseSplitIso_inv_f`, `mappingConeHomOfDegreewiseSplitIso_hom_f`
`triangleOfDegreewiseSplit` 📖	CompOp	6 math math: `triangleOfDegreewiseSplit_obj₁`, `triangleOfDegreewiseSplit_obj₂`, `triangleOfDegreewiseSplit_mor₂`, `triangleOfDegreewiseSplit_obj₃`, `triangleOfDegreewiseSplit_mor₃`, `triangleOfDegreewiseSplit_mor₁`
`triangleOfDegreewiseSplitRotateRotateIso` 📖	CompOp	—
`trianglehOfDegreewiseSplit` 📖	CompOp	1 math math: `HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit`
`trianglehOfDegreewiseSplitRotateRotateIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homOfDegreewiseSplit_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `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.ShortComplex.X₃` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₁` `homOfDegreewiseSplit` `HomComplex.Cochain.v` `HomComplex.Cochain` `AddSubgroup` `AddCommGroup.toAddGroup` `HomComplex.instAddCommGroupCochain` `SetLike.instMembership` `AddSubgroup.instSetLike` `HomComplex.cocycle` `cocycleOfDegreewiseSplit`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `HomComplex.Cochain.rightShift_v` `CategoryTheory.Category.comp_id`
`mappingConeHomOfDegreewiseSplitIso_hom_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `mappingCone` `CategoryTheory.ShortComplex.X₃` `CochainComplex` `HomologicalComplex.instCategory` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₁` `homOfDegreewiseSplit` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Iso.hom` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `mappingConeHomOfDegreewiseSplitIso` `mappingConeHomOfDegreewiseSplitXIso`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct`
`mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃` 📖	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.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `mappingCone` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `homOfDegreewiseSplit` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Pretriangulated.Triangle.obj₁` `mappingCone.triangle` `CategoryTheory.Iso.inv` `mappingConeHomOfDegreewiseSplitIso` `CategoryTheory.Pretriangulated.Triangle.mor₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instNegHom` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `HomologicalComplex.hom_ext` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.id_comp` `CategoryTheory.Preadditive.sub_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` `sub_zero`
`mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_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.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `mappingCone` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `homOfDegreewiseSplit` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Iso.inv` `mappingConeHomOfDegreewiseSplitIso` `CategoryTheory.Pretriangulated.Triangle.obj₁` `mappingCone.triangle` `CategoryTheory.Pretriangulated.Triangle.mor₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instNegHom` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.g`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃`
`mappingConeHomOfDegreewiseSplitIso_inv_f` 📖	mathematical	—	`HomologicalComplex.Hom.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `ComplexShape.up` `AddSemigroup.toAdd` `AddRightCancelSemigroup.toAddSemigroup` `AddRightCancelMonoid.toAddRightCancelSemigroup` `AddCancelMonoid.toAddRightCancelMonoid` `AddGroup.toAddCancelMonoid` `Int.instAddGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `CategoryTheory.Functor.obj` `CochainComplex` `HomologicalComplex.instCategory` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms` `mappingCone` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `homOfDegreewiseSplit` `CategoryTheory.Iso.inv` `AddRightCancelSemigroup.toIsRightCancelAdd` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `mappingConeHomOfDegreewiseSplitIso` `mappingConeHomOfDegreewiseSplitXIso`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct`
`shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv` 📖	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.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₁` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.X₂` `mappingCone` `CategoryTheory.ShortComplex.X₃` `homOfDegreewiseSplit` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.f` `CategoryTheory.Iso.inv` `mappingConeHomOfDegreewiseSplitIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instNegHom` `mappingCone.inr`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `HomologicalComplex.hom_ext` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.ShortComplex.Splitting.f_r` `CategoryTheory.Category.id_comp` `CategoryTheory.Preadditive.comp_sub` `HomologicalComplex.comp_f_assoc` `CategoryTheory.ShortComplex.zero` `HomologicalComplex.zero_f` `CategoryTheory.Limits.zero_comp` `zero_sub` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'`
`shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_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.Functor.obj` `CategoryTheory.shiftFunctor` `Int.instAddMonoid` `instHasShiftInt` `CategoryTheory.ShortComplex.X₁` `HomologicalComplex.instHasZeroMorphisms` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.f` `mappingCone` `CategoryTheory.ShortComplex.X₃` `homOfDegreewiseSplit` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `HomologicalComplex.X` `CategoryTheory.Iso.inv` `mappingConeHomOfDegreewiseSplitIso` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `HomologicalComplex.instNegHom` `mappingCone.inr`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval` `instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv`
`triangleOfDegreewiseSplit_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` `triangleOfDegreewiseSplit` `CategoryTheory.ShortComplex.f` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleOfDegreewiseSplit_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` `triangleOfDegreewiseSplit` `CategoryTheory.ShortComplex.g` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleOfDegreewiseSplit_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` `triangleOfDegreewiseSplit` `homOfDegreewiseSplit`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleOfDegreewiseSplit_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` `triangleOfDegreewiseSplit` `CategoryTheory.ShortComplex.X₁` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleOfDegreewiseSplit_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` `triangleOfDegreewiseSplit` `CategoryTheory.ShortComplex.X₂` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleOfDegreewiseSplit_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` `triangleOfDegreewiseSplit` `CategoryTheory.ShortComplex.X₃` `HomologicalComplex.instHasZeroMorphisms`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`

CochainComplex.mappingCone

Definitions

Name	Category	Theorems
`triangleRotateIsoTriangleOfDegreewiseSplit` 📖	CompOp	—
`triangleRotateShortComplex` 📖	CompOp	8 math math: `triangleRotateShortComplex_X₂`, `triangleRotateShortComplex_X₃`, `triangleRotateShortComplex_X₁`, `cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v`, `triangleRotateShortComplexSplitting_r`, `triangleRotateShortComplex_g`, `triangleRotateShortComplexSplitting_s`, `triangleRotateShortComplex_f`
`triangleRotateShortComplexSplitting` 📖	CompOp	3 math math: `cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v`, `triangleRotateShortComplexSplitting_r`, `triangleRotateShortComplexSplitting_s`
`trianglehRotateIsoTrianglehOfDegreewiseSplit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v` 📖	mathematical	—	`CochainComplex.HomComplex.Cochain.v` `CategoryTheory.ShortComplex.X₃` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `CategoryTheory.ShortComplex.X₁` `CochainComplex.HomComplex.Cochain` `AddSubgroup` `AddCommGroup.toAddGroup` `CochainComplex.HomComplex.instAddCommGroupCochain` `SetLike.instMembership` `AddSubgroup.instSetLike` `CochainComplex.HomComplex.cocycle` `CochainComplex.cocycleOfDegreewiseSplit` `triangleRotateShortComplexSplitting` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CategoryTheory.Discrete.as` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `HomologicalComplex.Hom.f`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `CochainComplex.HomComplex.Cochain.v.congr_simp` `CategoryTheory.Preadditive.neg_comp` `CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat` `CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct` `add_zero` `d_snd_v` `CategoryTheory.Preadditive.comp_add` `inl_v_fst_v_assoc` `inl_v_snd_v_assoc` `CategoryTheory.Limits.zero_comp`
`triangleRotateShortComplexSplitting_r` 📖	mathematical	—	`CategoryTheory.ShortComplex.Splitting.r` `CategoryTheory.ShortComplex.map` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `HomologicalComplex.eval` `HomologicalComplex.instPreservesZeroMorphismsEval` `triangleRotateShortComplexSplitting` `CochainComplex.HomComplex.Cochain.v` `CochainComplex.mappingCone` `snd`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleRotateShortComplexSplitting_s` 📖	mathematical	—	`CategoryTheory.ShortComplex.Splitting.s` `CategoryTheory.ShortComplex.map` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `HomologicalComplex.eval` `HomologicalComplex.instPreservesZeroMorphismsEval` `triangleRotateShortComplexSplitting` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `HomologicalComplex.X` `CochainComplex.mappingCone` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CategoryTheory.Preadditive.homGroup` `CochainComplex.HomComplex.Cochain.v` `inl`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `HomologicalComplex.instPreservesZeroMorphismsEval`
`triangleRotateShortComplex_X₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₁` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `CategoryTheory.Pretriangulated.Triangle.obj₁` `CochainComplex.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.rotate` `HomologicalComplex.instPreadditive` `triangle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleRotateShortComplex_X₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₂` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `CategoryTheory.Pretriangulated.Triangle.obj₂` `CochainComplex.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.rotate` `HomologicalComplex.instPreadditive` `triangle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleRotateShortComplex_X₃` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₃` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `CategoryTheory.Pretriangulated.Triangle.obj₃` `CochainComplex.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.rotate` `HomologicalComplex.instPreadditive` `triangle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleRotateShortComplex_f` 📖	mathematical	—	`CategoryTheory.ShortComplex.f` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `CategoryTheory.Pretriangulated.Triangle.mor₁` `CochainComplex.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.rotate` `HomologicalComplex.instPreadditive` `triangle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`
`triangleRotateShortComplex_g` 📖	mathematical	—	`CategoryTheory.ShortComplex.g` `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` `HomologicalComplex.instHasZeroMorphisms` `triangleRotateShortComplex` `CategoryTheory.Pretriangulated.Triangle.mor₂` `CochainComplex.instHasShiftInt` `CategoryTheory.Pretriangulated.Triangle.rotate` `HomologicalComplex.instPreadditive` `triangle`	—	`AddRightCancelSemigroup.toIsRightCancelAdd`

HomotopyCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`distinguished_iff_iso_trianglehOfDegreewiseSplit` 📖	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` `CategoryTheory.Iso` `CategoryTheory.Pretriangulated.triangleCategory` `CochainComplex.trianglehOfDegreewiseSplit`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `instHasZeroObject` `instAdditiveIntUpShiftFunctor` `HomologicalComplex.instPreservesZeroMorphismsEval` `CategoryTheory.Pretriangulated.inv_rot_of_distTriang` `CategoryTheory.Pretriangulated.rotate_distinguished_triangle` `CategoryTheory.Pretriangulated.isomorphic_distinguished`

---

← Back to Index