The dg shift of a functor computes the H⁰ shift

DGFunctor.shiftedFunctor shifts a dg functor by n, and H0.shiftFunctor shifts an object of H⁰ by n. Both are built from the same choice, namely IsPretriangulated.exists_shift, so they agree:

H⁰ (F[n]) = H⁰ F ⋙ (-)[n],

The object equality is rfl; the morphism equality is the second computation lemma below. The resulting functor equality and its natural-isomorphism wrapper make ordinary categorical properties such as equivalence and triangulatedness reusable for shifted dg functors.

Why it is not just rfl on morphisms

Two things differ, and both are harmless. The shifted functor carries the Koszul sign (-1)^(n p), which at the degree p = 0 of an H⁰ morphism is +1. And the shifted functor's action is IsShiftBy.shiftMap at degree zero, while the H⁰ shift's is IsShiftBy.mapShift; those are the same map, but shiftMap indexes its middle composite by n + 0 where mapShift uses n, and for a variable n that is only propositionally an equality. IsShiftBy.shiftMap_zero_eq_mapShift crosses it.

What this is for

It makes "the cotwist is the shift of the cone functor" a statement about the dg functor rather than only about each value: the first vertex of an inversely rotated cone triangle is Z⟦-1⟧ in H⁰, and by the object lemma below that is the value of the dg shifted functor.

The equality and natural isomorphism are categorical interfaces. The sign-correct CommShift and exactness packages below transport through that interface. The direct CommShift package obtained from the shifted dg functor is proved to agree with that transport, and the compatibility survives ordinary endpoint equivalences; the two computation lemmas remain available for strict objectwise formulas.

Opposite successive shifts are normalized by shiftedFunctorCompIsoIdH0. It applies Mathlib's shiftFunctorCompIsoId to the HasShift structure on closed dg functors and descends that isomorphism to H⁰, so the cancellation reuses the same unit and associativity laws.

theorem CategoryTheory.DGFunctor.shiftedFunctor_h0_obj {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : H0 C) : (F.shiftedFunctor n).h0.obj X = (shiftFunctor (H0 D) n).obj (F.h0.obj X)

On objects, the dg shifted functor is the H⁰ shift. Both choose the shifted object with IsPretriangulated.exists_shift, so this is rfl.

Not @[simp]: h0_obj and shiftedFunctor_obj both rewrite inside this statement's own left-hand side, so it is not in simp normal form. Use it with rw.

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctor_h0_map {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) {X Y : H0 C} (f : X ⟶ Y) : (F.shiftedFunctor n).h0.map f = (shiftFunctor (H0 D) n).map (F.h0.map f)

On morphisms too. The Koszul sign is +1 because an H⁰ morphism has degree zero, and the two transports agree by IsShiftBy.shiftMap_zero_eq_mapShift.

theorem CategoryTheory.DGFunctor.shiftedFunctor_h0_eq {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : (F.shiftedFunctor n).h0 = F.h0.comp (shiftFunctor (H0 D) n)

The object and morphism computations assemble into an equality of ordinary functors.

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorH0Iso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) : (F.shiftedFunctor n).h0 ≅ F.h0.comp (shiftFunctor (H0 D) n)

The dg shift computes the pointwise shift on H⁰, functorially.

This categorical interface packages shiftedFunctor_h0_eq as a natural isomorphism for consumers that should transport structure through isomorphism rather than rewrite functors.

Equations

• F.shiftedFunctorH0Iso n = CategoryTheory.eqToIso ⋯

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorCompIsoIdH0 {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n m : ℤ) (h : n + m = 0) : ((F.shiftedFunctor n).shiftedFunctor m).h0 ≅ F.h0

Opposite dg-functor shifts cancel canonically on H⁰.

This is Mathlib's shiftFunctorCompIsoId for the HasShift structure on closed dg functors, descended through DGFunctor.h0Iso. In particular, its coherence is inherited from the packaged zero and addition comparisons rather than reproved objectwise.

Equations

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

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorH0Iso_hom_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : H0 C) : (F.shiftedFunctorH0Iso n).hom.app X = CategoryStruct.id ((F.shiftedFunctor n).h0.obj X)

The comparison H⁰(F[n]) ≅ H⁰(F)[n] is the identity on each object; only its functorial typing records the morphism computation.

@[simp]

theorem CategoryTheory.DGFunctor.shiftedFunctorH0Iso_inv_app {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (X : H0 C) : (F.shiftedFunctorH0Iso n).inv.app X = CategoryStruct.id ((F.h0.comp (shiftFunctor (H0 D) n)).obj X)

The inverse comparison is likewise the identity on each object.

theorem CategoryTheory.DGFunctor.shiftedFunctorH0Iso_commShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] [IsPretriangulated C] (F : DGFunctor C D) (n : ℤ) : NatTrans.CommShift (F.shiftedFunctorH0Iso n).hom ℤ

The canonical comparison H⁰(F[n]) ≅ H⁰(F)[n] is compatible with the direct shift package on H⁰(F[n]), the canonical package on H⁰(F), and the Koszul-signed package on [n].

The source package is the one constructed directly from the shifted dg functor, rather than a package manufactured by transporting across this isomorphism.

noncomputable def CategoryTheory.DGFunctor.transportedShiftedFunctorH0Iso {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {X : Type uX} {Y : Type uY} [Category.{vX, uX} X] [Category.{vY, uY} Y] (F : DGFunctor C D) (n : ℤ) (eC : H0 C ≌ X) (eD : H0 D ≌ Y) [HasShift Y ℤ] [eD.functor.CommShift ℤ] : (eC.inverse.comp (F.shiftedFunctor n).h0).comp eD.functor ≅ ((eC.inverse.comp F.h0).comp eD.functor).comp (shiftFunctor Y n)

Transporting H⁰ of a shifted dg functor through ordinary equivalences agrees with transporting H⁰ first and then shifting in the target.

Only the forward target equivalence needs a shift comparison: the shift occurs after H⁰ F, so no CommShift structure is required on the source equivalence.

Equations

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

theorem CategoryTheory.DGFunctor.transportedShiftedFunctorH0Iso_commShift {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] {X : Type uX} {Y : Type uY} [Category.{vX, uX} X] [Category.{vY, uY} Y] (F : DGFunctor C D) (n : ℤ) (eC : H0 C ≌ X) (eD : H0 D ≌ Y) [IsPretriangulated C] [HasShift X ℤ] [HasShift Y ℤ] [eC.functor.CommShift ℤ] [eD.functor.CommShift ℤ] [Preadditive Y] [∀ (k : ℤ), (shiftFunctor Y k).Additive] [eD.functor.Additive] : NatTrans.CommShift (F.transportedShiftedFunctorH0Iso n eC eD).hom ℤ

The transported comparison H⁰(F[n]) ≅ H⁰(F)[n] respects the canonical shift packages at both endpoints and the Koszul-signed package on the final shift functor.

Additivity of the forward target equivalence is exactly what lets its shift comparison commute with the Koszul sign.

theorem CategoryTheory.DGFunctor.shiftedFunctor_h0_isEquivalence {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (hF : F.h0.IsEquivalence) : (F.shiftedFunctor n).h0.IsEquivalence

If H⁰ F is an equivalence, then so is H⁰ of every shifted dg functor.

This is only an ordinary categorical conclusion; it neither asserts that the shifted dg functor is a quasi-equivalence nor supplies triangulatedness.

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorH0Equivalence {C : Type u} {D : Type u'} [DGCategory C] [DGCategory D] [IsPretriangulated D] (F : DGFunctor C D) (n : ℤ) (hF : F.h0.IsEquivalence) : H0 C ≌ H0 D

The ordinary equivalence on H⁰ induced from an equivalence H⁰ F after shifting the dg functor.

Equations

• F.shiftedFunctorH0Equivalence n hF = (F.shiftedFunctor n).h0.asEquivalence

@[reducible]

noncomputable def CategoryTheory.DGFunctor.shiftedFunctorH0CommShift {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] [IsPretriangulated A] [IsPretriangulated B] (F : DGFunctor A B) (n : ℤ) (hF : F.PreservesShifts) : (F.shiftedFunctor n).h0.CommShift ℤ

The sign-correct shift comparison on H⁰ of a shifted dg functor.

It is obtained by composing the canonical comparison on H⁰(F) with the signed comparison on [n], then transporting that structure across shiftedFunctorH0Iso. The result is explicit rather than a global instance, so consumers control which shift comparison is in scope.

Equations

• F.shiftedFunctorH0CommShift n hF = CategoryTheory.Functor.CommShift.ofIso (F.shiftedFunctorH0Iso n).symm ℤ

theorem CategoryTheory.DGFunctor.shiftedFunctorH0IsTriangulated {A : Type u} {B : Type u'} [DGCategory A] [DGCategory B] [IsPretriangulated A] [IsPretriangulated B] (F : DGFunctor A B) (n : ℤ) (hShift : F.PreservesShifts) : (F.shiftedFunctor n).h0.IsTriangulated

A dg functor remains exact on H⁰ after every integral dg shift. The shift argument selects the comparison used by shiftedFunctorH0CommShift; cone preservation is automatic for every dg functor.

The proof composes the exact functor H⁰(F) with the sign-correct exact ordinary shift [n], then transports exactness across shiftedFunctorH0Iso.