Documentation

Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

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 which would require that the triangle (op X)⟦-1⟧ ⟶ op Z ⟶ op Y ⟶ op X (without signs) is antidistinguished.

References #

source
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.
Instances For
    source
    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
    source
    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'))
    source
    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
    source
    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.
    Instances For
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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
      source
      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.
      Instances For
        source
        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
        source
        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
        source
        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₃
        source
        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.
        Instances For
          source
          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
          source
          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'))
          source
          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
          source
          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
          source
          theorem CategoryTheory.Functor.map_distinguished_op_exact {C : Type u_1} [CategoryTheory.Category.{u_4, 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_3, 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