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 #

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

    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} [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) :
      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) :

      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.

        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_map (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.HasShift C ] {T₁ : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ} {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₃ := }

          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

            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

                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

                    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

                        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