Degree-zero Hom cohomology in a scalar-linear dg category #
The degree-zero cohomology of a scalar-linear dg Hom-complex is the quotient of
closed degree-zero morphisms by boundaries. This file identifies that quotient
with the existing Hom-module in H⁰.
This comparison is intrinsic to a scalar-linear dg category: it does not use a pretriangulated structure or a selected shift.
noncomputable def
CategoryTheory.H0.homologyZeroLinearEquiv
{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]
(X Y : C)
:
↑(HomologicalComplex.homology (DGLinear.homComplex k X Y) 0) ≃ₗ[k] (have this := X;
this) ⟶ have this := Y;
this
Degree-zero cohomology of the scalar-linear dg Hom-complex is the Hom-module
of H⁰.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.H0.homologyZeroLinearEquiv_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]
(X Y : C)
(f : ↑((DGCategoryStruct.dgHom X Y).X 0))
(hf : (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Y).d 0 1)) f = 0)
:
(homologyZeroLinearEquiv X Y)
((ModuleCat.Hom.hom (HomologicalComplex.homologyπ (DGLinear.homComplex k X Y) 0))
(HomologicalComplex.cyclesMk (DGLinear.homComplex k X Y) f 1 ⋯ hf)) = homMk ⟨f, hf⟩
The degree-zero comparison sends the homology class represented by a
closed dg morphism to its class in H⁰.