Euler characteristic of a dg Hom-complex

The cohomology of a scalar-linear dg Hom-complex is the family of morphism spaces into the selected shifts in H⁰. Consequently Mathlib's junk-total homological Euler characteristic agrees with the repository's junk-total chiHom. No boundedness or finite-dimensionality hypothesis is needed for this equality.

theorem CategoryTheory.H0.homComplex_homologyEulerChar_eq_chiHom {k : Type w} [Field 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) : HomologicalComplex.homologyEulerChar (DGLinear.homComplex k X Y) = Triangulated.chiHom k (H0 C) (have this := X; this) (have this := Y; this)

The homological Euler characteristic of the dg Hom-complex is the Euler pairing of the corresponding objects of H⁰. Both sides retain their existing junk values on infinite support.