ShortExact

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

Statistics

Metric	Count
Definitions triangleOfSES, triangleOfSESIso, triangleOfSESδ	3
Theorems triangleOfSES_distinguished, triangleOfSES_mor₁, triangleOfSES_mor₂, triangleOfSES_mor₃, triangleOfSES_obj₁, triangleOfSES_obj₂, triangleOfSES_obj₃	7
Total	10

DerivedCategory

Definitions

Name	Category	Theorems
triangleOfSES 📖	CompOp	13 math math: CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, triangleOfSES_mor₁, triangleOfSES_obj₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, triangleOfSES_obj₁, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, triangleOfSES_mor₃, triangleOfSES_distinguished, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, triangleOfSES_obj₂, triangleOfSES_mor₂
triangleOfSESIso 📖	CompOp	—
triangleOfSESδ 📖	CompOp	1 math math: triangleOfSES_mor₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
triangleOfSES_distinguished 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle DerivedCategory instCategory instHasShiftInt Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles instHasZeroObject instPreadditive instAdditiveShiftFunctorInt instPretriangulated triangleOfSES	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instAdditiveShiftFunctorInt CategoryTheory.Abelian.hasBinaryBiproducts mem_distTriang_iff
triangleOfSES_mor₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle.mor₁ DerivedCategory instCategory instHasShiftInt triangleOfSES CategoryTheory.Functor.map Q CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleOfSES_mor₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle.mor₂ DerivedCategory instCategory instHasShiftInt triangleOfSES CategoryTheory.Functor.map Q CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleOfSES_mor₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle.mor₃ DerivedCategory instCategory instHasShiftInt triangleOfSES triangleOfSESδ	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleOfSES_obj₁ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle.obj₁ DerivedCategory instCategory instHasShiftInt triangleOfSES CategoryTheory.Functor.obj Q CategoryTheory.ShortComplex.X₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleOfSES_obj₂ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle.obj₂ DerivedCategory instCategory instHasShiftInt triangleOfSES CategoryTheory.Functor.obj Q CategoryTheory.ShortComplex.X₂	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangleOfSES_obj₃ 📖	mathematical	CategoryTheory.ShortComplex.ShortExact CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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	CategoryTheory.Pretriangulated.Triangle.obj₃ DerivedCategory instCategory instHasShiftInt triangleOfSES CategoryTheory.Functor.obj Q CategoryTheory.ShortComplex.X₃	—	AddRightCancelSemigroup.toIsRightCancelAdd

---

← Back to Index