Presenting a dg adjunction on ordinary categories #
A strict dg adjunction A : L ⊣ R induces A.h0 : L.h0 ⊣ R.h0. An
application usually does not use the literal homotopy categories, however: it
has equivalences H⁰ C ≌ X and H⁰ D ≌ Y, and names the transported
functors by ordinary functors F : X ⥤ Y and G : Y ⥤ X.
DGAdjunction.H0Presentation packages exactly those two functor
identifications. Its toAdjunction is obtained only by composing Mathlib
adjunctions and transporting along Mathlib natural isomorphisms. The
construction therefore introduces no second notion of transported
adjunction. The unit and counit accessors expose the comparison maps needed
by cone and kernel presentations downstream.
The category equivalences are arguments rather than Enhancements because
pretriangulated structure is irrelevant here. Taking them to be the
comparison equivalences of two enhancements is the intended principal use.
What this does not provide #
The functor isomorphisms are supplied data. In particular, this file does not show that a geometric functor has a dg lift, construct a Fourier--Mukai kernel, or turn an ordinary adjunction into a dg adjunction. Nor does it identify the transported adjunction with some independently chosen adjunction: that requires compatibility of units or counits, not merely the fact that the endpoint functors are isomorphic.
The left functor obtained from L.h0 by changing source and target along
the supplied category equivalences.
Equations
Instances For
The right functor obtained from R.h0 by changing source and target along
the supplied category equivalences. Its parentheses match the right adjoint
produced by two applications of Adjunction.comp.
Equations
Instances For
Transport the adjunction induced by a strict dg adjunction through two equivalences of ordinary categories.
This is the composite of eC.symm.toAdjunction, A.h0, and
eD.toAdjunction; all coherence is inherited from Mathlib's
Adjunction.comp.
Equations
- A.transportedH0 eC eD = (eC.symm.toAdjunction.comp A.h0).comp eD.toAdjunction
Instances For
Expand both Adjunction.comp steps in the transported unit, making the
original h0Unit visible between the source- and target-equivalence units.
Expand both Adjunction.comp steps in the transported counit, making the
original h0Counit visible between the source- and target-equivalence
counits.
Data presenting two dg functors, after passage to H⁰ and transport
through category equivalences, by named ordinary functors.
The data depends only on the endpoint functors. A particular adjunction
between them is supplied later to toAdjunction, so the same presentation may
be reused for more than one adjunction structure.
Identification of the transported left dg functor with its ordinary presentation.
Identification of the transported right dg functor with its ordinary presentation.
Instances For
The ordinary adjunction presented by P.
Mathlib first transports the composed H⁰ adjunction along leftIso, then
along rightIso.
Equations
- P.toAdjunction A = ((A.transportedH0 eC eD).ofNatIsoLeft P.leftIso).ofNatIsoRight P.rightIso
Instances For
The presented unit is the transported H⁰ unit followed by the two
stored functor comparisons.
The presented counit is the inverse right comparison, then the inverse
left comparison, followed by the transported H⁰ counit. This is the
normal form consumed by a counit-cone or counit-kernel presentation.
Pointwise normal form of the presented unit.
Pointwise normal form of the presented counit.