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
🔸 coverage
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
    Instances For
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      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
      🔸 coverage
      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
        Instances For
          source
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          📐 coverage
          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
          🔸 coverage
          instance CategoryTheory.Pretriangulated.Opposite.instCommShiftOppositeOpOpInt (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] :
          (opOp C).CommShift ℤ
          Equations
            source
            🔸 coverage
            instance CategoryTheory.Pretriangulated.Opposite.instCommShiftOppositeUnopUnopInt (C : Type u_1) [Category.{v_1, u_1} C] [HasShift C ℤ] :
            (unopUnop C).CommShift ℤ
            Equations
              source
              📐 coverage
              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
              📐 coverage
              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
              📐 coverage
              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
              📐 coverage
              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
              📐 coverage
              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
              📐 coverage
              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
              📐 coverage
              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
              📐 coverage
              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
              🔸 coverage
              instance CategoryTheory.Pretriangulated.instCommShiftOppositeFunctorOpOpEquivalenceInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] :
              (opOpEquivalence C).functor.CommShift ℤ
              Equations
                source
                🔸 coverage
                instance CategoryTheory.Pretriangulated.instCommShiftOppositeInverseOpOpEquivalenceInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] :
                (opOpEquivalence C).inverse.CommShift ℤ
                Equations
                  source
                  📐 coverage
                  instance CategoryTheory.Pretriangulated.instCommShiftOppositeOpOpEquivalenceInt {C : Type u_1} [Category.{v_1, u_1} C] [HasShift C ℤ] :
                  (opOpEquivalence C).CommShift ℤ
                  source
                  📐 coverage
                  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
                  📐 coverage
                  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
                  📐 coverage
                  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