The model shift is Mathlib's shift

Cdg.isShiftBy K n exhibits K⟦n⟧ as a shift of K in the dg sense: the witness is the canonical closed cochain Cdg.shiftCocycle K n of degree -n, and nothing about HasShift (CochainComplex A ℤ) ℤ enters that statement. This file proves that the dg notion really does restrict to the categorical one, in the three forms dg-enhancements-e7 needs before Functor.CommShift can be built for the seam:

• Cdg.mapShift_isShiftBy -- the dg action of the shift on a morphism is φ ↦ φ⟦n⟧';
• Cdg.shiftCocycle_zero -- the degree-0 witness is shiftFunctorZero;
• Cdg.comp_shiftCocycle -- composing the witnesses for a and b is the witness for a + b, corrected by shiftFunctorAdd.

The last two are exactly the two coherence identities a CommShift structure asks for, transcribed into the dg model. That they hold on the nose, with no sign, is because Cochain.rightShift carries none: the Koszul sign of the shift lives on Cochain.leftShift, which shifts the source of a cochain, and shiftCocycle shifts the target.

Why the work is done on CochainComplex A ℤ and transferred afterwards

Cdg A is a type synonym for CochainComplex A ℤ and Cdg.of is the identity, so of A (shiftObj K a) and (of A K)⟦a⟧ are the same term -- but only after unfolding two definitions, which rw will not do while it builds a motive. A component computation phrased on Cdg therefore produces goals that are ill-typed at instances transparency and no rewrite fires.

rightShift_id_zero and rightShift_id_comp are consequently stated on plain cochain complexes, where every object is one opaque term, and the Cdg-level statements are read off them by term elaboration, which crosses the synonym where tactic matching does not.

Everything is XIsoOfEq, and that is the point

Each identity is, degreewise, an equality between composites of identity-like maps between components indexed by integers that omega proves equal. There is no homological content here; the content is that the two indexings agree, which is what makes the seam's shift comparison exist at all.

On plain cochain complexes

theorem CategoryTheory.Cdg.rightShift_id_zero {A : Type u} [Category.{v, u} A] [Preadditive A] (K : CochainComplex A ℤ) : (CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id K)).rightShift 0 (-0) ⋯ = CochainComplex.HomComplex.Cochain.ofHom ((shiftFunctorZero (CochainComplex A ℤ) ℤ).inv.app K)

The degree-zero canonical cochain is shiftFunctorZero. Stated on a plain cochain complex; Cdg.shiftCocycle_zero is the same statement read on C^dg.

theorem CategoryTheory.Cdg.rightShift_id_comp {A : Type u} [Category.{v, u} A] [Preadditive A] (K : CochainComplex A ℤ) (a b : ℤ) : ((CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id K)).rightShift a (-a) ⋯).comp ((CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id ((shiftFunctor (CochainComplex A ℤ) a).obj K))).rightShift b (-b) ⋯) ⋯ = ((CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id K)).rightShift (a + b) (-(a + b)) ⋯).comp (CochainComplex.HomComplex.Cochain.ofHom (have this := (shiftFunctorAdd (CochainComplex A ℤ) a b).hom.app K; this)) ⋯

The canonical cochains compose, up to shiftFunctorAdd. Stated on a plain cochain complex; Cdg.comp_shiftCocycle is the same statement read on C^dg.

The type ascription on the second factor of the right-hand side is load-bearing: without it that composite's target elaborates as (shiftFunctor a ⋙ shiftFunctor b).obj K while the left-hand side's is (shiftFunctor b).obj ((shiftFunctor a).obj K), and the two -- definitionally equal -- forms block every rewrite.

theorem CategoryTheory.Cdg.comp_shiftCocycle_id {A : Type u} [Category.{v, u} A] [Preadditive A] {M N : CochainComplex A ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain M N n) (a n' : ℤ) (hn' : n' + a = n) : γ.comp ((CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id N)).rightShift a (-a) ⋯) ⋯ = γ.rightShift a n' hn'

Right composition with the canonical shift cochain is Cochain.rightShift.

On C^dg

theorem CategoryTheory.Cdg.shiftCocycle_v {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (n p q : ℤ) (hpq : p + -n = q) : (↑(K.shiftCocycle n)).v p q hpq = eqToHom ⋯

The canonical shift cochain, degreewise: the identity-like map from K in degree p to K⟦n⟧ in degree q, where q + n = p.

theorem CategoryTheory.Cdg.mapShift_isShiftBy {A : Type u} [Category.{v, u} A] [Preadditive A] {K L : Cdg A} (n : ℤ) (φ : of A K ⟶ of A L) : (K.isShiftBy n).mapShift (L.isShiftBy n) (CochainComplex.HomComplex.Cochain.ofHom φ) = CochainComplex.HomComplex.Cochain.ofHom ((shiftFunctor (CochainComplex A ℤ) n).map φ)

The dg shift acts on morphisms as ⟦n⟧'. mapShift is built from IsShiftBy.inv, which is Classical.choice; IsShiftBy.mapShift_unique reduces the identification to the naturality square of shiftCocycle, and that is degreewise an equality of two identity maps.

theorem CategoryTheory.Cdg.shiftCocycle_zero {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) : ↑(K.shiftCocycle 0) = CochainComplex.HomComplex.Cochain.ofHom ((shiftFunctorZero (CochainComplex A ℤ) ℤ).inv.app (of A K))

The degree-zero witness is shiftFunctorZero.

theorem CategoryTheory.Cdg.comp_shiftCocycle {A : Type u} [Category.{v, u} A] [Preadditive A] (K : Cdg A) (a b : ℤ) : (↑(K.shiftCocycle a)).comp ↑((K.shiftObj a).shiftCocycle b) ⋯ = (↑(K.shiftCocycle (a + b))).comp (CochainComplex.HomComplex.Cochain.ofHom ((shiftFunctorAdd (CochainComplex A ℤ) a b).hom.app (of A K))) ⋯

The witnesses compose, up to shiftFunctorAdd. Composing the witness for a with the witness for b on K⟦a⟧ is the witness for a + b, followed by Mathlib's comparison K⟦a + b⟧ ≅ (K⟦a⟧)⟦b⟧.