SingleTriangle

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

Statistics

Metric	Count
Definitions singleTriangle, singleTriangleIso, singleδ	3
Theorems 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₃	13
Total	16

CategoryTheory.ShortComplex.ShortExact

Definitions

Name	Category	Theorems
singleTriangle 📖	CompOp	15 math math: CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_apply, singleTriangleIso_hom_hom₁, CategoryTheory.Abelian.Ext.preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply, singleTriangleIso_inv_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
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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.SingleFunctors.functor Int.instAddMonoid DerivedCategory.singleFunctors CategoryTheory.Functor.comp CochainComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.SingleFunctors.functor Int.instAddMonoid DerivedCategory.singleFunctors CategoryTheory.Functor.comp CochainComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.SingleFunctors.functor Int.instAddMonoid DerivedCategory.singleFunctors CategoryTheory.Functor.comp CochainComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CochainComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CochainComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt DerivedCategory.triangleOfSES CategoryTheory.ShortComplex.map HomologicalComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup HomologicalComplex.instPreservesZeroMorphismsSingle map_of_exact HomologicalComplex.instPreservesFiniteLimitsSingle HomologicalComplex.instPreservesFiniteColimitsSingle singleTriangleIso CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CochainComplex 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory 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 AddRightCancelSemigroup.toIsRightCancelAdd 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 DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	—
singleTriangle_mor₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.mor₂ DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.map DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
singleTriangle_mor₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.mor₃ DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle singleδ	—	—
singleTriangle_obj₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.obj₁ DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₁	—	—
singleTriangle_obj₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.obj₂ DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₂	—	—
singleTriangle_obj₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	CategoryTheory.Pretriangulated.Triangle.obj₃ DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt singleTriangle CategoryTheory.Functor.obj DerivedCategory.singleFunctor CategoryTheory.ShortComplex.X₃	—	—

---

← Back to Index