Documentation

DerivedAlgGeo.Algebra.Homology.DGCategory.NaturalTransformationH0

Closed degree-zero dg natural transformations in H⁰ #

A closed homogeneous dg natural transformation of degree zero has closed components, so each of them represents a morphism of H⁰, and its graded naturality at degree zero carries no sign. What comes out is an ordinary natural transformation H⁰ F ⟶ H⁰ G.

This is the adapter that lets dg-level data be compared with ordinary categorical data at all: without it a DGAdjunction and a Mathlib Adjunction on H⁰ are two unrelated structures.

Only degree zero, and only closed #

Both hypotheses are used and neither can be dropped. A transformation of degree n ≠ 0 has components in the wrong group to be a morphism of H⁰, and an unclosed degree-zero one has components that are not cocycles. The sign in graded naturality is (-1)^(n * p), which is +1 exactly because both n and the degree p of the morphism being transported are zero here; a degree-n version would have to land in a shifted Hom, which is the functorial-shift capability the roadmap still lists as open.

source
theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.IsClosed.app_mem_cocycles {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (hα : IsClosed α) (X : C) :
app α X ∈ cocycles (F.obj X) (G.obj X)

A closed dg natural transformation has closed components.

source
def CategoryTheory.DGFunctor.HomogeneousNatTrans.h0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} (α : ↥(F.HomogeneousNatTrans G 0)) (hα : IsClosed α) :
F.h0 ⟶ G.h0

A closed degree-zero dg natural transformation descends to H⁰.

The components are the classes of the dg components; naturality is graded naturality at degree zero, where the Koszul sign is +1.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.h0_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] {F G : DGFunctor C D} (α : ↥(F.HomogeneousNatTrans G 0)) (hα : IsClosed α) (X : H0 C) :
    (h0 α hα).app X = H0.homMk ⟨app α (H0.of C X), ⋯⟩
    source
    @[simp]
    theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.h0_id {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) (hF : IsClosed (id F)) :
    h0 (id F) hF = CategoryStruct.id F.h0

    The identity dg natural transformation descends to the identity.

    source
    theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.isClosed_id {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] (F : DGFunctor C D) :
    IsClosed (id F)

    The identity dg natural transformation is closed.