Documentation

Mathlib.CategoryTheory.Triangulated.Adjunction

The adjoint functor is triangulated #

If a functor F : C ⥤ D between pretriangulated categories is triangulated, and if we have an adjunction F ⊣ G, then G is also a triangulated functor. We deduce the symmetric statement (if G is a triangulated functor, then so is F) using opposite categories.

We then introduce a class IsTriangulated for adjunctions: an adjunction F ⊣ G is called triangulated if both F and G are triangulated, and if the adjunction is compatible with the shifts by ℤ on F and G (in the sense of Adjunction.CommShift); we prove that this is compatible with composition and that the identity adjunction is triangulated. Thanks to the results above, an adjunction carrying an Adjunction.CommShift instance is triangulated as soon as one of the adjoint functors is triangulated.

We finally specialize these structures to equivalences of categories, and prove that, if E : C ≌ D is an equivalence of pretriangulated categories, then E.functor is triangulated if and only if E.inverse is triangulated.

source
theorem CategoryTheory.Adjunction.isTriangulated_rightAdjoint {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [F.IsTriangulated] :
G.IsTriangulated

The right adjoint of a triangulated functor is triangulated.

source
theorem CategoryTheory.Adjunction.isTriangulated_leftAdjoint {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [G.IsTriangulated] :
F.IsTriangulated

The left adjoint of a triangulated functor is triangulated.

source
class CategoryTheory.Adjunction.IsTriangulated {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] :
Prop

We say that an adjunction F ⊣ G is triangulated if it is compatible with the CommShift structures on F and G (in the sense of Adjunction.CommShift) and if both F and G are triangulated functors.

  • commShift : adj.CommShift ℤ
  • leftAdjoint_isTriangulated : F.IsTriangulated
  • rightAdjoint_isTriangulated : G.IsTriangulated
Instances
    source
    theorem CategoryTheory.Adjunction.IsTriangulated.mk' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [F.IsTriangulated] :
    adj.IsTriangulated

    Constructor for Adjunction.IsTriangulated.

    source
    theorem CategoryTheory.Adjunction.IsTriangulated.mk'' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] [G.IsTriangulated] :
    adj.IsTriangulated

    Constructor for Adjunction.IsTriangulated.

    source
    instance CategoryTheory.Adjunction.IsTriangulated.id {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] :
    CategoryTheory.Adjunction.id.IsTriangulated

    The identity adjunction is triangulated.

    source
    instance CategoryTheory.Adjunction.IsTriangulated.comp {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.CommShift ℤ] [G.CommShift ℤ] [adj.CommShift ℤ] {E : Type u_3} [CategoryTheory.Category.{u_6, u_3} E] {F' : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor E D} (adj' : F' ⊣ G') [CategoryTheory.Limits.HasZeroObject E] [CategoryTheory.Preadditive E] [CategoryTheory.HasShift E ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor E n).Additive] [CategoryTheory.Pretriangulated E] [F'.CommShift ℤ] [G'.CommShift ℤ] [adj'.CommShift ℤ] [adj.IsTriangulated] [adj'.IsTriangulated] :
    (adj.comp adj').IsTriangulated

    A composition of triangulated adjunctions is triangulated.

    source
    @[reducible, inline]
    abbrev CategoryTheory.Equivalence.IsTriangulated {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] :
    Prop

    We say that an equivalence of categories E is triangulated if both E.functor and E.inverse are triangulated functors.

    Equations
    • E.IsTriangulated = E.toAdjunction.IsTriangulated
    Instances For
      source
      instance CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.IsTriangulated] :
      E.functor.IsTriangulated
      source
      instance CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverse {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.IsTriangulated] :
      E.inverse.IsTriangulated
      source
      instance CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverseSymmOfFunctor {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [h : E.functor.IsTriangulated] :
      E.symm.inverse.IsTriangulated
      source
      instance CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctorSymmOfInverse {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.inverse.CommShift ℤ] [h : E.inverse.IsTriangulated] :
      E.symm.functor.IsTriangulated
      source
      theorem CategoryTheory.Equivalence.IsTriangulated.mk' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ] (h : E.functor.IsTriangulated) :
      E.IsTriangulated

      Constructor for Equivalence.IsTriangulated.

      source
      theorem CategoryTheory.Equivalence.IsTriangulated.mk'' {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ] (h : E.inverse.IsTriangulated) :
      E.IsTriangulated

      Constructor for Equivalence.IsTriangulated.

      source
      instance CategoryTheory.Equivalence.IsTriangulated.refl {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Preadditive C] [CategoryTheory.HasShift C ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] :
      CategoryTheory.Equivalence.refl.IsTriangulated

      The identity equivalence is triangulated.

      source
      instance CategoryTheory.Equivalence.IsTriangulated.symm {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ] [E.IsTriangulated] :
      E.symm.IsTriangulated

      If the equivalence E is triangulated, so is the equivalence E.symm.

      source
      instance CategoryTheory.Equivalence.IsTriangulated.trans {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.HasShift C ℤ] [CategoryTheory.HasShift D ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [CategoryTheory.Pretriangulated C] [CategoryTheory.Pretriangulated D] (E : C ≌ D) [E.functor.CommShift ℤ] [E.inverse.CommShift ℤ] [E.CommShift ℤ] {D' : Type u_3} [CategoryTheory.Category.{u_6, u_3} D'] [CategoryTheory.Limits.HasZeroObject D'] [CategoryTheory.Preadditive D'] [CategoryTheory.HasShift D' ℤ] [∀ (n : ℤ), (CategoryTheory.shiftFunctor D' n).Additive] [CategoryTheory.Pretriangulated D'] {E' : D ≌ D'} [E'.functor.CommShift ℤ] [E'.inverse.CommShift ℤ] [E'.CommShift ℤ] [E.IsTriangulated] [E'.IsTriangulated] :
      (E.trans E').IsTriangulated

      If equivalences E : C ≌ D and E' : D ≌ F are triangulated, so is E.trans E'.