Scalar-linear copowers in a dg category

For a k-linear dg category, DGLinear.homComplex k X Y repackages the existing abelian-group-valued Hom-complex as a complex in ModuleCat k. It changes no underlying graded group or differential; DGLinear supplies exactly the linearity needed for the repackaging.

IsLinearCopowerOf k K X Z then says that Z represents degree-p k-linear cochains from K to DGLinear.homComplex k X W, for every degree and target. The universal family is an actual morphism of cochain complexes, and the existence wrappers follow Mathlib's HasLimit pattern.

This is intentionally not a refinement of the additive IsCopowerOf API. The latter is bijective onto all additive cochains; forgetting a linear universal property would only give bijectivity onto the linear ones, so no such projection is mathematically available for a general scalar extension. The two interfaces coincide only after additional comparison input (for example, over the integers), which is not asserted here.

The sibling LinearCopowerFunctor module packages coefficient-complex functoriality and homotopy invariance, while LinearEvaluation assembles these copowers into a scalar-linear evaluation functor and its closed evaluation transformation. None of these modules derives an Euler-class formula, which still needs a finite cohomology presentation.

def CategoryTheory.linearCopowerCochain (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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (univ : K ⟶ DGLinear.homComplex k X Z) {W : C} (p : ℤ) : ↑((DGLinear.homComplex k Z W).X p) →ₗ[k] CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p

The degree-p linear cochain induced by a degree-p morphism out of a linear copower: apply the universal chain map, then compose.

Equations

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

@[simp]

theorem CategoryTheory.linearCopowerCochain_apply (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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (univ : K ⟶ DGLinear.homComplex k X Z) {W : C} (p : ℤ) (g : ↑((DGCategoryStruct.dgHom Z W).X p)) (i j : ℤ) (h : i + p = j) (x : ↑(K.X i)) : (ModuleCat.Hom.hom (((linearCopowerCochain k univ p) g).v i j h)) x = ((DGCategoryStruct.dgComp i p j h) ((ConcreteCategory.hom (univ.f i)) x)) g

structure CategoryTheory.IsLinearCopowerOf (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] (K : CochainComplex (ModuleCat k) ℤ) (X Z : C) : Type v

Z is the k-linear tensoring of X by the complex K.

The universal family is a chain map K ⟶ DGLinear.homComplex k X Z. Composition with it identifies degree-p morphisms out of Z with degree-p linear cochains out of K, for every degree and target.

• univ : K ⟶ DGLinear.homComplex k X Z

  The universal linear chain map.

• bijective (W : C) (p : ℤ) : Function.Bijective ⇑(linearCopowerCochain k self.univ p)

  Composition with the universal chain map is bijective onto linear cochains, in every degree and from every target.

theorem CategoryTheory.IsLinearCopowerOf.univ_d {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) (i j : ℤ) (x : ↑(K.X i)) : (ConcreteCategory.hom (t.univ.f j)) ((ModuleCat.Hom.hom (K.d i j)) x) = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom X Z).d i j)) ((ConcreteCategory.hom (t.univ.f i)) x)

The universal family commutes with the differentials.

noncomputable def CategoryTheory.IsLinearCopowerOf.cochainLinearEquiv {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) (W : C) (p : ℤ) : ↑((DGCategoryStruct.dgHom Z W).X p) ≃ₗ[k] CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p

The representing bijection as a linear equivalence.

Equations

• t.cochainLinearEquiv W p = LinearEquiv.ofBijective (CategoryTheory.linearCopowerCochain k t.univ p) ⋯

theorem CategoryTheory.IsLinearCopowerOf.lift_unique {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) {W : C} {p : ℤ} {g g' : ↑((DGCategoryStruct.dgHom Z W).X p)} (h : ∀ (i j : ℤ) (hij : i + p = j) (x : ↑(K.X i)), ((DGCategoryStruct.dgComp i p j hij) ((ConcreteCategory.hom (t.univ.f i)) x)) g = ((DGCategoryStruct.dgComp i p j hij) ((ConcreteCategory.hom (t.univ.f i)) x)) g') : g = g'

A morphism out of a linear copower is determined by the cochain it induces.

noncomputable def CategoryTheory.IsLinearCopowerOf.lift {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) {W : C} (p : ℤ) (c : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p) : ↑((DGCategoryStruct.dgHom Z W).X p)

Every linear cochain out of K is induced by a morphism out of the linear copower.

Equations

• t.lift p c = (t.cochainLinearEquiv W p).symm c

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.lift_zero {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) {W : C} (p : ℤ) : t.lift p 0 = 0

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.lift_add {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) {W : C} (p : ℤ) (c c' : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p) : t.lift p (c + c') = t.lift p c + t.lift p c'

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.lift_smul {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) {W : C} (p : ℤ) (a : k) (c : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p) : t.lift p (a • c) = a • t.lift p c

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.univ_comp_lift {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) {W : C} (p : ℤ) (c : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p) (i j : ℤ) (hij : i + p = j) (x : ↑(K.X i)) : ((DGCategoryStruct.dgComp i p j hij) ((ConcreteCategory.hom (t.univ.f i)) x)) (t.lift p c) = (ModuleCat.Hom.hom (c.v i j hij)) x

noncomputable def CategoryTheory.IsLinearCopowerOf.compare {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') : ↑((DGCategoryStruct.dgHom Z Z').X 0)

The canonical comparison between two linear copowers of the same data.

Equations

• t.compare t' = t.lift 0 (CochainComplex.HomComplex.Cochain.ofHom t'.univ)

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.univ_comp_compare {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') (i : ℤ) (x : ↑(K.X i)) : ((DGCategoryStruct.dgComp i 0 i ⋯) ((ConcreteCategory.hom (t.univ.f i)) x)) (t.compare t') = (ConcreteCategory.hom (t'.univ.f i)) x

theorem CategoryTheory.IsLinearCopowerOf.compare_mem_cocycles {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') : t.compare t' ∈ cocycles Z Z'

The canonical comparison is closed, hence is a morphism in Z⁰ C.

theorem CategoryTheory.IsLinearCopowerOf.compare_comp_compare {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (t.compare t')) (t'.compare t) = DGCategoryStruct.dgId Z

The two canonical comparisons compose to the identity.

theorem CategoryTheory.IsLinearCopowerOf.compare_trans {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' Z'' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') (t'' : IsLinearCopowerOf k K X Z'') : ((DGCategoryStruct.dgComp 0 0 0 ⋯) (t.compare t')) (t'.compare t'') = t.compare t''

Canonical linear-copower comparisons compose strictly.

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.compare_self {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) : t.compare t = DGCategoryStruct.dgId Z

Comparing a linear copower with itself is the identity.

noncomputable def CategoryTheory.IsLinearCopowerOf.compareIso {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') : (have this := Z; this) ≅ have this := Z'; this

The canonical comparison between two linear-copower witnesses as an isomorphism in the closed degree-zero category.

Equations

• t.compareIso t' = { hom := ⟨t.compare t', ⋯⟩, inv := ⟨t'.compare t, ⋯⟩, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.compareIso_hom_val {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') : ↑(t.compareIso t').hom = t.compare t'

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.compareIso_inv_val {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') : ↑(t.compareIso t').inv = t'.compare t

@[simp]

theorem CategoryTheory.IsLinearCopowerOf.compareIso_self {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) : t.compareIso t = Iso.refl (have this := Z; this)

The canonical comparison of a linear-copower witness with itself is the identity isomorphism.

theorem CategoryTheory.IsLinearCopowerOf.compareIso_trans {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z Z' Z'' : C} (t : IsLinearCopowerOf k K X Z) (t' : IsLinearCopowerOf k K X Z') (t'' : IsLinearCopowerOf k K X Z'') : t.compareIso t' ≪≫ t'.compareIso t'' = t.compareIso t''

Canonical linear-copower comparison isomorphisms are transitive.

structure CategoryTheory.LinearCopowerData {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] (K : CochainComplex (ModuleCat k) ℤ) (X : C) : Type (max u v)

A linear copower object together with its universal-property witness.

• obj : C

  The chosen linear copower object.

• isLinearCopower : IsLinearCopowerOf k K X self.obj

  The universal property witnessed by the chosen object.

class CategoryTheory.HasLinearCopower (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] (K : CochainComplex (ModuleCat k) ℤ) (X : C) : Prop

Mere existence of a linear copower of X by K.

• exists_linearCopower : Nonempty (LinearCopowerData K X)

theorem CategoryTheory.HasLinearCopower.of_isLinearCopower {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] {K : CochainComplex (ModuleCat k) ℤ} {X Z : C} (t : IsLinearCopowerOf k K X Z) : HasLinearCopower k K X

A witnessed linear copower supplies the corresponding existence instance.

noncomputable def CategoryTheory.linearCopowerData {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] (K : CochainComplex (ModuleCat k) ℤ) (X : C) [HasLinearCopower k K X] : LinearCopowerData K X

A noncomputably selected linear copower and its witness.

Equations

• CategoryTheory.linearCopowerData K X = Classical.choice ⋯

noncomputable def CategoryTheory.linearCopowerObj {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] (K : CochainComplex (ModuleCat k) ℤ) (X : C) [HasLinearCopower k K X] : C

The linear copower object selected from HasLinearCopower k K X.

Equations

• CategoryTheory.linearCopowerObj K X = (CategoryTheory.linearCopowerData K X).obj

noncomputable def CategoryTheory.linearCopowerIsLinearCopower {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] (K : CochainComplex (ModuleCat k) ℤ) (X : C) [HasLinearCopower k K X] : IsLinearCopowerOf k K X (linearCopowerObj K X)

The witness for the selected linearCopowerObj k K X.

Equations

• CategoryTheory.linearCopowerIsLinearCopower K X = (CategoryTheory.linearCopowerData K X).isLinearCopower

class CategoryTheory.HasLinearCopowers (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] : Prop

Existence of all k-linear copowers in a k-linear dg category.

• has_linearCopower (K : CochainComplex (ModuleCat k) ℤ) (X : C) : HasLinearCopower k K X

@[instance 100]

instance CategoryTheory.hasLinearCopowerOfHasLinearCopowers {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] (K : CochainComplex (ModuleCat k) ℤ) (X : C) : HasLinearCopower k K X

All linear copowers give each individual linear copower.