Functoriality of scalar-linear dg copowers #
A degree-p element of HomComplex.Cochain K L p induces a degree-p
morphism between any chosen scalar-linear copowers of a fixed dg object X:
compose the cochain with the target universal chain map, then apply the source
representing inverse. This construction is linear, commutes with
differentials, and preserves graded composition strictly.
Consequently, when all scalar-linear copowers exist, the selected objects form
a linear dg functor C^dg(ModuleCat k) ⟶ C. At witness level,
homotopy-equivalent coefficient complexes induce isomorphic copowers in H⁰.
The specialized comparison through Mathlib's homotopy category lives with the
H⁰(C^dg) enhancement seam.
This is homotopy invariance, not quasi-isomorphism invariance. No boundedness, finite-dimensionality, shift decomposition, Euler-class formula, cone preservation, or concrete copower instance is asserted here.
theorem
CategoryTheory.IsLinearCopowerOf.linearCopowerCochain_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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
(W : C)
(p q : ℤ)
(f : ↑((DGCategoryStruct.dgHom ZK W).X p))
:
CochainComplex.HomComplex.δ p q ((linearCopowerCochain k tK.univ p) f) = (linearCopowerCochain k tK.univ q) ((AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom ZK W).d p q)) f)
The representing map from a linear copower is a morphism of Hom-complexes.
noncomputable def
CategoryTheory.IsLinearCopowerOf.homComplexIso
{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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
(W : C)
:
DGLinear.homComplex k ZK W ≅ DGLinear.homComplex k
(have this := K;
this)
(have this := DGLinear.homComplex k X W;
this)
The universal property as an isomorphism of Hom-complexes. This packages all degrees and the compatibility with differentials in one categorical interface.
Equations
- tK.homComplexIso W = HomologicalComplex.Hom.isoOfComponents (fun (p : ℤ) => (tK.cochainLinearEquiv W p).toModuleIso) ⋯
Instances For
theorem
CategoryTheory.IsLinearCopowerOf.homComplexIso_hom_f_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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
(W : C)
(p : ℤ)
(f : ↑((DGCategoryStruct.dgHom ZK W).X p))
:
theorem
CategoryTheory.IsLinearCopowerOf.homComplexIso_inv_f_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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
(W : C)
(p : ℤ)
(γ : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p)
:
theorem
CategoryTheory.IsLinearCopowerOf.lift_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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
{W : C}
(p q : ℤ)
(γ : CochainComplex.HomComplex.Cochain K (DGLinear.homComplex k X W) p)
:
tK.lift q (CochainComplex.HomComplex.δ p q γ) = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom ZK W).d p q)) (tK.lift p γ)
The representing inverse intertwines Mathlib's Hom-complex differential with the dg differential.
noncomputable def
CategoryTheory.IsLinearCopowerOf.coefficientMap
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(p : ℤ)
:
A homogeneous cochain between coefficient complexes induces a homogeneous morphism between their scalar-linear copowers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.IsLinearCopowerOf.univ_comp_coefficientMap
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(p : ℤ)
(γ : CochainComplex.HomComplex.Cochain K L p)
(i j : ℤ)
(hij : i + p = j)
(x : ↑(K.X i))
:
((DGCategoryStruct.dgComp i p j hij) ((ConcreteCategory.hom (tK.univ.f i)) x)) ((tK.coefficientMap tL p) γ) = (ConcreteCategory.hom (tL.univ.f j)) ((ModuleCat.Hom.hom (γ.v i j hij)) x)
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMap_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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(p q : ℤ)
(γ : CochainComplex.HomComplex.Cochain K L p)
:
(tK.coefficientMap tL q) (CochainComplex.HomComplex.δ p q γ) = (AddCommGrpCat.Hom.hom ((DGCategoryStruct.dgHom ZK ZL).d p q)) ((tK.coefficientMap tL p) γ)
The homogeneous cochain action intertwines Mathlib's Hom-complex differential with the dg differential.
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMap_comp
{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 L M : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL ZM : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(tM : IsLinearCopowerOf k M X ZM)
(p q r : ℤ)
(h : p + q = r)
(γ : CochainComplex.HomComplex.Cochain K L p)
(η : CochainComplex.HomComplex.Cochain L M q)
:
((DGCategoryStruct.dgComp p q r h) ((tK.coefficientMap tL p) γ)) ((tL.coefficientMap tM q) η) = (tK.coefficientMap tM r) (γ.comp η h)
Homogeneous coefficient cochains compose strictly after passage to their scalar-linear copowers.
@[simp]
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMap_id
{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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
:
(tK.coefficientMap tK 0) (CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id K)) = DGCategoryStruct.dgId ZK
The identity cochain induces the dg identity when the same copower witness is used at both ends.
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMap_id_eq_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 ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tK' : IsLinearCopowerOf k K X ZL)
:
(tK.coefficientMap tK' 0) (CochainComplex.HomComplex.Cochain.ofHom (CategoryStruct.id K)) = tK.compare tK'
Between two choices for the same coefficient complex, the lifted identity is the existing canonical comparison.
noncomputable def
CategoryTheory.IsLinearCopowerOf.coefficientMapOfHom
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
:
A chain map between coefficient complexes induces a degree-zero dg morphism between their scalar-linear copowers.
Equations
- tK.coefficientMapOfHom tL = { toFun := fun (f : K ⟶ L) => (tK.coefficientMap tL 0) (CochainComplex.HomComplex.Cochain.ofHom f), map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.IsLinearCopowerOf.univ_comp_coefficientMapOfHom
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(f : K ⟶ L)
(i : ℤ)
(x : ↑(K.X i))
:
((DGCategoryStruct.dgComp i 0 i ⋯) ((ConcreteCategory.hom (tK.univ.f i)) x)) ((tK.coefficientMapOfHom tL) f) = (ConcreteCategory.hom (tL.univ.f i)) ((ConcreteCategory.hom (f.f i)) x)
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMapOfHom_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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(f : K ⟶ L)
:
Coefficient chain maps induce closed degree-zero dg morphisms.
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMapOfHom_id_eq_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 ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tK' : IsLinearCopowerOf k K X ZL)
:
The identity coefficient map is the canonical comparison between two choices for the same linear copower.
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMapOfHom_comp
{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 L M : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL ZM : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(tM : IsLinearCopowerOf k M X ZM)
(f : K ⟶ L)
(g : L ⟶ M)
:
((DGCategoryStruct.dgComp 0 0 0 ⋯) ((tK.coefficientMapOfHom tL) f)) ((tL.coefficientMapOfHom tM) g) = (tK.coefficientMapOfHom tM) (CategoryStruct.comp f g)
Coefficient chain maps compose strictly after passage to linear copowers.
theorem
CategoryTheory.IsLinearCopowerOf.coefficientMapOfHom_sub_mem_coboundaries
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
{f g : K ⟶ L}
(h : Homotopy f g)
:
Homotopic coefficient chain maps induce dg morphisms whose difference is a coboundary.
noncomputable def
CategoryTheory.IsLinearCopowerOf.coefficientHom
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(f : K ⟶ L)
:
The H⁰ morphism induced by a coefficient chain map.
Equations
- tK.coefficientHom tL f = CategoryTheory.H0.homMk ⟨(tK.coefficientMapOfHom tL) f, ⋯⟩
Instances For
theorem
CategoryTheory.IsLinearCopowerOf.coefficientHom_eq_of_homotopy
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
{f g : K ⟶ L}
(h : Homotopy f g)
:
Homotopic coefficient chain maps induce equal morphisms in H⁰ C.
@[simp]
theorem
CategoryTheory.IsLinearCopowerOf.coefficientHom_id
{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 ZK : C}
(tK : IsLinearCopowerOf k K X ZK)
:
The coefficient action preserves identities in H⁰ C.
theorem
CategoryTheory.IsLinearCopowerOf.coefficientHom_comp
{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 L M : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL ZM : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(tM : IsLinearCopowerOf k M X ZM)
(f : K ⟶ L)
(g : L ⟶ M)
:
CategoryStruct.comp (tK.coefficientHom tL f) (tL.coefficientHom tM g) = tK.coefficientHom tM (CategoryStruct.comp f g)
The coefficient action preserves composition in H⁰ C.
noncomputable def
CategoryTheory.IsLinearCopowerOf.homotopyEquivIso
{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 L : CochainComplex (ModuleCat k) ℤ}
{X ZK ZL : C}
(tK : IsLinearCopowerOf k K X ZK)
(tL : IsLinearCopowerOf k L X ZL)
(e : HomotopyEquiv K L)
:
A homotopy equivalence of coefficient complexes induces an isomorphism
between any witnessed scalar-linear copowers in H⁰ C.
Equations
- tK.homotopyEquivIso tL e = { hom := tK.coefficientHom tL e.hom, inv := tL.coefficientHom tK e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
noncomputable def
CategoryTheory.linearCopowerFunctor
(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]
(X : C)
:
For a fixed dg object, selected scalar-linear copowers form a linear dg functor from the standard dg category of complexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.linearCopowerFunctor_linear
{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]
(X : C)
:
DGFunctor.Linear k (linearCopowerFunctor k X)
@[simp]
theorem
CategoryTheory.linearCopowerFunctor_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]
(X : C)
(K : Cdg (ModuleCat k))
:
theorem
CategoryTheory.linearCopowerFunctor_map
{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]
(X : C)
{K L : Cdg (ModuleCat k)}
(p : ℤ)
(f : ↑((DGCategoryStruct.dgHom K L).X p))
:
((linearCopowerFunctor k X).map p) f = ((linearCopowerIsLinearCopower (Cdg.of (ModuleCat k) K) X).coefficientMap
(linearCopowerIsLinearCopower (Cdg.of (ModuleCat k) L) X) p)
f