Homogeneous idempotent projections #
noncomputable def
MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection
{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)
(e : A)
(d : ℤ)
:
M →ₗ[k] M
First take the homogeneous component, then apply the idempotent.
Instances For
theorem
MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection_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)
(e : A)
(he : e * e = e)
(he0 : e ∈ R.component 0)
(d : ℤ)
(x : M)
:
(G.idempotentProjection e d) x ∈ idempotentComponent R G e d
theorem
MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection_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)
(e : A)
(d : ℤ)
(x : M)
(hx : x ∈ idempotentComponent R G e d)
:
(G.idempotentProjection e d) x = x
theorem
MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection_of_degree_ne
{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)
(e : A)
{d d' : ℤ}
(h : d' ≠ d)
(x : M)
(hx : x ∈ G.component d')
:
(G.idempotentProjection e d) x = 0
theorem
MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection_of_orthogonal
{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)
{e f : A}
(hef : e * f = 0)
(d : ℤ)
(x : M)
(hx : x ∈ idempotentComponent R G f d)
:
(G.idempotentProjection e d) x = 0
theorem
MagnitudeConjecture.Graded.ModuleGrading.sum_idempotentProjection
{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)
(hsum : ∑ i : ι, e i = 1)
(δ : ν → ℤ)
(hδ : Function.Injective δ)
(hcover : ∀ (d : ℤ), G.component d ≠ ⊥ → ∃ (q : ν), δ q = d)
(x : M)
:
∑ p : ι × ν, (G.idempotentProjection (e p.1) (δ p.2)) x = x
The homogeneous idempotent coordinates sum back to the original vector.