Triangles in the opposite category of a (pre)triangulated category

Let C be a (pre)triangulated category. In CategoryTheory.Triangulated.Opposite.Basic, we have constructed a shift on Cᵒᵖ that will be part of a structure of (pre)triangulated category. In this file, we construct an equivalence of categories between (Triangle C)ᵒᵖ and Triangle Cᵒᵖ, called CategoryTheory.Pretriangulated.triangleOpEquivalence. It 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).

References

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

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.functor (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] : Functor (Triangle C)ᵒᵖ (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) [Category.{u_2, u_1} C] [HasShift C ℤ] {T₁ T₂ : (Triangle C)ᵒᵖ} (φ : T₁ ⟶ T₂) : ((functor C).map φ).hom₂ = φ.unop.hom₂.op

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.inverse (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] : Functor (Triangle Cᵒᵖ) (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_obj (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] (T : Triangle Cᵒᵖ) : (inverse C).obj T = Opposite.op (Triangle.mk T.mor₂.unop T.mor₁.unop (CategoryStruct.comp ((opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁).unop ((shiftFunctor C 1).map T.mor₃.unop)))

@[simp]

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

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.unitIso (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] : Functor.id (Triangle C)ᵒᵖ ≅ (functor C).comp (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) [Category.{u_2, u_1} C] [HasShift C ℤ] (X : (Triangle C)ᵒᵖ) : (unitIso C).inv.app X = ((Opposite.unop X).homMk (Triangle.mk (Opposite.unop X).mor₁ (Opposite.unop X).mor₂ (CategoryStruct.comp ((opShiftFunctorEquivalence C 1).unitIso.inv.app (Opposite.op (Opposite.unop X).obj₃)).unop ((shiftFunctor C 1).map (CategoryStruct.comp ((shiftFunctor Cᵒᵖ 1).map (Opposite.unop X).mor₃.op).unop ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op (Opposite.unop X).obj₁)).unop)))) (CategoryStruct.id (Opposite.unop X).obj₁) (CategoryStruct.id (Opposite.unop X).obj₂) (CategoryStruct.id (Opposite.unop X).obj₃) ⋯ ⋯ ⋯).op

@[simp]

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

noncomputable def CategoryTheory.Pretriangulated.TriangleOpEquivalence.counitIso (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] : (inverse C).comp (functor C) ≅ Functor.id (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) [Category.{u_2, u_1} C] [HasShift C ℤ] (X : Triangle Cᵒᵖ) : ((counitIso C).hom.app X).hom₁ = CategoryStruct.id X.obj₁

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Pretriangulated.triangleOpEquivalence (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] : (Triangle C)ᵒᵖ ≌ 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_functor (C : Type u_1) [Category.{u_2, u_1} C] [HasShift C ℤ] : (triangleOpEquivalence C).functor = TriangleOpEquivalence.functor C

@[simp]

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

@[simp]

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

@[simp]

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