IsShiftBy really is a shift of hom-complexes

Pretriangulated.lean says, in prose, that Y is a shift of X by n when dgHom W Y ≅ (dgHom W X)⟦n⟧ naturally in W. What IsShiftBy actually carries is weaker on its face: a closed element ε of degree -n such that right composition with it is bijective in each degree. Degreewise bijections are not an isomorphism of complexes, so the sentence is a gloss until someone supplies the differentials.

This file supplies them, and the point is that the Koszul sign is what makes it work. Leibniz gives

δ (f · ε) = f · (δ ε) + (-1) ^ (-n) • (δ f) · ε

and ε is closed, so δ (f · ε) = (-1) ^ (-n) • (δ f) · ε. Right composition with ε therefore does not commute with the differentials — it commutes with them up to (-1) ^ (-n). That is exactly the sign shiftD carries, so compRight is a map of complexes into the shifted hom-complex and into no other. The two (-1) ^ (-n) cancel because a unit squares to one, which is the whole proof of compRight_comm.

So Shift.lean's sign is not decoration on a definition: it is what makes IsShiftBy's degreewise data assemble into the isomorphism its docstring claims.

theorem CategoryTheory.compRight_comm {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} {ε : ↑((DGCategoryStruct.dgHom X Y).X (-n))} (hε : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d (-n) (-n + 1))) ε = 0) (W : C) (p p' q q' : ℤ) (hq : p + -n = q) (hq' : p' + -n = q') (hp : p + 1 = p') (f : ↑((DGCategoryStruct.dgHom W X).X p)) : (DGCategory.shiftD (-n) q q') ((compRight W ε p q hq) f) = (compRight W ε p' q' hq') ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom W X).d p p')) f)

Right composition with a closed element of degree -n is a map of complexes into the (-n)-shifted hom-complex. It is not a map into the unshifted one: Leibniz leaves a factor (-1) ^ (-n), and shiftD (-n) is where that factor is absorbed.

noncomputable def CategoryTheory.IsShiftBy.homMap {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (h : IsShiftBy X n Y) (W : C) : DGCategoryStruct.dgHom W X ⟶ (shiftFunctor (CochainComplex AddCommGrpCat ℤ) (-n)).obj (DGCategoryStruct.dgHom W Y)

The morphism of complexes underlying IsShiftBy: right composition with the structure element, landing in the shifted hom-complex.

Equations

• h.homMap W = { f := fun (p : ℤ) => AddCommGrpCat.ofHom (CategoryTheory.compRight W h.hom p (p + -n) ⋯), comm' := ⋯ }

theorem CategoryTheory.IsShiftBy.bijective_homMap {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (h : IsShiftBy X n Y) (W : C) (p : ℤ) : Function.Bijective ⇑(AddCommGrpCat.Hom.hom ((h.homMap W).f p))

Each component of IsShiftBy.homMap is bijective — this is the structure's own bijective field, restated at the degree the shifted complex uses.

noncomputable def CategoryTheory.IsShiftBy.homIso {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (h : IsShiftBy X n Y) (W : C) : DGCategoryStruct.dgHom W X ≅ (shiftFunctor (CochainComplex AddCommGrpCat ℤ) (-n)).obj (DGCategoryStruct.dgHom W Y)

The Hom-complex comparison represented by a chosen dg shift.

This is the categorical form of the degreewise bijectivity stored in IsShiftBy: homMap already supplies compatibility with the differentials, and its components are isomorphisms by bijective_homMap.

Equations

• h.homIso W = HomologicalComplex.Hom.isoOfComponents (fun (p : ℤ) => CategoryTheory.asIso ((h.homMap W).f p)) ⋯

@[simp]

theorem CategoryTheory.IsShiftBy.homIso_hom_f_apply {C : Type u} [DGCategory C] {X Y : C} {n : ℤ} (h : IsShiftBy X n Y) (W : C) (p : ℤ) (f : ↑((DGCategoryStruct.dgHom W X).X p)) : (AddCommGrpCat.Hom.hom ((h.homIso W).hom.f p)) f = ((DGCategoryStruct.dgComp p (-n) (p + -n) ⋯) f) h.hom