Canonical adjunction comparison maps from dg cones

Let S : A ⟶ B have a left dg adjoint L and a right dg adjoint R. The counit cone of S ⊣ R and the unit cone of L ⊣ S determine the two standard comparison maps

L T[-1] ⟶ R and R ⟶ C L,

where T = Cone(S R ⟶ 𝟭) and C = Cone(𝟭 ⟶ R S). This file constructs their closed degree-zero dg representatives and their images in H⁰.

The H⁰ cotwist comparison is also factored through the ordinary adjunction unit and the descended cone inclusion. Its compositor, unitor, and associator terms come from the generic dg-adjunction descent interface; no second comparison map is introduced.

The first construction is why source-shift regrading is the right primitive: the closed degree-one projection T ⟶ S R becomes T[-1] ⟶ S R in degree zero before applying L. Thus no shift-preservation comparison for L is needed.

No invertibility is claimed here. Whether either induced H⁰ map is an isomorphism is additional spherical-functor data.

noncomputable def CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparison {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] : ↥((((twist rightAdj K).shiftedFunctor (-1)).comp L).HomogeneousNatTrans R 0)

The canonical comparison L T[-1] ⟶ R associated to the twist cone T = Cone(S R ⟶ 𝟭_B).

It is the degree-zero source regrading of the cone projection T ⟶ S R, postcomposed with L, followed by the counit L S ⟶ 𝟭_A evaluated after R.

Equations

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

theorem CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparison_app {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] (X : B) : DGFunctor.HomogeneousNatTrans.app (twistAdjointComparison leftAdj rightAdj K) X = ((DGCategoryStruct.dgComp 0 0 0 ⋯) ((L.map 0) (((DGCategoryStruct.dgComp (-1) 1 0 ⋯) ((twist rightAdj K).shiftWitness (-1) X).inv) (DGFunctor.HomogeneousNatTrans.app (DGFunctor.HomogeneousNatTrans.ConeData.fst K) X)))) (DGFunctor.HomogeneousNatTrans.app leftAdj.counit (R.obj X))

The objectwise formula for the twist adjunction comparison.

theorem CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparison_isClosed {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] : DGFunctor.HomogeneousNatTrans.IsClosed (twistAdjointComparison leftAdj rightAdj K)

The twist adjunction comparison is a closed degree-zero transformation.

noncomputable def CategoryTheory.DGAdjunction.CounitConeData.twistAdjointComparisonH0 {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] : (((twist rightAdj K).shiftedFunctor (-1)).comp L).h0 ⟶ R.h0

The twist adjunction comparison as an ordinary natural transformation on H⁰.

Equations

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

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparison {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) : ↥(R.HomogeneousNatTrans (L.comp (unitCone rightAdj K)) 0)

The canonical comparison R ⟶ C L associated to the unit cone C = Cone(𝟭_A ⟶ R S).

It is the unit 𝟭_B ⟶ S L postcomposed with R, followed by the target inclusion R S ⟶ C evaluated after L.

Equations

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

theorem CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparison_app {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) (X : B) : DGFunctor.HomogeneousNatTrans.app (cotwistAdjointComparison leftAdj rightAdj K) X = ((DGCategoryStruct.dgComp 0 0 0 ⋯) ((R.map 0) (DGFunctor.HomogeneousNatTrans.app leftAdj.unit X))) (DGFunctor.HomogeneousNatTrans.app (DGFunctor.HomogeneousNatTrans.ConeData.inr K) (L.obj X))

The objectwise formula for the cotwist adjunction comparison.

theorem CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparison_isClosed {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) : DGFunctor.HomogeneousNatTrans.IsClosed (cotwistAdjointComparison leftAdj rightAdj K)

The cotwist adjunction comparison is a closed degree-zero transformation.

noncomputable def CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparisonH0 {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) : R.h0 ⟶ (L.comp (unitCone rightAdj K)).h0

The cotwist adjunction comparison as an ordinary natural transformation on H⁰.

Equations

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

theorem CategoryTheory.DGAdjunction.UnitConeData.cotwistAdjointComparisonH0_eq_h0Unit_comp_inrH0 {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) : cotwistAdjointComparisonH0 leftAdj rightAdj K = CategoryStruct.comp R.h0.leftUnitor.inv (CategoryStruct.comp (Functor.whiskerRight leftAdj.h0Unit R.h0) (CategoryStruct.comp (L.h0.associator S.h0 R.h0).hom (CategoryStruct.comp (L.h0.whiskerLeft (S.h0CompIso R).inv) (CategoryStruct.comp (L.h0.whiskerLeft (DGFunctor.HomogeneousNatTrans.h0 (DGFunctor.HomogeneousNatTrans.ConeData.inr K) ⋯)) (L.h0CompIso (unitCone rightAdj K)).inv))))

The cotwist adjunction comparison factors through the ordinary H⁰ unit and the cone inclusion.

This is the unshifted comparison R ⟶ C L. The left unitor and associator put ordinary functor composition in the required order, and the two inverse compositors return to the strict dg composites before and after the descended cone inclusion.