Documentation

DerivedAlgGeo.Algebra.Homology.Homotopy.FiniteCohomologyPresentationOfSupport

Finite cohomology presentations from finite support #

Over a division ring, this file composes the generic finite-support comparison between zero-differential homology models with the noncanonical formality equivalence to construct a FiniteCohomologyPresentation.

The support witness is explicit and the recorded finite set need not be minimal. No boundedness, finite-dimensionality, naturality, or quasi-isomorphism invariance is inferred.

source
noncomputable def CochainComplex.FiniteCohomologyPresentation.ofFiniteSupport {k : Type u} [DivisionRing k] (K : CochainComplex (ModuleCat k) ℤ) (degrees : Finset ℤ) (hSupport : ∀ i ∉ degrees, CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)) :
K.FiniteCohomologyPresentation

A finite-support witness constructs a finite cohomology presentation for a complex of vector spaces. The underlying formality equivalence remains noncanonical; the finite-support comparison itself uses only the categorical zero-differential models.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CochainComplex.FiniteCohomologyPresentation.ofFiniteSupport_degrees {k : Type u} [DivisionRing k] (K : CochainComplex (ModuleCat k) ℤ) (degrees : Finset ℤ) (hSupport : ∀ i ∉ degrees, CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)) :
    (ofFiniteSupport K degrees hSupport).degrees = degrees