The algebra action in homogeneous idempotent coordinates

theorem MagnitudeConjecture.Graded.ModuleGrading.projection_smul_of_mem {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) {t : ℤ} {x : M} (hx : x ∈ G.component t) (s : ℤ) (a : A) : (G.projection s) (a • x) = (R.projection (s - t)) a • x

For a homogeneous vector, the target projection selects one coefficient of the algebra element.

theorem MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection_smul {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) (δ : ν → ℤ) (hδ : Function.Injective δ) (hcover : ∀ (d : ℤ), G.component d ≠ ⊥ → ∃ (q : ν), δ q = d) (p : ι × ν) (a : A) (x : M) : (G.idempotentProjection (e p.1) (δ p.2)) (a • x) = ∑ q : ι × ν, (e p.1 * (R.projection (δ p.2 - δ q.2)) a * e q.1) • (G.idempotentProjection (e q.1) (δ q.2)) x

The action matrix is given by homogeneous corners of the algebra.