Documentation

DerivedAlgGeo.Algebra.Homology.DerivedCategory.HomComplexCohomologyLinear

Linear degree-zero class-to-derived comparison #

For a K-projective source in an R-linear abelian category, the existing additive comparison factors through the canonical class-to-homotopy equivalence and is R-linear. The class module instance is scoped; this is a comparison of Hom-sets, not an internal derived-Hom construction. The separate integer equivalence uses the canonical integer actions on both additive groups.

source
theorem CochainComplex.HomComplex.CohomologyClass.derivedCategoryHomAddEquiv_apply_eq {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K L : CochainComplex C ℤ) [K.IsKProjective] (x : CohomologyClass K L 0) :
(derivedCategoryHomAddEquiv K L) x = DerivedCategory.Qh.map ((cohomologyClassHomotopyAddEquiv K L) x)

The existing derived comparison is the canonical class-to-homotopy equivalence followed by Qh on morphisms.

source
noncomputable def CochainComplex.HomComplex.CohomologyClass.derivedCategoryHomLinearEquiv {R : Type u} [CommRing R] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [CategoryTheory.Linear R C] [HasDerivedCategory C] (K L : CochainComplex C ℤ) [K.IsKProjective] :
CohomologyClass K L 0 ≃ₗ[R] DerivedCategory.Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶ DerivedCategory.Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)

The degree-zero class-to-derived-Hom equivalence is linear for the scoped class-module action. Only the source is required to be K-projective.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def CochainComplex.HomComplex.CohomologyClass.derivedCategoryHomIntLinearEquiv {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (K L : CochainComplex C ℤ) [K.IsKProjective] :
    CohomologyClass K L 0 ≃ₗ[ℤ] DerivedCategory.Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶ DerivedCategory.Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)

    The same additive class-to-derived equivalence with the ordinary integer actions on both Hom groups. This does not use the scoped transported action.

    Equations
    Instances For