Presenting dg-adjunction cotwist triangles on ordinary categories #
The ordinary presentation of a dg adjunction unit gives a pointwise distinguished family
𝟭 X ⟶ F G ⟶ transportedUnitCone ⟶ (𝟭 X)⟦1⟧.
This file applies Mathlib's inverse rotation to obtain the conventional cotwist triangle
transportedCotwist ⟶ 𝟭 X ⟶ F G ⟶ transportedCotwist⟦1⟧,
where transportedCotwist is the pointwise [-1] shift of the transported
unit cone. It also compares this ordinary functor with the transport of the
actual shifted dg cone. The comparison reuses DGFunctor.shiftedFunctorH0Iso
and the source equivalence's CommShift structure.
The canonical pointwise shift and the generic transported-H⁰ package also
give an explicit CommShift and exactness result. Their comparison with the
actual shifted dg cone respects these canonical shift packages. An ordinary
autoequivalence is packaged only under the supplied hypothesis that the
unshifted cone is an equivalence on H⁰. No dg quasi-equivalence,
Fourier--Mukai comparison, choice independence, or sphericality is inferred.
Distinguishedness remains pointwise; this is not a distinguished triangle in
the functor category.
The actual shifted dg unit cone, after passing to H⁰ and transporting
through the ordinary source equivalence. No exactness is asserted.
Equations
- K.transportedDGCotwist eC = eC.inverse.comp (((CategoryTheory.DGAdjunction.UnitConeData.unitCone A K).shiftedFunctor (-1)).h0.comp eC.functor)
Instances For
The conventional ordinary cotwist associated to the transported unit
cone: its pointwise [-1] shift.
Equations
- K.transportedCotwist eC = (CategoryTheory.shiftFunctor (CategoryTheory.Functor X X) (-1)).obj (K.transportedUnitCone eC)
Instances For
Transporting the actual shifted dg unit cone agrees naturally with pointwise shifting the transported unshifted cone.
Equations
Instances For
The coherent shift comparison on the pointwise transported cotwist.
This is the composite of the generic transported-H⁰ comparison and the
canonical comparison on the ordinary shift functor.
Equations
Instances For
The comparison from the actual shifted dg unit cone to the conventional pointwise cotwist respects their canonical sign-correct shift packages.
Equivalence of the unshifted unit cone on H⁰ makes the conventional
transported cotwist an ordinary autoequivalence.
The ordinary autoequivalence presented by the conventional transported cotwist, under an explicit equivalence hypothesis on the unshifted cone.
Equations
- K.transportedCotwistEquivalence hK = ((CategoryTheory.DGAdjunction.UnitConeData.unitCone A K).transportedH0Equivalence eC eC hK).trans (CategoryTheory.shiftEquiv X (-1))
Instances For
The conventional transported cotwist is triangulated. Exactness of the shifted cone is unconditional in the cone choice; the ordinary comparison equivalence must be supplied as triangulated.
Under the explicit equivalence hypothesis, the transported cotwist equivalence carries Mathlib's canonical triangulated-equivalence package.
The inverse rotation of the presented unshifted unit triangle:
transportedCotwist ⟶ 𝟭 X ⟶ F G ⟶ transportedCotwist⟦1⟧.
Mathlib's invRotate owns the sign and the shift cancellation map.
Equations
Instances For
The first projection is strictly the pointwise-shifted transported unit cone.
The second projection is strictly the identity functor.
The third projection is strictly the presented adjunction composite.
At the natural-transformation level, inverse rotation moves the adjunction unit into the second map.
Every value of the conventional transported cotwist triangle is distinguished.