The scalar unit linear copower

In a k-linear dg category, the degree-zero single complex on k has X itself as its linear copower with X. The universal chain map sends 1 to the dg identity of X.

This is the unit computation for the existing IsLinearCopowerOf interface. It does not choose a global HasLinearCopowers instance or assert anything about finite-dimensional coefficient modules.

noncomputable def CategoryTheory.linearCopowerUnitCocycle {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] (X : C) : CochainComplex.HomComplex.Cocycle ((CochainComplex.singleFunctor (ModuleCat k) 0).obj (ModuleCat.of k k)) (DGLinear.homComplex k X X) 0

The closed cochain which sends the scalar unit to the dg identity of X.

Equations

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

noncomputable def CategoryTheory.linearCopowerUnitUniv {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] (X : C) : (CochainComplex.singleFunctor (ModuleCat k) 0).obj (ModuleCat.of k k) ⟶ DGLinear.homComplex k X X

The universal chain map for the scalar-unit linear copower of X.

Equations

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

theorem CategoryTheory.cochain_ofHom_linearCopowerUnitUniv {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] (X : C) : CochainComplex.HomComplex.Cochain.ofHom (linearCopowerUnitUniv X) = CochainComplex.HomComplex.Cochain.fromSingleMk (ModuleCat.ofHom ((LinearMap.ringLmapEquivSelf k k ↑((DGCategoryStruct.dgHom X X).X 0)).symm (DGCategoryStruct.dgId X))) ⋯

The universal chain map, in the canonical cochain coordinate on the degree-zero single, sends a to a • dgId X.

noncomputable def CategoryTheory.isLinearCopowerOfUnit {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] (X : C) : IsLinearCopowerOf k ((CochainComplex.singleFunctor (ModuleCat k) 0).obj (ModuleCat.of k k)) X X

The degree-zero single complex on the scalar ring has X itself as its linear copower with X.

Equations

• CategoryTheory.isLinearCopowerOfUnit X = { univ := CategoryTheory.linearCopowerUnitUniv X, bijective := ⋯ }

noncomputable def CategoryTheory.linearCopowerUnitIso {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] (X : C) [HasLinearCopower k ((CochainComplex.singleFunctor (ModuleCat k) 0).obj (ModuleCat.of k k)) X] : (have this := linearCopowerObj ((CochainComplex.singleFunctor (ModuleCat k) 0).obj (ModuleCat.of k k)) X; this) ≅ have this := X; this

The selected scalar-unit linear copower is isomorphic to the original object in H⁰ C.

Equations

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