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.
theorem
CategoryTheory.Adjunction.isTriangulated_rightAdjoint
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F : Functor C D}
{G : 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.
theorem
CategoryTheory.Adjunction.isTriangulated_leftAdjoint
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F : Functor C D}
{G : 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.
class
CategoryTheory.Adjunction.IsTriangulated
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.CommShift ℤ]
[G.CommShift ℤ]
:
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
theorem
CategoryTheory.Adjunction.IsTriangulated.mk'
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.CommShift ℤ]
[G.CommShift ℤ]
[adj.CommShift ℤ]
[F.IsTriangulated]
:
adj.IsTriangulated
Constructor for Adjunction.IsTriangulated.
theorem
CategoryTheory.Adjunction.IsTriangulated.mk''
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.CommShift ℤ]
[G.CommShift ℤ]
[adj.CommShift ℤ]
[G.IsTriangulated]
:
adj.IsTriangulated
Constructor for Adjunction.IsTriangulated.
instance
CategoryTheory.Adjunction.IsTriangulated.id
{C : Type u_1}
[Category.{u_3, u_1} C]
[Limits.HasZeroObject C]
[Preadditive C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
:
Adjunction.id.IsTriangulated
The identity adjunction is triangulated.
instance
CategoryTheory.Adjunction.IsTriangulated.comp
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
[F.CommShift ℤ]
[G.CommShift ℤ]
[adj.CommShift ℤ]
{E : Type u_3}
[Category.{u_6, u_3} E]
{F' : Functor D E}
{G' : Functor E D}
(adj' : F' ⊣ G')
[Limits.HasZeroObject E]
[Preadditive E]
[HasShift E ℤ]
[∀ (n : ℤ), (shiftFunctor E n).Additive]
[Pretriangulated E]
[F'.CommShift ℤ]
[G'.CommShift ℤ]
[adj'.CommShift ℤ]
[adj.IsTriangulated]
[adj'.IsTriangulated]
:
(adj.comp adj').IsTriangulated
A composition of triangulated adjunctions is triangulated.
@[reducible, inline]
abbrev
CategoryTheory.Equivalence.IsTriangulated
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[E.inverse.CommShift ℤ]
:
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
instance
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctor
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[E.inverse.CommShift ℤ]
[E.IsTriangulated]
:
E.functor.IsTriangulated
instance
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverse
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[E.inverse.CommShift ℤ]
[E.IsTriangulated]
:
E.inverse.IsTriangulated
instance
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverseSymmOfFunctor
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[h : E.functor.IsTriangulated]
:
E.symm.inverse.IsTriangulated
instance
CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedFunctorSymmOfInverse
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.inverse.CommShift ℤ]
[h : E.inverse.IsTriangulated]
:
E.symm.functor.IsTriangulated
theorem
CategoryTheory.Equivalence.IsTriangulated.mk'
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[E.inverse.CommShift ℤ]
[E.CommShift ℤ]
(h : E.functor.IsTriangulated)
:
E.IsTriangulated
Constructor for Equivalence.IsTriangulated.
theorem
CategoryTheory.Equivalence.IsTriangulated.mk''
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_3, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[E.inverse.CommShift ℤ]
[E.CommShift ℤ]
(h : E.inverse.IsTriangulated)
:
E.IsTriangulated
Constructor for Equivalence.IsTriangulated.
instance
CategoryTheory.Equivalence.IsTriangulated.refl
{C : Type u_1}
[Category.{u_3, u_1} C]
[Limits.HasZeroObject C]
[Preadditive C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[Pretriangulated C]
:
Equivalence.refl.IsTriangulated
The identity equivalence is triangulated.
instance
CategoryTheory.Equivalence.IsTriangulated.symm
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[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.
instance
CategoryTheory.Equivalence.IsTriangulated.trans
{C : Type u_1}
{D : Type u_2}
[Category.{u_4, u_1} C]
[Category.{u_5, u_2} D]
[Limits.HasZeroObject C]
[Limits.HasZeroObject D]
[Preadditive C]
[Preadditive D]
[HasShift C ℤ]
[HasShift D ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), (shiftFunctor D n).Additive]
[Pretriangulated C]
[Pretriangulated D]
(E : C ≌ D)
[E.functor.CommShift ℤ]
[E.inverse.CommShift ℤ]
[E.CommShift ℤ]
{D' : Type u_3}
[Category.{u_6, u_3} D']
[Limits.HasZeroObject D']
[Preadditive D']
[HasShift D' ℤ]
[∀ (n : ℤ), (shiftFunctor D' n).Additive]
[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'.