Hom cohomology as morphisms into selected shifts in H⁰ #
For a scalar-linear pretriangulated dg category, the explicit shift comparison
IsShiftBy.homologyLinearEquiv specializes to the object selected by the
existing HasShift (H0 C) ℤ instance. Thus
Hⁿ(dgHom X Y) ≃ₗ[k] Hom_{H⁰ C}(X, Y⟦n⟧).
The result asserts no finiteness, formality, Euler characteristic, or K₀
formula.
noncomputable def
CategoryTheory.H0.homologyShiftLinearEquiv
{k : Type w}
[CommRing k]
{C : Type u}
[DGCategory C]
[IsPretriangulated C]
[(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)]
[DGLinear k C]
(X Y : C)
(n : ℤ)
:
↑(HomologicalComplex.homology (DGLinear.homComplex k X Y) n) ≃ₗ[k] (have this := X;
this) ⟶ (CategoryTheory.shiftFunctor (H0 C) n).obj
(have this := Y;
this)
Cohomology of a scalar-linear dg Hom-complex as morphisms into the selected
shift in H⁰.