Cohomology of HomComplex and morphisms in the derived category #
Let K and L be two cochain complexes in an abelian category C.
Given a class x : HomComplex.CohomologyClass K L n, we construct an
element in the type
SmallShiftedHom (HomologicalComplex.quasiIso C (.up ℤ)) K L n, and
compute its image as a morphism Q.obj K ⟶ (Q.obj L)⟦n⟧ in the
derived category when x is given as the class of a cocycle.
noncomputable def
CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{K L : CochainComplex C ℤ}
{n : ℤ}
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
(x : CohomologyClass K L n)
:
Given x : CohomologyClass K L n, this is the element in the type
SmallShiftedHom relatively to quasi-isomorphisms that is associated
to the x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{K L : CochainComplex C ℤ}
{n : ℤ}
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
(x : Cocycle K L n)
:
@[simp]
theorem
CochainComplex.HomComplex.CohomologyClass.equiv_toSmallShiftedHom_mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
{K L : CochainComplex C ℤ}
{n : ℤ}
[CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
[HasDerivedCategory C]
(x : Cocycle K L n)
: