Documentation

DerivedAlgGeo.Algebra.Homology.HomotopyCategory.HomComplexSingle

Hom complexes from a degree-zero single object #

For an arbitrary integer-indexed cochain complex, the Hom complex from a degree-zero single object is the degreewise additive coyoneda functor. The comparison includes the incoming degree-minus-one boundary; it does not replace cohomology by the outgoing kernel. A represented additive functor inherits the same comparison, including its degree-zero homology.

This is a generic Hom-complex extension. No affine, quasicoherent, boundedness, or injectivity hypothesis is used.

Main definitions #

Main results #

The isomorphism identifies the full Hom complex, and the additive equivalence identifies cohomology in every integer degree with represented degreewise homology. The degree-zero result is a specialization.

Implementation notes #

Mathlib's fromSingleEquiv supplies each component. Its formula for the Hom-complex differential proves compatibility without a support bound.

References #

Mathlib HomComplexSingle.lean and Preadditive/Yoneda/Basic.lean at pin 520045ab14e26149ee970e2e617ca04b09bde5d6.

Tags #

Hom complex, additive coyoneda, represented functor, cohomology

source
noncomputable def CochainComplex.HomComplex.singleCoyonedaIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (K : CochainComplex C ℤ) :
((singleFunctor C 0).obj X).HomComplex K ≅ ((CategoryTheory.preadditiveCoyoneda.obj (Opposite.op X)).mapHomologicalComplex (ComplexShape.up ℤ)).obj K

The Hom complex from a degree-zero single object is the additive coyoneda functor applied degreewise. The component maps are Mathlib's Cochain.fromSingleEquiv; Cochain.δ_fromSingleMk supplies differential compatibility at every integer degree.

Equations
Instances For
    source
    noncomputable def CochainComplex.HomComplex.singleRepresentedIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (F : CategoryTheory.Functor C AddCommGrpCat) [F.PreservesZeroMorphisms] (e : CategoryTheory.preadditiveCoyoneda.obj (Opposite.op X) ≅ F) (K : CochainComplex C ℤ) :
    ((singleFunctor C 0).obj X).HomComplex K ≅ (F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K

    Specialize singleCoyonedaIso along a supplied representation of a zero-morphism-preserving functor. The representation is a natural isomorphism of functors; the complex comparison does not require a separate additivity or exactness hypothesis.

    Equations
    Instances For
      source
      noncomputable def CochainComplex.HomComplex.singleRepresentedHomologyAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (F : CategoryTheory.Functor C AddCommGrpCat) [F.PreservesZeroMorphisms] (e : CategoryTheory.preadditiveCoyoneda.obj (Opposite.op X) ≅ F) (K : CochainComplex C ℤ) (n : ℤ) :
      CohomologyClass ((singleFunctor C 0).obj X) K n ≃+ ↑(((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homology n)

      Degree-n classes in the Hom complex are degree-n homology of any represented zero-morphism-preserving functor applied degreewise. In particular, the quotient retains boundaries from degree n - 1.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def CochainComplex.HomComplex.singleRepresentedHomologyZeroAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] (X : C) (F : CategoryTheory.Functor C AddCommGrpCat) [F.PreservesZeroMorphisms] (e : CategoryTheory.preadditiveCoyoneda.obj (Opposite.op X) ≅ F) (K : CochainComplex C ℤ) :
        CohomologyClass ((singleFunctor C 0).obj X) K 0 ≃+ ↑(((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homology 0)

        Degree-zero specialization of singleRepresentedHomologyAddEquiv.

        Equations
        Instances For