Homogeneous maps commute with shifted projections #
theorem
MagnitudeConjecture.Graded.ModuleGrading.projection_map_homogeneous
{k : Type u_1}
{A : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Field k]
[Ring A]
[Algebra k A]
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
{R : VectorGrading k A}
(G : ModuleGrading R)
(H : ModuleGrading R)
(f : M →ₗ[A] N)
(t : ℤ)
(hf : G.Homogeneous H t f)
(d : ℤ)
(x : M)
:
(H.projection (d + t)) (f x) = f ((G.projection d) x)
theorem
MagnitudeConjecture.Graded.ModuleGrading.idempotentProjection_map
{k : Type u_1}
{A : Type u_2}
{M : Type u_3}
{N : Type u_4}
[Field k]
[Ring A]
[Algebra k A]
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
{R : VectorGrading k A}
(G : ModuleGrading R)
(H : ModuleGrading R)
(f : M →ₗ[A] N)
(t : ℤ)
(hf : G.Homogeneous H t f)
(e : A)
(d : ℤ)
(x : M)
:
(H.idempotentProjection e (d + t)) (f x) = f ((G.idempotentProjection e d) x)