Bundling graded modules with the canonical field action #
def
MagnitudeConjecture.Graded.bundledModule
{A : Type u}
[Ring A]
{M : Type v}
[AddCommGroup M]
[Module A M]
:
ModuleCat A
Instances For
def
MagnitudeConjecture.Graded.moduleCatScalarEquiv
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{M : Type v}
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
:
↑bundledModule ≃ₗ[k] M
The canonical field action on a bundled algebra module agrees linearly with any given compatible field action.
Instances For
def
MagnitudeConjecture.Graded.ModuleGrading.toBundled
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{M : Type v}
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
{R : VectorGrading k A}
(G : ModuleGrading R)
[FiniteDimensional k M]
:
Bundle the grading after identifying the two compatible field actions.