Finite-free scalar-linear copowers

Degreewise scalar-linear copowers of single coefficient modules form a coherent shifted family. A supplied finite basis expands the degree-zero member as a finite biproduct of copies of the original object in H⁰; finite free modules over rings with strong rank condition therefore have a finrank expansion.

The public basis interface allows an arbitrary finite index universe. Its implementation reindexes to Fin n, where Mathlib's concrete ModuleCat.biproductIsoPi and additive-functor preservation apply, and then uses Mathlib's categorical biproduct reindexing. No basis-independence, Grothendieck-class, or Euler claim is made.

noncomputable def CategoryTheory.linearCopowerSingleFunctors {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] [IsPretriangulated C] (X : C) : SingleFunctors (ModuleCat k) (H0 C) ℤ

Degreewise scalar-linear copowers of single coefficient modules, with their coherent shift comparison inherited by postcomposition.

Equations

• CategoryTheory.linearCopowerSingleFunctors X = (CochainComplex.singleFunctors (ModuleCat k)).postcomp ((CategoryTheory.Cdg.toH0 (ModuleCat k)).comp (CategoryTheory.linearCopowerFunctor k X).h0)

@[simp]

theorem CategoryTheory.linearCopowerSingleFunctors_obj {k : Type w} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] [IsPretriangulated C] (X : C) (i : ℤ) (V : ModuleCat k) : ((linearCopowerSingleFunctors X).functor i).obj V = have this := linearCopowerObj ((CochainComplex.singleFunctor (ModuleCat k) i).obj V) X; this

noncomputable def CategoryTheory.linearCopowerSingleZeroIsoOfBasis {k : Type v} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] [IsPretriangulated C] {ι : Type w} [Finite ι] {V : ModuleCat k} (b : Module.Basis ι k ↑V) (X : C) : (have this := linearCopowerObj ((CochainComplex.singleFunctor (ModuleCat k) 0).obj V) X; this) ≅ ⨁ fun (x : ι) => have this := X; this

A chosen finite basis expands the degree-zero single linear copower into a finite biproduct of copies of the original object. The index universe is independent of the coefficient-module universe.

Equations

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

noncomputable def CategoryTheory.linearCopowerSingleZeroFinrankIso {k : Type v} [CommRing k] {C : Type u} [DGCategory C] [(X Y : C) → (p : ℤ) → Module k ↑((DGCategoryStruct.dgHom X Y).X p)] [DGLinear k C] [HasLinearCopowers k C] [StrongRankCondition k] [IsPretriangulated C] {V : ModuleCat k} [Module.Free k ↑V] [Module.Finite k ↑V] (X : C) : (have this := linearCopowerObj ((CochainComplex.singleFunctor (ModuleCat k) 0).obj V) X; this) ≅ ⨁ fun (x : Fin (Module.finrank k ↑V)) => have this := X; this

A finite free degree-zero coefficient module over a ring with strong rank condition expands its selected linear copower into finrank copies of the original object. The isomorphism uses Mathlib's noncomputably selected finite basis; fields are the main specialization.

Equations

• CategoryTheory.linearCopowerSingleZeroFinrankIso X = CategoryTheory.linearCopowerSingleZeroIsoOfBasis (Module.finBasis k ↑V) X