Finite homogeneous idempotent coordinates of an actual module

noncomputable def MagnitudeConjecture.Graded.ModuleGrading.idempotentCoordinateEquiv {k : Type u_1} {A : Type u_2} {M : Type u_3} [Field k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] {R : VectorGrading k A} (G : ModuleGrading R) {ι : Type u_4} {ν : Type u_5} [Fintype ι] [Fintype ν] (e : ι → A) (he : ∀ (i : ι), e i * e i = e i) (he0 : ∀ (i : ι), e i ∈ R.component 0) (hsum : ∑ i : ι, e i = 1) (horth : Pairwise fun (i j : ι) => e i * e j = 0) (δ : ν → ℤ) (hδ : Function.Injective δ) (hcover : ∀ (d : ℤ), G.component d ≠ ⊥ → ∃ (q : ν), δ q = d) : M ≃ₗ[k] (p : ι × ν) → ↥(idempotentComponent R G (e p.1) (δ p.2))

An actual graded module is the product of its finitely many homogeneous idempotent parts.