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 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

noncomputable def CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : CategoryTheory.HasShift Cᵒᵖ ℤ

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

• CategoryTheory.Pretriangulated.Opposite.instHasShiftOppositeInt C = inferInstance

instance CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (n : ℤ) : (CategoryTheory.shiftFunctor Cᵒᵖ n).Additive

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Pretriangulated.shiftFunctorOpIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n m : ℤ) (hnm : n + m = 0) : CategoryTheory.shiftFunctor Cᵒᵖ n ≅ (CategoryTheory.shiftFunctor C m).op

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

Equations

• CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm = CategoryTheory.eqToIso ⋯

theorem CategoryTheory.Pretriangulated.shiftFunctorZero_op_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) : (CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C 0 0 ⋯).hom.app X) ((CategoryTheory.shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

theorem CategoryTheory.Pretriangulated.shiftFunctorZero_op_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) : (CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C 0 0 ⋯).inv.app X)

theorem CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (a₁ a₂ a₃ : ℤ) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : ℤ) (h₁ : a₁ + b₁ = 0) (h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0) : (CategoryTheory.shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₃ b₃ h₃).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((CategoryTheory.shiftFunctor C b₁).toPrefunctor.1 (Opposite.unop X)))) ((CategoryTheory.shiftFunctor Cᵒᵖ a₂).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₁ b₁ h₁).inv.app X))))

theorem CategoryTheory.Pretriangulated.shiftFunctorAdd'_op_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (a₁ a₂ a₃ : ℤ) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : ℤ) (h₁ : a₁ + b₁ = 0) (h₂ : a₂ + b₂ = 0) (h₃ : a₃ + b₃ = 0) : (CategoryTheory.shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ a₂).map ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₁ b₁ h₁).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((CategoryTheory.shiftFunctor C b₁).op.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C a₃ b₃ h₃).inv.app X)))

theorem CategoryTheory.Pretriangulated.shiftFunctor_op_map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n m : ℤ) (hnm : n + m = 0) {K L : Cᵒᵖ} (φ : K ⟶ L) : (CategoryTheory.shiftFunctor Cᵒᵖ n).map φ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).hom.app K) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m).map φ.unop).op ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C n m hnm).inv.app L))

noncomputable def CategoryTheory.Pretriangulated.opShiftFunctorEquivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) : Cᵒᵖ ≌ Cᵒᵖ

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.

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor = CategoryTheory.shiftFunctor Cᵒᵖ n

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse = (CategoryTheory.shiftFunctor C n).op

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 {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X) ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ} (h : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op h)

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X) f

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f).unop).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op) ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X) f

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X) (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X) ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op)

@[simp]

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) {Z : Cᵒᵖ} (h : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op) h)

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 0).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop).op

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_zero_unitIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 0).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 0).map ((CategoryTheory.shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop).op ((CategoryTheory.shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_hom_app_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (m n p : ℤ) (h : m + n = p) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C p).unitIso.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).unitIso.hom.app ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)).unop).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C m n p h).hom.app (Opposite.unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).functor.obj ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)))).op ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' Cᵒᵖ n m p ⋯).inv.app X).unop).op))

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_unitIso_inv_app_eq {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (m n p : ℤ) (h : m + n = p) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C p).unitIso.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C p).map ((CategoryTheory.shiftFunctorAdd' Cᵒᵖ n m p ⋯).hom.app X).unop).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C m n p h).inv.app (Opposite.unop (((CategoryTheory.shiftFunctor Cᵒᵖ n).comp (CategoryTheory.shiftFunctor Cᵒᵖ m)).obj X))).op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C m).unitIso.inv.app ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)).unop).op ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)))

theorem CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ) : (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop = ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop

theorem CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_hom_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ) : (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop = ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_app_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) = (CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app X)

theorem CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ) : (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) = (CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)

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.

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₂ = φ.unop.hom₂.op

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₃ = φ.unop.hom₁.op

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_map_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).map φ).hom₁ = φ.unop.hom₃.op

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (T : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ) : (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).obj T = CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop T).mor₂.op (Opposite.unop T).mor₁.op (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop T).obj₁)) ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop T).mor₃.op))

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : CategoryTheory.Functor (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ

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.

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ} (φ : T₁ ⟶ T₂) : (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).map φ = Quiver.Hom.op { hom₁ := φ.hom₃.unop, hom₂ := φ.hom₂.unop, hom₃ := φ.hom₁.unop, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse_obj (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).obj T = Opposite.op (CategoryTheory.Pretriangulated.Triangle.mk T.mor₂.unop T.mor₁.unop (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop ((CategoryTheory.shiftFunctor C 1).map T.mor₃.unop)))

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ ≅ (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C).comp (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C)

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.

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_inv_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ) : (CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).inv.app X = ((Opposite.unop X).homMk (CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso_hom_app (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : (CategoryTheory.Pretriangulated.Triangle C)ᵒᵖ) : (CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C).hom.app X = ((CategoryTheory.Pretriangulated.Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((CategoryTheory.shiftFunctor C 1).map (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))).homMk (Opposite.unop X) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₁) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₂) (CategoryTheory.CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : (CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C).comp (CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C) ≅ CategoryTheory.Functor.id (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)

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.

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₂ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₂ = CategoryTheory.CategoryStruct.id X.obj₂

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_hom_app_hom₁ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁

@[simp]

theorem CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso_inv_app_hom₃ (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : ((CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C).inv.app X).hom₃ = CategoryTheory.CategoryStruct.id X.obj₃

noncomputable def CategoryTheory.Pretriangulated.triangleOpEquivalence (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [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 correspond to a distinguished triangle in C via this equivalence.

Equations

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

@[simp]

theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_counitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : (CategoryTheory.Pretriangulated.triangleOpEquivalence C).counitIso = CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso C

@[simp]

theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_unitIso (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : (CategoryTheory.Pretriangulated.triangleOpEquivalence C).unitIso = CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso C

@[simp]

theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor = CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor C

@[simp]

theorem CategoryTheory.Pretriangulated.triangleOpEquivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] : (CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse = CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse C

def CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : Set (CategoryTheory.Pretriangulated.Triangle Cᵒᵖ)

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.

theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔ Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔ ∃ (T' : CategoryTheory.Pretriangulated.Triangle C) (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))

theorem CategoryTheory.Pretriangulated.Opposite.isomorphic_distinguished {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T₁ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C) (T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (e : T₂ ≅ T₁) : T₂ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C

noncomputable def CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : CategoryTheory.Pretriangulated.contractibleTriangle X ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op (CategoryTheory.Pretriangulated.contractibleTriangle (Opposite.unop X)).invRotate)

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.

@[simp]

theorem CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₁ = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₁ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₁ = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₂ = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₂ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₂ = CategoryTheory.CategoryStruct.id X

@[simp]

theorem CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₃ = (⋯.iso ⋯).inv

@[simp]

theorem CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_hom_hom₃ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ) : (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).hom.hom₃ = (⋯.iso ⋯).hom

theorem CategoryTheory.Pretriangulated.Opposite.contractible_distinguished {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (X : Cᵒᵖ) : CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C

noncomputable def CategoryTheory.Pretriangulated.Opposite.rotateTriangleOpEquivalenceInverseObjRotateUnopIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : (Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T.rotate)).rotate ≅ Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T)

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.

theorem CategoryTheory.Pretriangulated.Opposite.rotate_distinguished_triangle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔ T.rotate ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C

theorem CategoryTheory.Pretriangulated.Opposite.distinguished_cocone_triangle {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {X Y : Cᵒᵖ} (f : X ⟶ Y) : ∃ (Z : Cᵒᵖ) (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor Cᵒᵖ 1).obj X), CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C

theorem CategoryTheory.Pretriangulated.Opposite.complete_distinguished_triangle_morphism {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C) (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁) : ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧ CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor Cᵒᵖ 1).map a) = CategoryTheory.CategoryStruct.comp c T₂.mor₃

def CategoryTheory.Pretriangulated.Opposite.instOpposite {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : CategoryTheory.Pretriangulated Cᵒᵖ

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.

theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Pretriangulated.mem_distTriang_op_iff' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ ∃ (T' : CategoryTheory.Pretriangulated.Triangle C) (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))

theorem CategoryTheory.Pretriangulated.op_distinguished {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Pretriangulated.unop_distinguished {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : Opposite.unop ((CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse.obj T) ∈ CategoryTheory.Pretriangulated.distinguishedTriangles

theorem CategoryTheory.Functor.map_distinguished_op_exact {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] {A : Type u_2} [CategoryTheory.Category.{u_4, u_2} A] [CategoryTheory.Abelian A] (F : CategoryTheory.Functor Cᵒᵖ A) [F.IsHomological] (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) : ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).op.map F).Exact