Linearity of the standard dg category of complexes #
For a commutative ring k, Mathlib's Hom-complexes of complexes of
k-modules carry their existing pointwise k-module structures. Mathlib's
linearity lemmas for the Hom differential and cochain composition therefore
supply the DGLinear k structure on Cdg (ModuleCat k) directly.
No additional module structure is introduced here.
@[implicit_reducible]
instance
CategoryTheory.Cdg.homModule
(k : Type w)
[CommRing k]
(K L : Cdg (ModuleCat k))
(p : ℤ)
:
Module k ↑((DGCategoryStruct.dgHom K L).X p)
Expose Mathlib's existing pointwise module structure through the opaque
Cdg/dgHom wrappers. This is a definitional bridge, not a new action.
Equations
- CategoryTheory.Cdg.homModule k K L p = id inferInstance