Counit cones and twists of dg adjunctions

For a dg adjunction L ⊣ R, the twist-side endofunctor is the cone of the counit

L R ⟶ id_D.

This file is only the generic adjunction layer. It neither assumes that the result is an autoequivalence nor calls the adjunction spherical. Those are additional properties. Likewise, the usual cotwist is a shift of the cone of the unit id_C ⟶ R L; the unshifted unit cone is exposed here while a functorial dg shift is left as a separate capability.

@[reducible, inline]

abbrev CategoryTheory.DGAdjunction.CounitConeData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) : Type (max u' v)

Chosen objectwise cones of the adjunction counit.

Equations

• A.CounitConeData = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData A.counit

noncomputable def CategoryTheory.DGAdjunction.chosenCounitConeData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated D] : A.CounitConeData

A pretriangulated target supplies cones of all counit components.

Equations

• A.chosenCounitConeData = CategoryTheory.DGFunctor.HomogeneousNatTrans.chosenConeData A.counit ⋯

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGAdjunction.CounitConeData.twist {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (K : A.CounitConeData) : DGFunctor D D

The counit-cone dg endofunctor, i.e. the twist candidate associated to L ⊣ R.

Equations

• CategoryTheory.DGAdjunction.CounitConeData.twist A K = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functor K

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGAdjunction.CounitConeData.inclusion {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (K : A.CounitConeData) : ↥((DGFunctor.id D).HomogeneousNatTrans (twist A K) 0)

The canonical closed transformation id_D ⟶ twist.

Equations

• CategoryTheory.DGAdjunction.CounitConeData.inclusion A K = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inr K

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGAdjunction.CounitConeData.boundary {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (K : A.CounitConeData) : ↥((R.comp L).HomogeneousNatTrans (twist A K) (-1))

The degree--1 boundary transformation L R ⟶ twist.

Equations

• CategoryTheory.DGAdjunction.CounitConeData.boundary A K = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inl K

theorem CategoryTheory.DGAdjunction.CounitConeData.inclusion_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (K : A.CounitConeData) : DGFunctor.HomogeneousNatTrans.IsClosed (inclusion A K)

The twist inclusion is closed.

theorem CategoryTheory.DGAdjunction.CounitConeData.differential_boundary {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (K : A.CounitConeData) : DGFunctor.HomogeneousNatTrans.differential (boundary A K) = DGFunctor.HomogeneousNatTrans.comp A.counit (inclusion A K)

The differential of the twist boundary is the counit followed by the canonical inclusion.

@[reducible, inline]

abbrev CategoryTheory.DGAdjunction.UnitConeData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) : Type (max u v)

Chosen objectwise cones of the adjunction unit. The conventional cotwist is obtained from this cone by a shift by -1.

Equations

• A.UnitConeData = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData A.unit

noncomputable def CategoryTheory.DGAdjunction.chosenUnitConeData {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) [IsPretriangulated C] : A.UnitConeData

A pretriangulated source supplies cones of all unit components.

Equations

• A.chosenUnitConeData = CategoryTheory.DGFunctor.HomogeneousNatTrans.chosenConeData A.unit ⋯

@[reducible, inline]

noncomputable abbrev CategoryTheory.DGAdjunction.UnitConeData.unitCone {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (K : A.UnitConeData) : DGFunctor C C

The unshifted cone of the unit id_C ⟶ R L.

Equations

• CategoryTheory.DGAdjunction.UnitConeData.unitCone A K = CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.functor K