# Documentation

Mathlib.CategoryTheory.Triangulated.Opposite

# The (pre)triangulated structure on the opposite category #

In this file, we shall construct the (pre)triangulated structure on the opposite category Cᵒᵖ of a (pre)triangulated category C.

The shift on Cᵒᵖ is obtained by combining the constructions in the files CategoryTheory.Shift.Opposite and CategoryTheory.Shift.Pullback. When the user opens CategoryTheory.Pretriangulated.Opposite, the category Cᵒᵖ is equipped with the shift by ℤ such that shifting by n : ℤ on Cᵒᵖ corresponds to the shift by -n on C. This is actually a definitional equality, but the user should not rely on this, and instead use the isomorphism shiftFunctorOpIso C n m hnm : shiftFunctor Cᵒᵖ n ≅ (shiftFunctor C m).op where hnm : n + m = 0.

Some compatibilities between the shifts on C and Cᵒᵖ are also expressed through the equivalence of categories opShiftFunctorEquivalence C n : Cᵒᵖ ≌ Cᵒᵖ whose functor is shiftFunctor Cᵒᵖ n and whose inverse functor is (shiftFunctor C n).op.

If X ⟶ Y ⟶ Z ⟶ X⟦1⟧ is a distinguished triangle in C, then the triangle op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧ that is deduced without introducing signs shall be a distinguished triangle in Cᵒᵖ. This is equivalent to the definition in [Verdiers's thesis, p. 96][verdier1996] which would require that the triangle (op X)⟦-1⟧ ⟶ op Z ⟶ op Y ⟶ op X (without signs) is antidistinguished.

## References #

• [Jean-Louis Verdier, Des catégories dérivées des catégories abéliennes][verdier1996]

The category Cᵒᵖ is equipped with the shift such that the shift by n on Cᵒᵖ corresponds to the shift by -n on C.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
noncomputable def CategoryTheory.Pretriangulated.shiftFunctorOpIso (C : Type u_1) [] (n : ) (m : ) (hnm : n + m = 0) :

The shift functor on the opposite category identifies to the opposite functor of a shift functor on the original category.

Equations
Instances For
theorem CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app {C : Type u_1} [] (X : Cᵒᵖ) (a₁ : ) (a₂ : ) (a₃ : ) (h : a₁ + a₂ = a₃) (b₁ : ) (b₂ : ) (b₃ : ) (h₁ : a₁ + b₁ = 0) (h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0) :
().hom.app X = CategoryTheory.CategoryStruct.comp (().hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ (_ : b₁ + b₂ = b₃)).inv.app X.unop).op (CategoryTheory.CategoryStruct.comp (().inv.app { unop := ().toPrefunctor.1 X.unop }) (.map (().inv.app X))))
theorem CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app {C : Type u_1} [] (X : Cᵒᵖ) (a₁ : ) (a₂ : ) (a₃ : ) (h : a₁ + a₂ = a₃) (b₁ : ) (b₂ : ) (b₃ : ) (h₁ : a₁ + b₁ = 0) (h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0) :
().inv.app X = CategoryTheory.CategoryStruct.comp (.map (().hom.app X)) (CategoryTheory.CategoryStruct.comp (().hom.app (().op.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ (_ : b₁ + b₂ = b₃)).hom.app X.unop).op (().inv.app X)))
theorem CategoryTheory.Pretriangulated.shiftFunctor_op_map {C : Type u_1} [] (n : ) (m : ) (hnm : n + m = 0) {K : Cᵒᵖ} {L : Cᵒᵖ} (φ : K L) :
.map φ = CategoryTheory.CategoryStruct.comp (().hom.app K) (CategoryTheory.CategoryStruct.comp (.map φ.unop).op (().inv.app L))
@[simp]

The autoequivalence Cᵒᵖ ≌ Cᵒᵖ whose functor is shiftFunctor Cᵒᵖ n and whose inverse functor is (shiftFunctor C n).op. Do not unfold the definitions of the unit and counit isomorphisms: the compatibilities they satisfy are stated as separate lemmas.

Equations
• One or more equations did not get rendered due to their size.
Instances For

The naturality of the unit and counit isomorphisms are restated in the following lemmas so as to mitigate the need for erw.

@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {Z : Cᵒᵖ} (h : .inverse.obj (.functor.obj Y) Z) :
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
CategoryTheory.CategoryStruct.comp f (.unitIso.hom.app Y) = CategoryTheory.CategoryStruct.comp (.unitIso.hom.app X) (.map (.map f).unop).op
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {Z : Cᵒᵖ} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (.map (.map f).unop).op (CategoryTheory.CategoryStruct.comp (.unitIso.inv.app Y) h) = CategoryTheory.CategoryStruct.comp (.unitIso.inv.app X)
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
CategoryTheory.CategoryStruct.comp (.map (.map f).unop).op (.unitIso.inv.app Y) = CategoryTheory.CategoryStruct.comp (.unitIso.inv.app X) f
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {Z : Cᵒᵖ} (h : Y Z) :
CategoryTheory.CategoryStruct.comp (.map (.map f.unop).op) (CategoryTheory.CategoryStruct.comp (.counitIso.hom.app Y) h) = CategoryTheory.CategoryStruct.comp (.counitIso.hom.app X)
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
CategoryTheory.CategoryStruct.comp (.map (.map f.unop).op) (.counitIso.hom.app Y) = CategoryTheory.CategoryStruct.comp (.counitIso.hom.app X) f
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) {Z : Cᵒᵖ} (h : .functor.obj (.inverse.obj Y) Z) :
@[simp]
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality (C : Type u_1) [] (n : ) {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
CategoryTheory.CategoryStruct.comp f (.counitIso.inv.app Y) = CategoryTheory.CategoryStruct.comp (.counitIso.inv.app X) (.map (.map f.unop).op)
theorem CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app {C : Type u_1} [] (X : Cᵒᵖ) (n : ) :
.map (.counitIso.inv.app X).unop = (.unitIso.hom.app (Opposite.op (.obj X.unop))).unop
theorem CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app {C : Type u_1} [] (X : Cᵒᵖ) (n : ) :
.map (.counitIso.hom.app X).unop = (.unitIso.inv.app (Opposite.op (.obj X.unop))).unop
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift {C : Type u_1} [] (X : Cᵒᵖ) (n : ) :
.counitIso.inv.app (.obj X) = .map (.unitIso.hom.app X)
theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift {C : Type u_1} [] (X : Cᵒᵖ) (n : ) :
.counitIso.hom.app (.obj X) = .map (.unitIso.inv.app X)
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj (C : Type u_1) [] :
= CategoryTheory.Pretriangulated.Triangle.mk T.unop.mor₂.op T.unop.mor₁.op (CategoryTheory.CategoryStruct.comp (.counitIso.inv.app (Opposite.op T.unop.obj₁)) (.map T.unop.mor₃.op))
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂ (C : Type u_1) [] (φ : T₁ T₂) :
.hom₂ = φ.unop.hom₂.op
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃ (C : Type u_1) [] (φ : T₁ T₂) :
.hom₃ = φ.unop.hom₁.op
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁ (C : Type u_1) [] (φ : T₁ T₂) :
.hom₁ = φ.unop.hom₃.op

The functor which sends a triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ in C to the triangle op Z ⟶ op Y ⟶ op X ⟶ (op Z)⟦1⟧ in Cᵒᵖ (without introducing signs).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj (C : Type u_1) [] :
= Opposite.op (CategoryTheory.Pretriangulated.Triangle.mk T.mor₂.unop T.mor₁.unop (CategoryTheory.CategoryStruct.comp (.unitIso.inv.app T.obj₁).unop (.map T.mor₃.unop)))
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map (C : Type u_1) [] (φ : T₁ T₂) :
= (CategoryTheory.Pretriangulated.TriangleMorphism.mk φ.hom₃.unop φ.hom₂.unop φ.hom₁.unop).op

The functor which sends a triangle X ⟶ Y ⟶ Z ⟶ X⟦1⟧ in Cᵒᵖ to the triangle Z.unop ⟶ Y.unop ⟶ X.unop ⟶ Z.unop⟦1⟧ in C (without introducing signs).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app (C : Type u_1) [] :
= (CategoryTheory.Pretriangulated.Triangle.homMk (CategoryTheory.Pretriangulated.Triangle.mk X.unop.mor₁ X.unop.mor₂ (CategoryTheory.CategoryStruct.comp (.unitIso.inv.app (Opposite.op X.unop.obj₃)).unop (.map (CategoryTheory.CategoryStruct.comp (.map X.unop.mor₃.op).unop (.counitIso.inv.app (Opposite.op X.unop.obj₁)).unop)))) X.unop (CategoryTheory.CategoryStruct.id X.unop.obj₁) (CategoryTheory.CategoryStruct.id X.unop.obj₂) (CategoryTheory.CategoryStruct.id X.unop.obj₃)).op
@[simp]
theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app (C : Type u_1) [] :
= (CategoryTheory.Pretriangulated.Triangle.homMk X.unop (CategoryTheory.Pretriangulated.Triangle.mk X.unop.mor₁ X.unop.mor₂ (CategoryTheory.CategoryStruct.comp (.unitIso.inv.app (Opposite.op X.unop.obj₃)).unop (.map (CategoryTheory.CategoryStruct.comp (.map X.unop.mor₃.op).unop (.counitIso.inv.app (Opposite.op X.unop.obj₁)).unop)))) (CategoryTheory.CategoryStruct.id X.unop.obj₁) (CategoryTheory.CategoryStruct.id X.unop.obj₂) (CategoryTheory.CategoryStruct.id X.unop.obj₃)).op

The unit isomorphism of the equivalence triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ .

Equations
• One or more equations did not get rendered due to their size.
Instances For

The counit isomorphism of the equivalence triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ .

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
@[simp]
@[simp]
@[simp]

An anti-equivalence between the categories of triangles in C and in Cᵒᵖ. A triangle in Cᵒᵖ shall be distinguished iff it correspond to a distinguished triangle in C via this equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For

A triangle in Cᵒᵖ shall be distinguished iff it corresponds to a distinguished triangle in C via the equivalence triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff {C : Type u_1} [] [] :
(.obj T).unop CategoryTheory.Pretriangulated.distinguishedTriangles
theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff' {C : Type u_1} [] [] :
∃ (T' : ) (_ : T' CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (T .obj ())
@[simp]
@[simp]
@[simp]
@[simp]

Up to rotation, the contractible triangle X ⟶ X ⟶ 0 ⟶ X⟦1⟧ for X : Cᵒᵖ corresponds to the contractible triangle for X.unop in C.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Isomorphism expressing a compatibility of the equivalence triangleOpEquivalence C with the rotation of triangles.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Pretriangulated.Opposite.distinguished_cocone_triangle {C : Type u_1} [] [] {X : Cᵒᵖ} {Y : Cᵒᵖ} (f : X Y) :
∃ (Z : Cᵒᵖ) (g : Y Z) (h : Z .obj X),
theorem CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism {C : Type u_1} [] [] (a : T₁.obj₁ T₂.obj₁) (b : T₁.obj₂ T₂.obj₂) (comm : = ) :
∃ (c : T₁.obj₃ T₂.obj₃), = CategoryTheory.CategoryStruct.comp T₁.mor₃ (.map a) =

The pretriangulated structure on the opposite category of a pretriangulated category. It is a scoped instance, so that we need to open CategoryTheory.Pretriangulated.Opposite in order to be able to use it: the reason is that it relies on the definition of the shift on the opposite category Cᵒᵖ, for which it is unclear whether it should be a global instance or not.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff {C : Type u_1} [] [] :
T CategoryTheory.Pretriangulated.distinguishedTriangles (.obj T).unop CategoryTheory.Pretriangulated.distinguishedTriangles
theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff' {C : Type u_1} [] [] :
T CategoryTheory.Pretriangulated.distinguishedTriangles ∃ (T' : ) (_ : T' CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (T .obj ())
theorem CategoryTheory.Pretriangulated.op_distinguished {C : Type u_1} [] [] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
.obj () CategoryTheory.Pretriangulated.distinguishedTriangles
theorem CategoryTheory.Pretriangulated.unop_distinguished {C : Type u_1} [] [] (hT : T CategoryTheory.Pretriangulated.distinguishedTriangles) :
(.obj T).unop CategoryTheory.Pretriangulated.distinguishedTriangles