Theorems · Definition · category theory
CategoryTheory.Pretriangulated.Triangle.mk
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.HasShift C ℤ] →
{X Y Z : C} →
(X ⟶ Y) → (Y ⟶ Z) → (Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X) → CategoryTheory.Pretriangulated.Triangle CA triangle (X,Y,Z,f,g,h) in C is defined by the morphisms f : X ⟶ Y, g : Y ⟶ Z
and h : Z ⟶ X⟦1⟧.
- Cited by
- 183 results in Mathlib
- Foundations
- Depth 33 from the axioms, rests on 308 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- CategoryTheory.shiftFunctorstatement and proof · cited by 1,553
- CategoryTheory.HasShiftstatement and proof · cited by 1,527
- CategoryTheory.Pretriangulated.Trianglestatement · cited by 645
Cited by256
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.mapTriangleproof · cited by 87
- CochainComplex.mappingCone.triangleproof · cited by 48
- CategoryTheory.Pretriangulated.Triangle.rotateproof · cited by 43
- CategoryTheory.Pretriangulated.Triangle.invRotateproof · cited by 38
- CategoryTheory.Triangulated.Octahedronstatement · cited by 34
- CategoryTheory.ObjectProperty.trWproof · cited by 32
- CategoryTheory.Pretriangulated.Triangle.shiftFunctorproof · cited by 31
- CategoryTheory.Pretriangulated.contractibleTriangleproof · cited by 27
- CategoryTheory.ShortComplex.ShortExact.singleTriangleproof · cited by 26
- CategoryTheory.Triangulated.Octahedron'statement · cited by 25
- CategoryTheory.ObjectProperty.extensionProductproof · cited by 24
- CochainComplex.mappingConeCompTriangleproof · cited by 20
Showing the 200 most cited of 256.