Finite cohomology presentations of scalar-linear copowers

An explicit finite cohomology presentation of a coefficient complex can be transported through the selected scalar-linear copower dg functor. The result is a finite biproduct of shifted degree-zero copowers in H⁰ C.

The construction reuses three existing categorical interfaces:

• homotopy invariance of linearCopowerFunctor;
• Mathlib's preservation of finite biproducts by additive functors;
• SingleFunctors.postcomp and the established coherent shift action on H⁰ of a dg functor.

Thus this file introduces no copower-specific direct-sum preservation record and no new shift comparison. Its finite-free specialization consumes the generic sibling interface, makes no basis-independence claim, computes no Grothendieck class, and asserts no Euler formula.

noncomputable def CochainComplex.FiniteCohomologyPresentation.linearCopowerIso {k : Type w} [CommRing k] {C : Type u} [CategoryTheory.DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((CategoryTheory.DGCategoryStruct.dgHom X Y).X p)] [CategoryTheory.DGLinear k C] [CategoryTheory.HasLinearCopowers k C] {K : CochainComplex (ModuleCat k) ℤ} [CategoryTheory.IsPretriangulated C] (P : K.FiniteCohomologyPresentation) (X : C) : (have this := CategoryTheory.linearCopowerObj K X; this) ≅ ⨁ fun (i : ↥P.degrees) => (CategoryTheory.shiftFunctor (CategoryTheory.H0 C) (-↑i)).obj (have this := CategoryTheory.linearCopowerObj ((singleFunctor (ModuleCat k) 0).obj (HomologicalComplex.homology K ↑i)) X; this)

A finite cohomology presentation of the coefficient complex presents its selected scalar-linear copower as a finite biproduct of shifted degree-zero copowers.

The shift is -i, following Mathlib's cochain convention. No cone preservation or exactness hypothesis is needed.

Equations

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

noncomputable def CochainComplex.FiniteCohomologyPresentation.linearCopowerFinrankIso {k : Type v} [CommRing k] [StrongRankCondition k] {C : Type u} [CategoryTheory.DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((CategoryTheory.DGCategoryStruct.dgHom X Y).X p)] [CategoryTheory.DGLinear k C] [CategoryTheory.HasLinearCopowers k C] {K : CochainComplex (ModuleCat k) ℤ} [CategoryTheory.IsPretriangulated C] (P : K.FiniteCohomologyPresentation) [∀ (i : ↥P.degrees), Module.Free k ↑(HomologicalComplex.homology K ↑i)] [∀ (i : ↥P.degrees), Module.Finite k ↑(HomologicalComplex.homology K ↑i)] (X : C) : (have this := CategoryTheory.linearCopowerObj K X; this) ≅ ⨁ fun (i : ↥P.degrees) => ⨁ fun (x : Fin (Module.finrank k ↑(HomologicalComplex.homology K ↑i))) => (CategoryTheory.shiftFunctor (CategoryTheory.H0 C) (-↑i)).obj (have this := X; this)

If the homology modules in a supplied finite presentation are finite free, the selected scalar-linear copower is a finite biproduct of shifts of the original object, with multiplicities given by their finranks.

The nested biproduct records the cohomological degree and its multiplicity separately. The isomorphism is noncanonical: each inner expansion uses Mathlib's noncomputably selected finite basis.

Equations

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