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.toShiftedHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {n : ℤ} [HasDerivedCategory C] (x : CohomologyClass K L n) : DerivedCategory.Q.obj K ⟶ DerivedCategory.Q.obj L⟦n⟧

This is the morphism Q.obj K ⟶ (Q.obj L)⟦n⟧ in the derived category that is attached to a class in CohomologyClass K L n.

Equations

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

@[simp]

theorem CochainComplex.HomComplex.CohomologyClass.toShiftedHom_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {K L : CochainComplex C ℤ} {n : ℤ} [HasDerivedCategory C] (y : Cocycle K L n) : (mk y).toShiftedHom = CategoryTheory.ShiftedHom.map (Cocycle.equivHomShift.symm y) DerivedCategory.Q

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) : CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) 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 x.

Equations

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

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) : (mk x).toSmallShiftedHom = CategoryTheory.Localization.SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) (Cocycle.equivHomShift.symm x)

@[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) : (CategoryTheory.Localization.SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q) (mk x).toSmallShiftedHom = CategoryTheory.ShiftedHom.map (Cocycle.equivHomShift.symm x) DerivedCategory.Q