Finite cohomology presentations for dg Hom-complexes

In a scalar-linear pretriangulated dg category with HomFiniteBounded H⁰, the cohomology of every dg Hom-complex is finite-dimensional and supported in finitely many degrees. Over the coefficient field, the general formality theorem therefore supplies a finite cohomology presentation automatically.

The selected degree set is the finite support already carried by HomFiniteBounded. This file does not assert naturality of the resulting presentations or exactness of any evaluation functor.

noncomputable def CategoryTheory.H0.homComplexCohomologyDegrees (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] [Triangulated.HomFiniteBounded k (H0 C)] (X Y : C) : Finset ℤ

The finite set of shifts on which the H⁰ Hom-space can have nonzero dimension.

Equations

• CategoryTheory.H0.homComplexCohomologyDegrees k X Y = ⋯.toFinset

theorem CategoryTheory.H0.isZero_homComplex_homology_of_not_mem (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] [Triangulated.HomFiniteBounded k (H0 C)] (X Y : C) (i : ℤ) (hi : i ∉ homComplexCohomologyDegrees k X Y) : Limits.IsZero (HomologicalComplex.homology (DGLinear.homComplex k X Y) i)

The homology of a dg Hom-complex vanishes away from the finite support selected by HomFiniteBounded.

noncomputable def CategoryTheory.H0.homComplexFiniteCohomologyPresentation (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] [Triangulated.HomFiniteBounded k (H0 C)] (X Y : C) : (DGLinear.homComplex k X Y).FiniteCohomologyPresentation

The canonical finite-support choice together with coefficient-side formality gives a finite cohomology presentation of every dg Hom-complex.

Equations

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