The inverse-rotated first map of a dg cone triangle

For a closed degree-zero dg natural transformation α : F ⟶ G, its cone triangle has connecting map -fst into F[1]. Inverse rotation negates that map once more and shifts it by -1, so its first map is the degree-one cone projection fst, regraded to a closed degree-zero map Cone(α)[-1] ⟶ F.

This file records that identification as an equality of natural transformations. The source comparison is shiftedFunctorH0Iso: the dg functor shift and the pointwise shift on H⁰ are canonically isomorphic, not definitionally identified as functors. The shift cancellation used by inverse rotation is Mathlib's shiftFunctorCompIsoId, whose component computation is exposed by H0.shiftFunctorCompIsoId_hom_app.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inverseRotateFirstH0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (hα : IsClosed α) : K.functor.h0.comp (shiftFunctor (H0 D) (-1)) ⟶ F.h0

The first morphisms of the objectwise inverse-rotated cone triangles, assembled into a natural transformation.

Equations

• K.inverseRotateFirstH0 hα = { app := fun (X : CategoryTheory.H0 C) => (K.triangleObj hα (CategoryTheory.H0.of C X)).invRotate.mor₁, naturality := ⋯ }

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.shiftedFstH0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) : (K.functor.shiftedFunctor (-1)).h0 ⟶ F.h0

The closed degree-one cone projection, source-regraded to a degree-zero map out of the selected [-1] shift and descended to H⁰.

Equations

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

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.inverseRotateFirstH0_app_eq_shiftedFstH0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (hα : IsClosed α) (X : H0 C) : (K.inverseRotateFirstH0 hα).app X = K.shiftedFstH0.app X

Inverse rotation reads the cone projection through source regrading.

The cone triangle and inverse rotation each contribute one minus sign. After they cancel, the inverse-rotation shift comparison cancels the selected [1] witness in the connecting map, leaving the selected [-1] inverse followed by fst.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.ConeData.shiftedFstH0_eq {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {F G : DGFunctor C D} {α : ↥(F.HomogeneousNatTrans G 0)} (K : ConeData α) (hα : IsClosed α) : K.shiftedFstH0 = CategoryStruct.comp (K.functor.shiftedFunctorH0Iso (-1)).hom (K.inverseRotateFirstH0 hα)

The inverse-rotated first map is the H⁰ image of the regraded dg cone projection, after comparing the dg functor shift with the pointwise shift.