Documentation

Mathlib.CategoryTheory.Triangulated.Opposite.Basic

The shift on the opposite category of a pretriangulated category #

Let C be a (pre)triangulated category. We already have a shift on Cᵒᵖ given by CategoryTheory.Shift.Opposite, but this is not the shift that we want to make Cᵒᵖ into a (pre)triangulated category. The correct 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.

References #

source
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
Instances For
    source
    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
    source
    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
    Instances For
      source
      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
      source
      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)
      source
      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))))
      source
      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)))
      source
      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))
      source
      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.
      Instances For
        source
        @[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
        source
        @[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.

        source
        @[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
        source
        @[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)
        source
        @[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
        source
        @[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)
        source
        @[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
        source
        @[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)
        source
        @[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)
        source
        @[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)
        source
        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
        source
        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
        source
        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))
        source
        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)))
        source
        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
        source
        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
        source
        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)
        source
        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)