Hom cohomology and explicit dg shifts

For a scalar-linear dg category, an explicit witness s : IsShiftBy Y n Yn identifies degree-n cohomology of dgHom X Y with morphisms X ⟶ Yn in H⁰. The comparison uses the scalar-linear Hom-complex isomorphism induced by s, followed by Mathlib's homology comparison for shifted complexes.

This statement depends only on the supplied shift witness. Selecting shift objects functorially is a separate, pretriangulated enhancement layer.

noncomputable def CategoryTheory.IsShiftBy.homologyLinearEquiv {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {Y Yn : C} {n : ℤ} (s : IsShiftBy Y n Yn) (X : C) : ↑(HomologicalComplex.homology (DGLinear.homComplex k X Y) n) ≃ₗ[k] (have this := X; this) ⟶ have this := Yn; this

Cohomology of a scalar-linear dg Hom-complex as morphisms into an explicitly supplied target shift. The target is shifted by n, while the comparison of Hom-complexes is shifted by -n, so degree n becomes degree zero.

Equations

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

theorem CategoryTheory.IsShiftBy.homologyLinearEquiv_homologyπ_cyclesMk {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] {Y Yn : C} {n : ℤ} (s : IsShiftBy Y n Yn) (X : C) (f : ↑((DGCategoryStruct.dgHom X Y).X n)) (hf : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d n (n + 1))) f = 0) : (s.homologyLinearEquiv X) ((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (DGLinear.homComplex k X Y) n)) (HomologicalComplex.cyclesMk (DGLinear.homComplex k X Y) f (n + 1) ⋯ hf)) = H0.homMk ⟨((DGCategoryStruct.dgComp n (-n) 0 ⋯) f) s.hom, ⋯⟩

On a represented cohomology class, the explicit-shift comparison is right composition by the distinguished shift element.