Scalar-linear copowers and the homotopy-category enhancement #
The scalar-linear copower dg functor sends a homotopy equivalence of
coefficient complexes to an isomorphism between the selected copowers in
H⁰. This leaf owns the comparison because it uses the specialized
equivalence between H⁰(C^dg) and Mathlib's homotopy category.
noncomputable def
CategoryTheory.linearCopowerObjIsoOfHomotopyEquiv
{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)}
(e : HomotopyEquiv (Cdg.of (ModuleCat k) K) (Cdg.of (ModuleCat k) L))
:
(have this := linearCopowerObj (Cdg.of (ModuleCat k) K) X;
this) ≅ have this := linearCopowerObj (Cdg.of (ModuleCat k) L) X;
this
Homotopy equivalent coefficient complexes give isomorphic selected
scalar-linear copowers in H⁰ C. The construction uses the established seam
H⁰(C^dg) ≃ K(k) rather than another quotient-category implementation.