Documentation

Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

The triangulated equivalence Cᵒᵖᵒᵖ ≌ C. #

In this file, we show that if C is a pretriangulated category, then the functors opOp C : C ⥤ Cᵒᵖᵒᵖ and unopUnop C : Cᵒᵖᵒᵖ ⥤ C are triangulated. We also show that the unit and counit isomorphisms of the equivalence opOpEquivalence C : Cᵒᵖᵒᵖ ≌ C are compatible with shifts, which is summarized by the property (opOpEquivalence C).IsTriangulated.

source
def CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (n : ℤ) :
(shiftFunctor C n).comp (opOp C) ≅ (opOp C).comp (shiftFunctor Cᵒᵖᵒᵖ n)

The isomorphism expressing the commutation of the functor opOp C : C ⥤ Cᵒᵖᵒᵖ with the shift by n : ℤ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) :
    (iso C n).hom.app X = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X)))
    source
    theorem CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖᵒᵖ} (h : (shiftFunctor Cᵒᵖᵒᵖ n).obj ((opOp C).obj X) ⟶ Z) :
    CategoryStruct.comp ((iso C n).hom.app X) h = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op (CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X))) h)
    source
    theorem CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) :
    (iso C n).inv.app X = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X))) ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op
    source
    theorem CategoryTheory.Pretriangulated.Opposite.OpOpCommShift.iso_inv_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖᵒᵖ} (h : (opOp C).obj ((shiftFunctor C n).obj X) ⟶ Z) :
    CategoryStruct.comp ((iso C n).inv.app X) h = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X))) (CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op h)
    source
    def CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] (n : ℤ) :
    (shiftFunctor Cᵒᵖᵒᵖ n).comp (unopUnop C) ≅ (unopUnop C).comp (shiftFunctor C n)

    The isomorphism expressing the commutation of the functor unopUnop C : Cᵒᵖᵒᵖ ⥤ C with the shift by n : ℤ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) :
      (iso C n).hom.app X = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop
      source
      theorem CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : C} (h : (shiftFunctor C n).obj ((unopUnop C).obj X) ⟶ Z) :
      CategoryStruct.comp ((iso C n).hom.app X) h = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop (CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop h)
      source
      theorem CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) :
      (iso C n).inv.app X = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop
      source
      theorem CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : C} (h : (unopUnop C).obj ((shiftFunctor Cᵒᵖᵒᵖ n).obj X) ⟶ Z) :
      CategoryStruct.comp ((iso C n).inv.app X) h = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop (CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop h)
      source
      instance CategoryTheory.Pretriangulated.Opposite.instCommShiftOppositeOpOpInt (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] :
      (opOp C).CommShift ℤ
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance CategoryTheory.Pretriangulated.Opposite.instCommShiftOppositeUnopUnopInt (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] :
      (unopUnop C).CommShift ℤ
      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) :
      (Functor.commShiftIso (opOp C) n).hom.app X = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X)))
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_opOp_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖᵒᵖ} (h : (shiftFunctor Cᵒᵖᵒᵖ n).obj ((opOp C).obj X) ⟶ Z) :
      CategoryStruct.comp ((Functor.commShiftIso (opOp C) n).hom.app X) h = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.op X)).op (CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app (Opposite.op (Opposite.op X))) h)
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) :
      (Functor.commShiftIso (opOp C) n).inv.app X = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X))) ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_opOp_inv_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : C) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : Cᵒᵖᵒᵖ} (h : (opOp C).obj ((shiftFunctor C n).obj X) ⟶ Z) :
      CategoryStruct.comp ((Functor.commShiftIso (opOp C) n).inv.app X) h = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app (Opposite.op (Opposite.op X))) (CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.op X)).op h)
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) :
      (Functor.commShiftIso (unopUnop C) n).hom.app X = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : C} (h : (shiftFunctor C n).obj ((unopUnop C).obj X) ⟶ Z) :
      CategoryStruct.comp ((Functor.commShiftIso (unopUnop C) n).hom.app X) h = CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop (CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop h)
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) :
      (Functor.commShiftIso (unopUnop C) n).inv.app X = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop
      source
      theorem CategoryTheory.Pretriangulated.commShiftIso_unopUnop_inv_app_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] (X : Cᵒᵖᵒᵖ) (n m : ℤ) (hnm : n + m = 0 := by lia) {Z : C} (h : (unopUnop C).obj ((shiftFunctor Cᵒᵖᵒᵖ n).obj X) ⟶ Z) :
      CategoryStruct.comp ((Functor.commShiftIso (unopUnop C) n).inv.app X) h = CategoryStruct.comp ((shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop (CategoryStruct.comp ((shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop h)
      source
      instance CategoryTheory.Pretriangulated.instCommShiftOppositeFunctorOpOpEquivalenceInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] :
      (opOpEquivalence C).functor.CommShift ℤ
      Equations
      source
      instance CategoryTheory.Pretriangulated.instCommShiftOppositeInverseOpOpEquivalenceInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] :
      (opOpEquivalence C).inverse.CommShift ℤ
      Equations
      source
      instance CategoryTheory.Pretriangulated.instCommShiftOppositeOpOpEquivalenceInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] :
      (opOpEquivalence C).CommShift ℤ
      source
      instance CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOp {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] :
      (opOp C).IsTriangulated
      source
      instance CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] :
      (opOpEquivalence C).IsTriangulated
      source
      instance CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] [Preadditive C] [Limits.HasZeroObject C] [∀ (n : ℤ), (shiftFunctor C n).Additive] [Pretriangulated C] :
      (unopUnop C).IsTriangulated