Idempotent coordinates commute with bundling a graded module #
def
MagnitudeConjecture.Graded.ModuleGrading.bundledIdempotentComponentEquiv
{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]
[FiniteDimensional k M]
{R : VectorGrading k A}
(G : ModuleGrading R)
(e : A)
(d : ℤ)
:
↥(idempotentComponent R G.toBundled.grading e d) ≃ₗ[k] ↥(idempotentComponent R G e d)
The canonical bundled field action preserves each homogeneous idempotent coordinate.