SingleTriangle

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean

Statistics

Metric	Count
Definitions singleTriangle, map, singleTriangleIso, singleδ	4
Theorems map_hom₁, map_hom₂, map_hom₃, singleTriangleIso_hom_hom₁, singleTriangleIso_hom_hom₂, singleTriangleIso_hom_hom₃, singleTriangleIso_inv_hom₁, singleTriangleIso_inv_hom₂, singleTriangleIso_inv_hom₃, singleTriangle_distinguished, singleTriangle_mor₁, singleTriangle_mor₂, singleTriangle_mor₃, singleTriangle_obj₁, singleTriangle_obj₂, singleTriangle_obj₃	16
Total	20

CategoryTheory.ShortComplex.ShortExact

Definitions

Name	Category	Theorems
singleTriangle 📖	CompOp	18 math math: CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, singleTriangleIso_hom_hom₁, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, singleTriangle.map_hom₁, singleTriangleIso_inv_hom₂, singleTriangle.map_hom₂, singleTriangleIso_inv_hom₃, singleTriangle_obj₂, singleTriangle_mor₃, singleTriangle_mor₁, singleTriangle_mor₂, singleTriangleIso_hom_hom₃, singleTriangleIso_inv_hom₁, singleTriangle_obj₁, singleTriangle_obj₃, singleTriangleIso_hom_hom₂, singleTriangle_distinguished, singleTriangle.map_hom₃
singleTriangleIso 📖	CompOp	6 math math: singleTriangleIso_hom_hom₁, singleTriangleIso_inv_hom₂, singleTriangleIso_inv_hom₃, singleTriangleIso_hom_hom₃, singleTriangleIso_inv_hom₁, singleTriangleIso_hom_hom₂
singleδ 📖	CompOp	2 math math: extClass_hom, singleTriangle_mor₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
singleTriangleIso_hom_hom₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.single CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.SingleFunctors.functor Int.instAddMonoid DerivedCategory.singleFunctors CategoryTheory.Functor.comp CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex.instHasShiftInt CochainComplex.singleFunctors DerivedCategory.Q CategoryTheory.SingleFunctors.Hom.hom CategoryTheory.SingleFunctors.postcomp DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory DerivedCategory.singleFunctorsPostcompQIso CategoryTheory.ShortComplex.X₁	—	CategoryTheory.Abelian.hasZeroObject 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle
singleTriangleIso_hom_hom₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.single CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.SingleFunctors.functor Int.instAddMonoid DerivedCategory.singleFunctors CategoryTheory.Functor.comp CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex.instHasShiftInt CochainComplex.singleFunctors DerivedCategory.Q CategoryTheory.SingleFunctors.Hom.hom CategoryTheory.SingleFunctors.postcomp DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory DerivedCategory.singleFunctorsPostcompQIso CategoryTheory.ShortComplex.X₂	—	CategoryTheory.Abelian.hasZeroObject 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle
singleTriangleIso_hom_hom₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.single CategoryTheory.Abelian.hasZeroObject CategoryTheory.Iso.hom CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.SingleFunctors.functor Int.instAddMonoid DerivedCategory.singleFunctors CategoryTheory.Functor.comp CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CochainComplex.instHasShiftInt CochainComplex.singleFunctors DerivedCategory.Q CategoryTheory.SingleFunctors.Hom.hom CategoryTheory.SingleFunctors.postcomp DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory DerivedCategory.singleFunctorsPostcompQIso CategoryTheory.ShortComplex.X₃	—	CategoryTheory.Abelian.hasZeroObject 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle
singleTriangleIso_inv_hom₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.single CategoryTheory.Abelian.hasZeroObject singleTriangle CategoryTheory.Iso.inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.SingleFunctors.functor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.singleFunctors DerivedCategory.Q DerivedCategory.singleFunctors CategoryTheory.SingleFunctors.Hom.hom CategoryTheory.SingleFunctors.postcomp DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory DerivedCategory.singleFunctorsPostcompQIso CategoryTheory.ShortComplex.X₁	—	CategoryTheory.Abelian.hasZeroObject 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle
singleTriangleIso_inv_hom₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.single CategoryTheory.Abelian.hasZeroObject singleTriangle CategoryTheory.Iso.inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.SingleFunctors.functor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.singleFunctors DerivedCategory.Q DerivedCategory.singleFunctors CategoryTheory.SingleFunctors.Hom.hom CategoryTheory.SingleFunctors.postcomp DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory DerivedCategory.singleFunctorsPostcompQIso CategoryTheory.ShortComplex.X₂	—	CategoryTheory.Abelian.hasZeroObject 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle
singleTriangleIso_inv_hom₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.instHasZeroMorphisms HomologicalComplex.single CategoryTheory.Abelian.hasZeroObject singleTriangle CategoryTheory.Iso.inv CategoryTheory.Pretriangulated.Triangle CategoryTheory.Pretriangulated.triangleCategory 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CochainComplex AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.SingleFunctors.functor Int.instAddMonoid CochainComplex.instHasShiftInt CochainComplex.singleFunctors DerivedCategory.Q DerivedCategory.singleFunctors CategoryTheory.SingleFunctors.Hom.hom CategoryTheory.SingleFunctors.postcomp DerivedCategory.instCommShiftCochainComplexIntQ CategoryTheory.SingleFunctors CategoryTheory.SingleFunctors.instCategory DerivedCategory.singleFunctorsPostcompQIso CategoryTheory.ShortComplex.X₃	—	CategoryTheory.Abelian.hasZeroObject 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 HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle
singleTriangle_distinguished 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles DerivedCategory.instHasZeroObject DerivedCategory.instPreadditive DerivedCategory.instAdditiveShiftFunctorInt DerivedCategory.instPretriangulated singleTriangle	—	CategoryTheory.Pretriangulated.isomorphic_distinguished DerivedCategory.instHasZeroObject DerivedCategory.instAdditiveShiftFunctorInt 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.Abelian.hasZeroObject HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle DerivedCategory.triangleOfSES_distinguished
singleTriangle_mor₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.mor₁ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	—
singleTriangle_mor₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.mor₂ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
singleTriangle_mor₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.mor₃ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle singleδ	—	—
singleTriangle_obj₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.obj₁ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	—
singleTriangle_obj₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.obj₂ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	—
singleTriangle_obj₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.obj₃ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	—

CategoryTheory.ShortComplex.ShortExact.singleTriangle

Definitions

Name	Category	Theorems
map 📖	CompOp	3 math math: map_hom₁, map_hom₂, map_hom₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_hom₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₁ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt CategoryTheory.ShortComplex.ShortExact.singleTriangle map CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.Hom.τ₁	—	—
map_hom₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₂ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt CategoryTheory.ShortComplex.ShortExact.singleTriangle map CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.Hom.τ₂	—	—
map_hom₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.TriangleMorphism.hom₃ DerivedCategory instCategoryDerivedCategory DerivedCategory.instHasShiftInt CategoryTheory.ShortComplex.ShortExact.singleTriangle map CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.Hom.τ₃	—	—

---

← Back to Index