H⁰ of the dg category of dg functors, compared with ordinary functors

DGFunctor C D is itself a dg category, so H⁰ (DGFunctor C D) is an ordinary category: its objects are dg functors and its morphisms are closed degree-zero dg natural transformations up to homotopy. Separately, every dg functor has an H⁰ and every closed degree-zero transformation descends to one. This file says those two facts assemble into a functor

H⁰ (DGFunctor C D) ⥤ (H⁰ C ⥤ H⁰ D).

It also records the pseudofunctorial bookkeeping needed by consumers: strict vertical composition descends to ordinary composition, and dg left or right whiskering descends through the canonical h0CompIso compositors. These are equalities of natural transformations, so later cone and adjunction arguments do not need to repeat componentwise quotient calculations.

What the functor is, and what it is not

It is the comparison map, and it is the reason the dg functor category is worth having: without it, DGFunctor C D and H⁰ C ⥤ H⁰ D are two unrelated categories that happen to have related objects.

It is not claimed to be full, faithful, or essentially surjective, and none of the three is true in general. An ordinary natural transformation between the induced functors need not lift to a dg one, two dg transformations can descend to the same ordinary one without being homotopic in any recorded sense beyond the quotient's own, and an arbitrary functor H⁰ C ⥤ H⁰ D need not come from a dg functor at all. Making any of those precise is the Morita and quasi-functor theory the roadmap lists as open.

Homotopy invariance is the only content

Everything else is bookkeeping. The one step that has to be checked is that a morphism of H⁰ (DGFunctor C D) — a homotopy class — determines the induced ordinary transformation. It does, componentwise: if α - β = δ θ in the dg functor category then α X - β X = δ (θ X) in D, because the differential of the dg functor category is the pointwise one, so the two components agree in H⁰ D.

theorem CategoryTheory.DGFunctor.isClosed_of_mem_cocycles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {η : ↥(F.HomogeneousNatTrans G 0)} (hη : η ∈ cocycles F G) : HomogeneousNatTrans.IsClosed η

A degree-zero cocycle of the dg category of dg functors is a closed homogeneous natural transformation. The two say the same thing: the differential of DGFunctor C D is the pointwise one by definition.

theorem CategoryTheory.DGFunctor.mem_cocycles_of_isClosed {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {η : ↥(F.HomogeneousNatTrans G 0)} (hη : HomogeneousNatTrans.IsClosed η) : η ∈ cocycles F G

Conversely, a closed transformation is a cocycle.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.h0_comp {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G H : DGFunctor C D} (η : ↥(F.HomogeneousNatTrans G 0)) (θ : ↥(G.HomogeneousNatTrans H 0)) (hη : IsClosed η) (hθ : IsClosed θ) (hηθ : IsClosed (((composition F G H 0 0 0 ⋯) η) θ)) : h0 (((composition F G H 0 0 0 ⋯) η) θ) hηθ = CategoryStruct.comp (h0 η hη) (h0 θ hθ)

Descending a vertical composite is composing the descents.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.h0_comp' {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G H : DGFunctor C D} (η : ↥(F.HomogeneousNatTrans G 0)) (θ : ↥(G.HomogeneousNatTrans H 0)) (hη : IsClosed η) (hθ : IsClosed θ) (hηθ : IsClosed (comp η θ)) : h0 (comp η θ) hηθ = CategoryStruct.comp (h0 η hη) (h0 θ hθ)

Descending the strict vertical composite of homogeneous transformations is composition of their descents. This primed form targets the direct HomogeneousNatTrans.comp API; h0_comp targets its additive arbitrary-result-degree composition wrapper.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.h0_whiskerLeft {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {E : Type u''} [DGCategory E] (P : DGFunctor C D) {F G : DGFunctor D E} (η : ↥(F.HomogeneousNatTrans G 0)) (hη : IsClosed η) : h0 (whiskerLeft P η) ⋯ = CategoryStruct.comp (P.h0CompIso F).hom (CategoryStruct.comp (P.h0.whiskerLeft (h0 η hη)) (P.h0CompIso G).inv)

Descent to H⁰ commutes with dg left whiskering, through the canonical comparisons between H⁰ of a composite and the composite of H⁰ functors.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.h0_whiskerRight {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {E : Type u''} [DGCategory E] {F G : DGFunctor C D} (η : ↥(F.HomogeneousNatTrans G 0)) (hη : IsClosed η) (P : DGFunctor D E) : h0 (whiskerRight η P) ⋯ = CategoryStruct.comp (F.h0CompIso P).hom (CategoryStruct.comp (Functor.whiskerRight (h0 η hη) P.h0) (G.h0CompIso P).inv)

Descent to H⁰ commutes with dg right whiskering, through the canonical comparisons between H⁰ of a composite and the composite of H⁰ functors.

noncomputable def CategoryTheory.DGFunctor.h0Comparison (C : Type u) (D : Type u') [DGCategory C] [DGCategory D] : Functor (H0 (DGFunctor C D)) (Functor (H0 C) (H0 D))

The comparison functor.

An object of H⁰ (DGFunctor C D) is a dg functor, and it goes to the induced functor on H⁰. A morphism is a homotopy class of closed degree-zero dg natural transformations, and it goes to the ordinary transformation any representative descends to.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.h0Comparison_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : H0 (DGFunctor C D)) : (h0Comparison C D).obj F = (H0.of (DGFunctor C D) F).h0

@[simp]

theorem CategoryTheory.DGFunctor.h0Comparison_map_mk {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : H0 (DGFunctor C D)} (a : ↥(cocycles (H0.of (DGFunctor C D) F) (H0.of (DGFunctor C D) G))) : (h0Comparison C D).map ↑a = HomogeneousNatTrans.h0 ↑a ⋯

noncomputable def CategoryTheory.DGFunctor.h0Iso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : Z0 (DGFunctor C D)} (e : F ≅ G) : (Z0.of (DGFunctor C D) F).h0 ≅ (Z0.of (DGFunctor C D) G).h0

An isomorphism of dg functors in the closed degree-zero category descends to a natural isomorphism between their H⁰ functors. This is the image under the canonical composite Z⁰ → H⁰ → Fun(H⁰ C, H⁰ D).

Equations

• CategoryTheory.DGFunctor.h0Iso e = (CategoryTheory.DGFunctor.h0Comparison C D).mapIso ((CategoryTheory.Z0.toH0 (CategoryTheory.DGFunctor C D)).mapIso e)

@[simp]

theorem CategoryTheory.DGFunctor.h0Iso_hom {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : Z0 (DGFunctor C D)} (e : F ≅ G) : (h0Iso e).hom = HomogeneousNatTrans.h0 ↑e.hom ⋯

@[simp]

theorem CategoryTheory.DGFunctor.h0Iso_inv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : Z0 (DGFunctor C D)} (e : F ≅ G) : (h0Iso e).inv = HomogeneousNatTrans.h0 ↑e.inv ⋯

@[simp]

theorem CategoryTheory.DGFunctor.h0Iso_hom_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : Z0 (DGFunctor C D)} (e : F ≅ G) (X : H0 C) : ((h0Iso e).app X).hom = (HomogeneousNatTrans.h0 ↑e.hom ⋯).app X

@[simp]

theorem CategoryTheory.DGFunctor.h0Iso_inv_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : Z0 (DGFunctor C D)} (e : F ≅ G) (X : H0 C) : ((h0Iso e).app X).inv = (HomogeneousNatTrans.h0 ↑e.inv ⋯).app X

@[simp]

theorem CategoryTheory.DGFunctor.h0Iso_refl {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : Z0 (DGFunctor C D)) : h0Iso (Iso.refl F) = Iso.refl (Z0.of (DGFunctor C D) F).h0

theorem CategoryTheory.DGFunctor.h0Iso_trans {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G H : Z0 (DGFunctor C D)} (e : F ≅ G) (f : G ≅ H) : h0Iso (e ≪≫ f) = h0Iso e ≪≫ h0Iso f