Regrading homogeneous dg natural transformations by a source shift

Shifting the source by n raises the degree of a homogeneous transformation from p to n + p. This file packages that operation as an additive equivalence, using the generic IsShiftBy.precompEquiv in the dg category of dg functors. In particular, a degree-p transformation F ⟶ G becomes a degree-zero transformation F[-p] ⟶ G.

The construction is one-sided on purpose. It changes the source by composing with the inverse shift element; it does not introduce another shift functor or another HasShift instance. The inverse composes with the selected shift element, and closedness is preserved and reflected.

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorWitness_inv_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : C) : HomogeneousNatTrans.app (F.shiftedFunctorWitness n).inv X = (F.shiftWitness n X).inv

The inverse selected by representability in the dg functor category is the pointwise inverse already selected in the target. This makes the abstract source regrading below compute through the original objectwise witnesses.

noncomputable def CategoryTheory.DGFunctor.HomogeneousNatTrans.sourceShiftEquiv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F G : DGFunctor C D) (n p q : ℤ) (h : n + p = q) : ↥(F.HomogeneousNatTrans G p) ≃+ ↥((F.shiftedFunctor n).HomogeneousNatTrans G q)

Regrade a homogeneous dg natural transformation by shifting its source. Forward transport is precomposition by the inverse shift element; inverse transport is precomposition by the shift element.

Equations

• CategoryTheory.DGFunctor.HomogeneousNatTrans.sourceShiftEquiv F G n p q h = (F.shiftedFunctorWitness n).precompEquiv G p q h

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.sourceShiftEquiv_apply_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F G : DGFunctor C D) (n p q : ℤ) (h : n + p = q) (α : ↥(F.HomogeneousNatTrans G p)) (X : C) : app ((sourceShiftEquiv F G n p q h) α) X = ((DGCategoryStruct.dgComp n p q h) (F.shiftWitness n X).inv) (app α X)

The forward source regrading, evaluated at an object.

@[simp]

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.sourceShiftEquiv_symm_apply_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F G : DGFunctor C D) (n p q : ℤ) (h : n + p = q) (β : ↥((F.shiftedFunctor n).HomogeneousNatTrans G q)) (X : C) : app ((sourceShiftEquiv F G n p q h).symm β) X = ((DGCategoryStruct.dgComp (-n) q p ⋯) (F.shiftWitness n X).hom) (app β X)

The inverse source regrading, evaluated at an object.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.differential_sourceShiftEquiv {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F G : DGFunctor C D) (n p q : ℤ) (h : n + p = q) (α : ↥(F.HomogeneousNatTrans G p)) : differential ((sourceShiftEquiv F G n p q h) α) = (sourceShiftEquiv F G n (p + 1) (q + 1) ⋯) (differential α)

Source-shift regrading commutes with the pointwise differential because the inverse shift element is closed and occurs on the left of the transformed component, where the surviving Leibniz term carries no sign.

theorem CategoryTheory.DGFunctor.HomogeneousNatTrans.sourceShiftEquiv_isClosed_iff {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F G : DGFunctor C D) (n p q : ℤ) (h : n + p = q) (α : ↥(F.HomogeneousNatTrans G p)) : IsClosed ((sourceShiftEquiv F G n p q h) α) ↔ IsClosed α

Source-shift regrading preserves and reflects closedness.