The dg category of dg functors is pretriangulated

DGFunctor C D is a dg category, and IsPretriangulated asks it for three things: a zero object, a shift of every object in every degree, and a cone on every closed degree-zero morphism. When D is pretriangulated all three are available objectwise, and this file assembles them into the instance.

• The zero object is the constant dg functor at a dg zero object of D.
• The shift is DGFunctor.shiftedFunctor, whose value at X is a chosen shift of F.obj X and whose action on a degree-p morphism is the transport of F.map p f across those choices, with the sign (-1)^(n * p).
• The cone is HomogeneousNatTrans.ConeData.isConeOf, built from the objectwise cones of a closed degree-zero dg natural transformation. Its splitting is natural because the cone projections are, which is what ConeData.fst and ConeData.snd record.

The last of these is what makes the repository's objectwise twist a cone of functors, which is the form Anno--Logvinenko's triangle SR ⟶ Id_B ⟶ T takes.

The sign on the shift is forced

Writing s X : IsShiftBy (F.obj X) n (Y X) for the chosen witnesses, the map on a degree-p morphism is

(F[n]).map p f = (-1)^(n * p) • (s X).inv ≫ F.map p f ≫ (s Y).hom,

and the sign is forced, not chosen. Both (s X).inv and (s Y).hom are closed, so the Leibniz rule leaves one term, and with the repository's convention δ(a ≫ b) = a ≫ δb + (-1)^|b| δa ≫ b and |(s Y).hom| = -n that term carries (-1)^n; this is IsShiftBy.shiftMap_d. A dg functor must satisfy map (p+1) (δ f) = δ (map p f), so the coefficient ε must satisfy ε (p+1) = (-1)^n ε p. No constant sign does, and ε p = (-1)^(n * p) is the solution. With it map_id is the unit law, map_comp is (-1)^(n p) (-1)^(n q) = (-1)^(n (p+q)), and the shift witness is the family (s X).hom, whose graded naturality is exactly the same sign cancelling against (-1)^(-n p).

Two spellings of the same object

shiftObj names the chosen shift and shiftedFunctor carries it as its obj field, so (F.shiftedFunctor n).obj X and F.shiftObj n X are definitionally equal and syntactically different. A goal that mixes them is not type-correct at instances transparency, and rw then rejects every motive it builds. Two proofs below therefore go through show or through the object-general lemmas IsShiftBy.comp_inv_naturality and IsShiftBy.comp_inv_comp_hom, where unification at default transparency identifies the two spellings; each such place says so.

What this does not give

IsPretriangulated is dg data, not a triangulated structure. Turning the instance below into a pretriangulated structure on H⁰ (DGFunctor C D) needs the DGEnhancement layer, and nothing here asserts that the shift chosen objectwise agrees with any shift already present on H⁰.

def CategoryTheory.DGFunctor.constZero {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (Z : D) (hZ : DGCategoryStruct.dgId Z = 0) : DGFunctor C D

The dg functor constant at an object with vanishing dg identity.

Only a zero object gives a dg functor this way: map_id asks for 0 = dgId Z, which is exactly the hypothesis.

Equations

• CategoryTheory.DGFunctor.constZero Z hZ = { obj := fun (x : C) => Z, map := fun {X Y : C} (x : ℤ) => 0, map_d := ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.DGFunctor.constZero_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (Z : D) (hZ : DGCategoryStruct.dgId Z = 0) (X : C) : (constZero Z hZ).obj X = Z

theorem CategoryTheory.DGFunctor.constZero_map {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (Z : D) (hZ : DGCategoryStruct.dgId Z = 0) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((constZero Z hZ).map p) f = 0

theorem CategoryTheory.DGFunctor.dgId_constZero_eq_zero {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (Z : D) (hZ : DGCategoryStruct.dgId Z = 0) : DGCategoryStruct.dgId (constZero Z hZ) = 0

The dg category of dg functors has a zero object, as soon as the target has one: the constant functor at it.

theorem CategoryTheory.DGFunctor.exists_zero_dgFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] : ∃ (Z : DGFunctor C D), DGCategoryStruct.dgId Z = 0

The dg category of dg functors has a zero object whenever the target is pretriangulated.

theorem CategoryTheory.DGFunctor.exists_cone_dgFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} (α : ↑((DGCategoryStruct.dgHom F G).X 0)) (hα : α ∈ cocycles F G) : ∃ (Z : DGFunctor C D), Nonempty (IsConeOf α Z)

Every closed degree-zero dg natural transformation has a cone in the dg category of dg functors, whenever the target is pretriangulated.

This is ConeData.isConeOf applied to the objectwise cones the target supplies, and it is the exists_cone field of a pretriangulated structure on DGFunctor C D. The remaining field is the shift; see the module docstring.

noncomputable def CategoryTheory.DGFunctor.shiftObj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : C) : D

The chosen shift by n of one value of F.

Equations

• F.shiftObj n X = ⋯.choose

noncomputable def CategoryTheory.DGFunctor.shiftWitness {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : C) : IsShiftBy (F.obj X) n (F.shiftObj n X)

The chosen shift witness at one object.

Equations

• F.shiftWitness n X = ⋯.some

noncomputable def CategoryTheory.DGFunctor.shiftedFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : DGFunctor C D

The shift of a dg functor.

The value at X is a chosen shift of F.obj X, and the action on a degree-p morphism is the transport of F.map p f across those choices, multiplied by (-1)^(n * p).

That sign is forced. IsShiftBy.shiftMap_d says transport anticommutes with the differential by (-1)^n, so a coefficient ε makes the assignment a dg functor only if ε (p+1) = (-1)^n ε p; no constant sign satisfies that, and (-1)^(n * p) is the solution. With it map_id and map_comp also hold, the latter because (-1)^(n p) (-1)^(n q) = (-1)^(n (p+q)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctor_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : C) : (F.shiftedFunctor n).obj X = F.shiftObj n X

theorem CategoryTheory.DGFunctor.shiftedFunctor_map {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) {X Y : C} (p : ℤ) (f : ↑((DGCategoryStruct.dgHom X Y).X p)) : ((F.shiftedFunctor n).map p) f = (n * p).negOnePow • (F.shiftWitness n X).shiftMap (F.shiftWitness n Y) p ((F.map p) f)

Not @[simp]: shiftedFunctor_obj rewrites the objects in this statement's own type, so its left-hand side is not in simp normal form. Use it with rw.

noncomputable def CategoryTheory.DGFunctor.shiftHom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : ↥(F.HomogeneousNatTrans (F.shiftedFunctor n) (-n))

The chosen shift elements assemble into a degree--n homogeneous dg natural transformation F ⟶ F[n].

Its graded naturality is the characterising square of shiftMap, with the functor's sign (-1)^(n p) cancelling the naturality sign (-1)^(-n p).

Equations

• F.shiftHom n = ⟨fun (X : C) => (F.shiftWitness n X).hom, ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.shiftHom_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : C) : HomogeneousNatTrans.app (F.shiftHom n) X = (F.shiftWitness n X).hom

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorWitness {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : IsShiftBy F n (F.shiftedFunctor n)

The shift of a dg functor is a shift in the dg category of dg functors.

Equations

• F.shiftedFunctorWitness n = { hom := F.shiftHom n, hom_closed := ⋯, bijective := ⋯ }

theorem CategoryTheory.DGFunctor.exists_shift_dgFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : ∃ (G : DGFunctor C D), Nonempty (IsShiftBy F n G)

Every dg functor has a shift in every degree, in the dg category of dg functors.

Shifting a degree-zero dg natural transformation

The associativity coherence below has to shift the comparison F[n][m] ⟶ F[n + m] once more. This is transport across the chosen shifts, pointwise. It is stated for every degree-zero homogeneous transformation; closed transformations remain closed, as recorded below.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.shiftedDegreeZero {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} (α : ↥(F.HomogeneousNatTrans G 0)) (n : ℤ) : ↥((F.shiftedFunctor n).HomogeneousNatTrans (G.shiftedFunctor n) 0)

Shift a degree-zero homogeneous dg natural transformation pointwise.

Naturality is IsShiftBy.shiftMap_comp: both sides are the transport of the original naturality square, with the common Koszul sign from the shifted functors.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.shiftedDegreeZero_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} (α : ↥(F.HomogeneousNatTrans G 0)) (n : ℤ) (X : C) : app (shiftedDegreeZero α n) X = (F.shiftWitness n X).shiftMap (G.shiftWitness n X) 0 (app α X)

The component of a pointwise shifted degree-zero transformation.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.shiftedDegreeZero_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (hα : IsClosed α) (n : ℤ) : IsClosed (shiftedDegreeZero α n)

Pointwise shifting preserves closed degree-zero transformations.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.shiftedDegreeZero_id {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : shiftedDegreeZero (id F) n = id (F.shiftedFunctor n)

Pointwise shifting takes the identity transformation to the identity.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.shiftedDegreeZero_comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G H : DGFunctor C D} (α : ↥(F.HomogeneousNatTrans G 0)) (β : ↥(G.HomogeneousNatTrans H 0)) (n : ℤ) : shiftedDegreeZero (((composition F G H 0 0 0 ⋯) α) β) n = ((composition (F.shiftedFunctor n) (G.shiftedFunctor n) (H.shiftedFunctor n) 0 0 0 ⋯) (shiftedDegreeZero α n)) (shiftedDegreeZero β n)

Pointwise shifting preserves vertical composition of degree-zero transformations.

Coherence of the shift in the degree

shiftedFunctor shifts by one integer. A shift functor also needs the two coherences: shifting by n and then by m agrees with shifting by n + m, and shifting by 0 changes nothing. Both hold up to a canonical isomorphism and not on the nose, because the shifted objects are chosen and two choices are only canonically isomorphic.

Both comparisons below are IsShiftBy.compare at every object. What has to be proved is that the objectwise comparison is natural, and that is IsShiftBy.shiftMap_compare together with IsShiftBy.comp'_shiftMap. The signs take care of themselves: the two composed shifts contribute (-1)^(m p) and (-1)^(n p), whose product is the (-1)^(r p) of the single shift because n p + m p = r p.

The additive comparison is associative as well. For three shifts, shiftedFunctorAdd_assoc identifies the path that first combines n and m with the path that first combines m and k, as degree-zero dg natural transformations rather than only after passing to H⁰.

noncomputable def CategoryTheory.DGFunctor.shiftWitnessComp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) (X : C) : IsShiftBy (F.obj X) r ((F.shiftedFunctor n).shiftObj m X)

The two chosen shift witnesses at one object, composed into a single witness for the total degree.

Equations

• F.shiftWitnessComp n m r h X = (F.shiftWitness n X).comp' ((F.shiftedFunctor n).shiftWitness m X) r h

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorAdd {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : ↥(((F.shiftedFunctor n).shiftedFunctor m).HomogeneousNatTrans (F.shiftedFunctor r) 0)

Shifting twice is shifting once, up to the canonical comparison.

The component is IsShiftBy.compare; naturality is IsShiftBy.comp'_shiftMap_smul followed by IsShiftBy.shiftMap_compare, and the two signs merge because n p + m p = r p.

Equations

• F.shiftedFunctorAdd n m r h = ⟨fun (X : C) => ((F.shiftWitness n X).comp' ((F.shiftedFunctor n).shiftWitness m X) r h).compare (F.shiftWitness r X), ⋯⟩

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorAddInv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : ↥((F.shiftedFunctor r).HomogeneousNatTrans ((F.shiftedFunctor n).shiftedFunctor m) 0)

The comparison in the other direction.

Equations

• F.shiftedFunctorAddInv n m r h = ⟨fun (X : C) => (F.shiftWitness r X).compare ((F.shiftWitness n X).comp' ((F.shiftedFunctor n).shiftWitness m X) r h), ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorAdd_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) (X : C) : HomogeneousNatTrans.app (F.shiftedFunctorAdd n m r h) X = (F.shiftWitnessComp n m r h X).compare (F.shiftWitness r X)

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorAddInv_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) (X : C) : HomogeneousNatTrans.app (F.shiftedFunctorAddInv n m r h) X = (F.shiftWitness r X).compare (F.shiftWitnessComp n m r h X)

Associativity of the additive comparison

For three shifts there are two composites of shiftedFunctorAdd. The left bracketing shifts the comparison F[n][m] ⟶ F[n + m] by k; the right bracketing first compares the last two shifts of F[n]. The theorem below says those two degree-zero dg natural transformations are equal, before passing to Z⁰ or H⁰.

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorAddAssocLeft {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m k nm r : ℤ) (hnm : n + m = nm) (hleft : nm + k = r) : ↥((((F.shiftedFunctor n).shiftedFunctor m).shiftedFunctor k).HomogeneousNatTrans (F.shiftedFunctor r) 0)

The left-associated composite from F[n][m][k] to F[r].

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorAddAssocRight {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m k mk r : ℤ) (hmk : m + k = mk) (hright : n + mk = r) : ↥((((F.shiftedFunctor n).shiftedFunctor m).shiftedFunctor k).HomogeneousNatTrans (F.shiftedFunctor r) 0)

The right-associated composite from F[n][m][k] to F[r].

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.DGFunctor.shiftedFunctorAdd_assoc {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m k nm mk r : ℤ) (hnm : n + m = nm) (hmk : m + k = mk) (hleft : nm + k = r) (hright : n + mk = r) : F.shiftedFunctorAddAssocLeft n m k nm r hnm hleft = F.shiftedFunctorAddAssocRight n m k mk r hmk hright

Associativity coherence for the shift of a dg functor.

The two composites of the canonical comparisons from F[n][m][k] to the chosen F[r] agree. Pointwise, both composites collapse by IsShiftBy.compare_trans; the only remaining equality is associativity of the three shift elements, IsShiftBy.comp'_assoc_hom.

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorZero {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) : ↥((F.shiftedFunctor 0).HomogeneousNatTrans F 0)

Shifting by zero changes nothing, up to the canonical comparison.

Equations

• F.shiftedFunctorZero = ⟨fun (X : C) => (F.shiftWitness 0 X).compare (CategoryTheory.IsShiftBy.self (F.obj X)), ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorZero_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (X : C) : HomogeneousNatTrans.app F.shiftedFunctorZero X = (F.shiftWitness 0 X).compare (IsShiftBy.self (F.obj X))

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorZeroInv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) : ↥(F.HomogeneousNatTrans (F.shiftedFunctor 0) 0)

The comparison from F to its shift by zero.

Equations

• F.shiftedFunctorZeroInv = ⟨fun (X : C) => (CategoryTheory.IsShiftBy.self (F.obj X)).compare (F.shiftWitness 0 X), ⋯⟩

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorZeroInv_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (X : C) : HomogeneousNatTrans.app F.shiftedFunctorZeroInv X = (IsShiftBy.self (F.obj X)).compare (F.shiftWitness 0 X)

Each comparison is closed, and each pair is mutually inverse. Together these say the two coherences are isomorphisms in the dg category of dg functors, not merely maps.

theorem CategoryTheory.DGFunctor.shiftedFunctorAdd_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : HomogeneousNatTrans.IsClosed (F.shiftedFunctorAdd n m r h)

theorem CategoryTheory.DGFunctor.shiftedFunctorAddInv_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : HomogeneousNatTrans.IsClosed (F.shiftedFunctorAddInv n m r h)

theorem CategoryTheory.DGFunctor.shiftedFunctorZero_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) : HomogeneousNatTrans.IsClosed F.shiftedFunctorZero

theorem CategoryTheory.DGFunctor.shiftedFunctorZeroInv_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) : HomogeneousNatTrans.IsClosed F.shiftedFunctorZeroInv

theorem CategoryTheory.DGFunctor.shiftedFunctorAdd_comp_inv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : ((HomogeneousNatTrans.composition ((F.shiftedFunctor n).shiftedFunctor m) (F.shiftedFunctor r) ((F.shiftedFunctor n).shiftedFunctor m) 0 0 0 ⋯) (F.shiftedFunctorAdd n m r h)) (F.shiftedFunctorAddInv n m r h) = HomogeneousNatTrans.id ((F.shiftedFunctor n).shiftedFunctor m)

theorem CategoryTheory.DGFunctor.shiftedFunctorAddInv_comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m r : ℤ) (h : n + m = r) : ((HomogeneousNatTrans.composition (F.shiftedFunctor r) ((F.shiftedFunctor n).shiftedFunctor m) (F.shiftedFunctor r) 0 0 0 ⋯) (F.shiftedFunctorAddInv n m r h)) (F.shiftedFunctorAdd n m r h) = HomogeneousNatTrans.id (F.shiftedFunctor r)

theorem CategoryTheory.DGFunctor.shiftedFunctorZero_comp_inv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) : ((HomogeneousNatTrans.composition (F.shiftedFunctor 0) F (F.shiftedFunctor 0) 0 0 0 ⋯) F.shiftedFunctorZero) F.shiftedFunctorZeroInv = HomogeneousNatTrans.id (F.shiftedFunctor 0)

theorem CategoryTheory.DGFunctor.shiftedFunctorZeroInv_comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) : ((HomogeneousNatTrans.composition F (F.shiftedFunctor 0) F 0 0 0 ⋯) F.shiftedFunctorZeroInv) F.shiftedFunctorZero = HomogeneousNatTrans.id F

instance CategoryTheory.DGFunctor.isPretriangulated_dgFunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] : IsPretriangulated (DGFunctor C D)

The dg category of dg functors is pretriangulated whenever the target is.

The zero object is the constant functor at one, the shift is the objectwise shift with the Koszul sign (-1)^(n p), and the cone is the objectwise cone assembled by ConeData. With this instance the twist candidate attached to a dg adjunction is a cone in a pretriangulated dg category, so its triangle is a triangle of functors in the sense Anno--Logvinenko use.