Finite cohomology presentations

This file packages the coefficient-side splitting input needed by finite cohomological constructions. For a complex K and a finite set of degrees s, finiteCohomologyModel K s is the finite biproduct of the homology objects of K, each placed in its own degree. A FiniteCohomologyPresentation K is an explicit homotopy equivalence from K to one such model.

The finite set is called degrees, not support: it may contain degrees in which homology vanishes. The presentation is data rather than a typeclass, because its chain maps and homotopies are noncanonical choices which later consumers use explicitly.

No formality theorem is asserted here. In particular, boundedness or finite dimensionality alone is not silently converted into a homotopy equivalence, and quasi-isomorphisms are not treated as homotopy equivalences. This file also does not mention dg copowers, Euler characteristics, or Grothendieck groups.

When homology vanishes away from the selected degrees, homologyModelIsoFiniteCohomologyModel identifies the full zero-differential homology model with this finite model. This is a categorical comparison, not a formality theorem for the original complex.

noncomputable def CochainComplex.finiteCohomologyModel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (degrees : Finset ℤ) : CochainComplex A ℤ

The finite zero-differential model formed from the homology objects of K in the specified degrees.

It is assembled from Mathlib's singleFunctor and finite biproduct rather than from a repository-owned shifted-sum construction.

Equations

• K.finiteCohomologyModel degrees = ⨁ fun (i : ↥degrees) => (CochainComplex.singleFunctor A ↑i).obj (HomologicalComplex.homology K ↑i)

noncomputable def CochainComplex.finiteCohomologyModelHomologyIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (degrees : Finset ℤ) (i : ℤ) : HomologicalComplex.homology (K.finiteCohomologyModel degrees) i ≅ ⨁ fun (j : ↥degrees) => HomologicalComplex.homology ((singleFunctor A ↑j).obj (HomologicalComplex.homology K ↑j)) i

Homology of the finite model is the finite biproduct of the homologies of its single summands. This is Mathlib's additive homology functor preserving a finite biproduct.

Equations

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

theorem CochainComplex.isZero_finiteCohomologyModel_X_of_not_mem {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (degrees : Finset ℤ) (i : ℤ) (hi : i ∉ degrees) : CategoryTheory.Limits.IsZero ((K.finiteCohomologyModel degrees).X i)

Away from the selected finite set, every degree of the finite cohomology model is a biproduct of zero objects.

@[simp]

theorem CochainComplex.finiteCohomologyModel_d {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (degrees : Finset ℤ) (i j : ℤ) : (K.finiteCohomologyModel degrees).d i j = 0

The finite cohomology model has zero differential.

noncomputable def CochainComplex.homologyModelIsoFiniteCohomologyModel {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (degrees : Finset ℤ) (hSupport : ∀ i ∉ degrees, CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)) : K.homologyModel ≅ K.finiteCohomologyModel degrees

If the homology of K vanishes away from degrees, its full zero-differential homology model is isomorphic to the existing finite cohomology model on degrees.

This comparison is categorical and does not assert that K itself is formal.

Equations

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

structure CochainComplex.FiniteCohomologyPresentation {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) : Type v

A chosen homotopy presentation of a complex by finitely many of its homology objects.

• degrees : Finset ℤ

  Degrees retained by the finite model. This need not be minimal.

• homotopyEquiv : HomotopyEquiv K (K.finiteCohomologyModel self.degrees)

  The chosen homotopy equivalence to the finite homology model.

noncomputable def CochainComplex.finiteCohomologyModelIsoShifted {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] (K : CochainComplex A ℤ) (degrees : Finset ℤ) : K.finiteCohomologyModel degrees ≅ ⨁ fun (i : ↥degrees) => (CategoryTheory.shiftFunctor (CochainComplex A ℤ) (-↑i)).obj ((singleFunctor A 0).obj (HomologicalComplex.homology K ↑i))

The finite homology model in its canonical shifted degree-zero form.

Mathlib's cochain convention is (K⟦n⟧).X p = K.X (p + n), so the single object in degree i is the degree-zero single shifted by -i. This normalization belongs to the model itself and requires no formality data.

Equations

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

noncomputable def CochainComplex.FiniteCohomologyPresentation.pullback {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {K L : CochainComplex A ℤ} (P : L.FiniteCohomologyPresentation) (e : HomotopyEquiv K L) : K.FiniteCohomologyPresentation

Pull a finite cohomology presentation back along a homotopy equivalence.

Equations

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

@[simp]

theorem CochainComplex.FiniteCohomologyPresentation.pullback_degrees {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {K L : CochainComplex A ℤ} (P : L.FiniteCohomologyPresentation) (e : HomotopyEquiv K L) : (P.pullback e).degrees = P.degrees

noncomputable def CochainComplex.FiniteCohomologyPresentation.homologyIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {K : CochainComplex A ℤ} (P : K.FiniteCohomologyPresentation) (i : ℤ) : HomologicalComplex.homology K i ≅ HomologicalComplex.homology (K.finiteCohomologyModel P.degrees) i

The presentation identifies the homology of K with that of its finite model.

Equations

• P.homologyIso i = P.homotopyEquiv.toHomologyIso i

theorem CochainComplex.FiniteCohomologyPresentation.isZero_homology_of_not_mem {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {K : CochainComplex A ℤ} (P : K.FiniteCohomologyPresentation) (i : ℤ) (hi : i ∉ P.degrees) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology K i)

A finite cohomology presentation forces homology to vanish outside its recorded finite set of degrees.

noncomputable def CochainComplex.FiniteCohomologyPresentation.shiftedHomotopyEquiv {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {K : CochainComplex A ℤ} (P : K.FiniteCohomologyPresentation) : HomotopyEquiv K (⨁ fun (i : ↥P.degrees) => (CategoryTheory.shiftFunctor (HomologicalComplex A (ComplexShape.up ℤ)) (-↑i)).obj ((singleFunctor A 0).obj (HomologicalComplex.homology K ↑i)))

A presentation also gives a homotopy equivalence directly to the shifted degree-zero normal form.

Equations

• P.shiftedHomotopyEquiv = P.homotopyEquiv.trans (HomotopyEquiv.ofIso (K.finiteCohomologyModelIsoShifted P.degrees))