Adjunctions of dg functors

This is the dg-enriched unit/counit presentation of an adjunction. The unit and counit are closed degree-zero homogeneous natural transformations and the two triangle identities hold before passage to H⁰.

The structure is intentionally independent of cones and triangulated categories. A counit cone is a downstream construction, not part of what an adjunction is.

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

A dg adjunction L ⊣ R, presented by closed degree-zero unit and counit transformations satisfying the triangle identities componentwise.

• unit : ↥((DGFunctor.id C).HomogeneousNatTrans (L.comp R) 0)

  The unit id_C ⟶ R L.

• counit : ↥((R.comp L).HomogeneousNatTrans (DGFunctor.id D) 0)

  The counit L R ⟶ id_D.

• unit_isClosed : DGFunctor.HomogeneousNatTrans.IsClosed self.unit

  The unit is closed.

• counit_isClosed : DGFunctor.HomogeneousNatTrans.IsClosed self.counit

  The counit is closed.

• left_triangle (X : C) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) ((L.map 0) (DGFunctor.HomogeneousNatTrans.app self.unit X))) (DGFunctor.HomogeneousNatTrans.app self.counit (L.obj X)) = DGCategoryStruct.dgId (L.obj X)

  The triangle identity on the left adjoint.

• right_triangle (Y : D) : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (DGFunctor.HomogeneousNatTrans.app self.unit (R.obj Y))) ((R.map 0) (DGFunctor.HomogeneousNatTrans.app self.counit Y)) = DGCategoryStruct.dgId (R.obj Y)

  The triangle identity on the right adjoint.

@[reducible, inline]

abbrev CategoryTheory.DGAdjunction.unitEndofunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} : DGFunctor C C

The endofunctor R L appearing as the source of the unit.

Equations

• CategoryTheory.DGAdjunction.unitEndofunctor = L.comp R

@[reducible, inline]

abbrev CategoryTheory.DGAdjunction.counitEndofunctor {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} : DGFunctor D D

The endofunctor L R appearing as the source of the counit.

Equations

• CategoryTheory.DGAdjunction.counitEndofunctor = R.comp L