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ᵒᵖ was constructed in ``CategoryTheory.Triangulated.Opposite.Basic, and is such that shifting by n : ℤonCᵒᵖcorresponds to the shift by `-nonC. In CategoryTheory.Triangulated.Opposite.Triangle, we constructed an equivalence (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ, called CategoryTheory.Pretriangulated.triangleOpEquivalence`.

Here, we defined the notion of distinguished triangles in Cᵒᵖ, such that triangleOpEquivalence sends distinguished triangles in C to distinguished triangles in Cᵒᵖ. In other words, 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]

def CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : Set (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} [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Triangle Cᵒᵖ) : T ∈ distinguishedTriangles C ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

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

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

noncomputable def CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso {C : Type u_1} [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Cᵒᵖ) : contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj (Opposite.op (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} [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] (X : Cᵒᵖ) : (contractibleTriangleIso X).hom.hom₃ = (⋯.iso ⋯).hom

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

noncomputable def CategoryTheory.Pretriangulated.Opposite.rotateTriangleOpEquivalenceInverseObjRotateUnopIso {C : Type u_1} [Category.{u_2, u_1} C] [HasShift C ℤ] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] (T : Triangle Cᵒᵖ) : (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate ≅ Opposite.unop ((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} [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Triangle Cᵒᵖ) : T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

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

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

noncomputable def CategoryTheory.Pretriangulated.Opposite.instOpposite {C : Type u_1} [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] : 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} [Category.{u_2, u_1} C] [HasShift C ℤ] [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] (T : Triangle Cᵒᵖ) : T ∈ distinguishedTriangles ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ distinguishedTriangles

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

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

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

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