H⁰ coherence and conventional shifted targets for dg-adjunction comparisons

For the twist comparison, this file first identifies the descended dg composite with the inverse-rotated first map, right-whiskered by the left adjoint and followed by the descended left counit. It then normalizes that last raw dg whisker to ordinary left whiskering of the H⁰ counit, with the canonical compositor, associator, and unitor. Both factorizations use generic descent coherence rather than an adjunction-specific comparison map.

The strict dg cone construction gives the cotwist comparison in the shift-free form

R ⟶ C L,

where C = Cone(𝟭 ⟶ R S). If the conventional cotwist is F = C[-1], Anno--Logvinenko write the target as (F L)[1]. These are canonically isomorphic, not definitionally equal: the two successive shifts [-1][1] must be cancelled.

This file performs that normalization through Mathlib's shiftFunctorCompIsoId, using the HasShift package on closed dg functors and then descending its component to H⁰. Thus the result inherits the packaged addition, zero, unit, and associativity coherence; no second comparison or paper-specific shift convention is introduced.

theorem CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparisonH0_eq_inverseRotateFirstH0 {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (leftAdj : DGAdjunction L S) (rightAdj : DGAdjunction S R) (K : rightAdj.CounitConeData) [IsPretriangulated B] : twistAdjointComparisonH0 leftAdj rightAdj K = CategoryStruct.comp (((twist rightAdj K).shiftedFunctor (-1)).h0CompIso L).hom (CategoryStruct.comp (Functor.whiskerRight (CategoryStruct.comp ((twist rightAdj K).shiftedFunctorH0Iso (-1)).hom (DGFunctor.HomogeneousNatTrans.ConeData.inverseRotateFirstH0 K ⋯)) L.h0) (CategoryStruct.comp ((R.comp S).h0CompIso L).inv (DGFunctor.HomogeneousNatTrans.h0 (DGFunctor.HomogeneousNatTrans.whiskerLeft R leftAdj.counit) ⋯)))

The twist adjunction comparison factors through inverse rotation.

The descended dg comparison is the first map of the inverse-rotated twist triangle, postcomposed with L, followed by the descended left-counit whisker. The two h0CompIso terms are the canonical compositor needed to pass between H⁰ of a dg composite and the composite of its H⁰ functors.

theorem CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparisonH0_eq_inverseRotateFirstH0_comp_h0Counit {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (leftAdj : DGAdjunction L S) (rightAdj : DGAdjunction S R) (K : rightAdj.CounitConeData) [IsPretriangulated B] : twistAdjointComparisonH0 leftAdj rightAdj K = CategoryStruct.comp (((twist rightAdj K).shiftedFunctor (-1)).h0CompIso L).hom (CategoryStruct.comp (Functor.whiskerRight (CategoryStruct.comp ((twist rightAdj K).shiftedFunctorH0Iso (-1)).hom (DGFunctor.HomogeneousNatTrans.ConeData.inverseRotateFirstH0 K ⋯)) L.h0) (CategoryStruct.comp (Functor.whiskerRight (R.h0CompIso S).hom L.h0) (CategoryStruct.comp (R.h0.associator S.h0 L.h0).hom (CategoryStruct.comp (R.h0.whiskerLeft leftAdj.h0Counit) R.h0.rightUnitor.hom))))

The twist adjunction comparison factors through the ordinary H⁰ counit.

This is the fully normalized form of twistAdjointComparisonH0_eq_inverseRotateFirstH0: the terminal descended dg whisker has been replaced by ordinary left whiskering of leftAdj.h0Counit. The remaining compositor, associator, and unitor are precisely the canonical comparison from strict dg composition to ordinary functor composition.

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparisonShiftedH0 {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (leftAdj : DGAdjunction L S) (rightAdj : DGAdjunction S R) (K : rightAdj.UnitConeData) [IsPretriangulated A] : R.h0 ⟶ ((L.comp ((unitCone rightAdj K).shiftedFunctor (-1))).shiftedFunctor 1).h0

The canonical comparison with the conventional cotwist target (C[-1] L)[1].

It is the shift-free map R ⟶ C L, followed by the inverse of the canonical cancellation (C L)[-1][1] ≅ C L.

Equations

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

theorem CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparisonShiftedH0_eq {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] {S : DGFunctor A B} {L R : DGFunctor B A} (leftAdj : DGAdjunction L S) (rightAdj : DGAdjunction S R) (K : rightAdj.UnitConeData) [IsPretriangulated A] : cotwistAdjointComparisonShiftedH0 leftAdj rightAdj K = CategoryStruct.comp (cotwistAdjointComparisonH0 leftAdj rightAdj K) ((L.comp (unitCone rightAdj K)).shiftedFunctorCompIsoIdH0 (-1) 1 ⋯).inv

The conventional cotwist comparison is the shift-free comparison followed by the canonical opposite-shift cancellation.