Theorems · Definition · category theory
CategoryTheory.Pretriangulated.triangleOpEquivalence
(C : Type u_1) →
[inst : CategoryTheory.Category.{v_1, u_1} C] →
[inst_1 : CategoryTheory.HasShift C ℤ] →
(CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ ≌ CategoryTheory.Pretriangulated.Triangle CᵒᵖAn anti-equivalence between the categories of triangles in C and in Cᵒᵖ.
A triangle in Cᵒᵖ shall be distinguished iff it corresponds to a distinguished
triangle in C via this equivalence.
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Oppositestatement · cited by 8,081
- CategoryTheory.HasShiftstatement and proof · cited by 1,527
- CategoryTheory.Pretriangulated.Trianglestatement · cited by 645
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.Pretriangulated.TriangleOpEquivalence.functorproof · cited by 15
- CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverseproof · cited by 13
- CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIsoproof · cited by 7
- CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIsoproof · cited by 3
Cited by40
Results whose statement or proof uses this declaration.
- CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIsostatement and proof · cited by 7
- CategoryTheory.Pretriangulated.Opposite.distinguishedTrianglesproof · cited by 7
- CategoryTheory.Pretriangulated.op_distinguishedstatement and proof · cited by 6
- CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorAppstatement and proof · cited by 6
- CategoryTheory.Abelian.Ext.contravariant_sequence_exact₁'proof · cited by 4
- CategoryTheory.Abelian.Ext.preadditiveYoneda_homologySequenceδ_singleTriangle_applystatement and proof · cited by 2
- CategoryTheory.Functor.isTriangulated_of_opproof · cited by 2
- CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iffstatement · cited by 2
- CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff'statement and proof · cited by 2
- CategoryTheory.Pretriangulated.unop_distinguishedstatement · cited by 2
- CategoryTheory.Abelian.Ext.contravariant_sequence_exact₂'proof · cited by 2
- CategoryTheory.Abelian.Ext.contravariant_sequence_exact₃'proof · cited by 2