Documentation

DerivedAlgGeo.Algebra.Homology.DGCategory.AdjunctionH0

A dg adjunction is an adjunction on H⁰ #

DGAdjunction L R carries closed degree-zero unit and counit with the two triangle identities holding on the nose in the dg category. Each of those is exactly what an ordinary Adjunction between the induced functors on H⁰ asks for, once the components are read as homotopy classes.

This adapter is what makes the dg notion comparable with the rest of the library: RightAdjointKernelData and the Fourier--Mukai layer speak in Mathlib Adjunctions, and without DGAdjunction.h0 a dg adjunction could never be offered to them.

The two identifications are trivial, and that is the point #

H⁰ of the identity dg functor is the identity functor and H⁰ of a composite is the composite, both by isomorphisms whose components are identities (DGFunctor.h0IdIso, DGFunctor.h0CompIso). Conjugating by them changes no component, so the two triangle identities below reduce to DGAdjunction.left_triangle and DGAdjunction.right_triangle applied to a representative, with no homotopy and no sign.

The same comparison coherence normalizes a descended left-whiskered dg counit and a descended right-whiskered dg unit to ordinary whiskering of h0Counit and h0Unit, including the canonical functor associators and unitors. These laws are kept at the generic adjunction root so cone and twist consumers do not repeat the calculation.

What this does not say #

It does not say that a dg adjunction is more than an adjunction on H⁰, and it does not go the other way: an ordinary adjunction between H⁰ L and H⁰ R carries no dg unit or counit, and nothing here produces one. It also does not relate the strict dg notion to the homotopy adjunctions of Anno--Logvinenko, whose units and counits are quasi-isomorphisms of bimodules rather than closed degree-zero transformations; that comparison needs the Morita framework the roadmap lists as open.

source
noncomputable def CategoryTheory.DGAdjunction.h0Unit {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) :
Functor.id (H0 C) ⟶ L.h0.comp R.h0

The unit of a dg adjunction, read on H⁰.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CategoryTheory.DGAdjunction.h0Counit {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) :
    R.h0.comp L.h0 ⟶ Functor.id (H0 D)

    The counit of a dg adjunction, read on H⁰.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.DGAdjunction.h0Unit_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (X : H0 C) :
      A.h0Unit.app X = H0.homMk ⟨DGFunctor.HomogeneousNatTrans.app A.unit (H0.of C X), ⋯⟩
      source
      @[simp]
      theorem CategoryTheory.DGAdjunction.h0Counit_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) (Y : H0 D) :
      A.h0Counit.app Y = H0.homMk ⟨DGFunctor.HomogeneousNatTrans.app A.counit (H0.of D Y), ⋯⟩
      source
      theorem CategoryTheory.DGAdjunction.h0_whiskerLeft_counit {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} {E : Type u''} [DGCategory E] (A : DGAdjunction L R) (P : DGFunctor E D) :
      CategoryStruct.comp ((P.comp R).h0CompIso L).inv (DGFunctor.HomogeneousNatTrans.h0 (DGFunctor.HomogeneousNatTrans.whiskerLeft P A.counit) ⋯) = CategoryStruct.comp (Functor.whiskerRight (P.h0CompIso R).hom L.h0) (CategoryStruct.comp (P.h0.associator R.h0 L.h0).hom (CategoryStruct.comp (P.h0.whiskerLeft A.h0Counit) P.h0.rightUnitor.hom))

      Descending a left-whiskered dg counit is ordinary left whiskering of the H⁰ counit, after the canonical compositor, associator, and unitor comparisons. The leading inverse compositor presents the source as (P.h0 ⋙ R.h0) ⋙ L.h0.

      source
      theorem CategoryTheory.DGAdjunction.h0_whiskerRight_unit {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} {E : Type u''} [DGCategory E] (A : DGAdjunction L R) (P : DGFunctor C E) :
      CategoryStruct.comp (DGFunctor.HomogeneousNatTrans.h0 (DGFunctor.HomogeneousNatTrans.whiskerRight A.unit P) ⋯) (L.h0CompIso (R.comp P)).hom = CategoryStruct.comp P.h0.leftUnitor.inv (CategoryStruct.comp (Functor.whiskerRight A.h0Unit P.h0) (CategoryStruct.comp (L.h0.associator R.h0 P.h0).hom (L.h0.whiskerLeft (R.h0CompIso P).inv)))

      Descending a right-whiskered dg unit is ordinary right whiskering of the H⁰ unit, after the canonical unitor, associator, and compositor comparisons. The trailing compositor presents the target as L.h0 ⋙ (R.comp P).h0.

      source
      noncomputable def CategoryTheory.DGAdjunction.h0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) :
      L.h0 ⊣ R.h0

      A dg adjunction induces an adjunction on H⁰.

      The unit and counit are the descended dg transformations, and each triangle identity is the corresponding dg identity read on a representative.

      Equations
      • A.h0 = { unit := A.h0Unit, counit := A.h0Counit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
      Instances For
        source
        @[simp]
        theorem CategoryTheory.DGAdjunction.h0_unit {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) :
        A.h0.unit = A.h0Unit
        source
        @[simp]
        theorem CategoryTheory.DGAdjunction.h0_counit {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {L : DGFunctor C D} {R : DGFunctor D C} (A : DGAdjunction L R) :
        A.h0.counit = A.h0Counit