Homogeneous components of module maps #
Projection of an algebra-linear map to a homogeneous degree is again algebra-linear. We work with left modules; applying the construction to the opposite algebra gives the project's right-module convention.
structure
MagnitudeConjecture.Graded.ModuleGrading
{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]
(R : VectorGrading k A)
extends MagnitudeConjecture.Graded.VectorGrading k M :
Type u_3
An internal vector-space grading compatible with the homogeneous algebra action. Multiplicativity of the algebra grading is not needed for this lemma.
- component : ℤ → Submodule k M
Instances For
theorem
MagnitudeConjecture.Graded.ModuleGrading.projection_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)
{i : ℤ}
{a : A}
(ha : a ∈ R.component i)
(j : ℤ)
(x : M)
:
(G.projection (i + j)) (a • x) = a • (G.projection j) x
Multiplication by a homogeneous algebra element shifts the projections.
theorem
MagnitudeConjecture.Graded.ModuleGrading.mapPart_smul_homogeneous
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
(d : ℤ)
(f : M →ₗ[A] N)
{i j : ℤ}
{a : A}
{x : M}
(ha : a ∈ R.component i)
(hx : x ∈ G.component j)
:
(G.mapPart H.toVectorGrading d (↑k f)) (a • x) = a • (G.mapPart H.toVectorGrading d (↑k f)) x
theorem
MagnitudeConjecture.Graded.ModuleGrading.mapPart_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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
(d : ℤ)
(f : M →ₗ[A] N)
(a : A)
(x : M)
:
(G.mapPart H.toVectorGrading d (↑k f)) (a • x) = a • (G.mapPart H.toVectorGrading d (↑k f)) x
Every homogeneous component of an algebra-linear map commutes with all algebra elements, not just homogeneous ones.
noncomputable def
MagnitudeConjecture.Graded.ModuleGrading.homPart
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
(d : ℤ)
(f : M →ₗ[A] N)
:
M →ₗ[A] N
The degree component as an actual algebra-linear map.
Instances For
theorem
MagnitudeConjecture.Graded.ModuleGrading.homPart_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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
(d : ℤ)
(f : M →ₗ[A] N)
{i : ℤ}
{x : M}
(hx : x ∈ G.component i)
:
def
MagnitudeConjecture.Graded.ModuleGrading.Homogeneous
{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]
{R : VectorGrading k A}
(G : ModuleGrading R)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
(H : ModuleGrading R)
(d : ℤ)
(f : M →ₗ[A] N)
:
A degree-preserving condition stated directly for algebra-linear maps.
Instances For
theorem
MagnitudeConjecture.Graded.ModuleGrading.homPart_homogeneous
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
(d : ℤ)
(f : M →ₗ[A] N)
:
G.Homogeneous H d (G.homPart H d f)
theorem
MagnitudeConjecture.Graded.ModuleGrading.homPart_of_homogeneous
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
{d : ℤ}
{f : M →ₗ[A] N}
(hf : G.Homogeneous H d f)
:
G.homPart H d f = f
theorem
MagnitudeConjecture.Graded.ModuleGrading.homPart_of_homogeneous_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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
{d e : ℤ}
{f : M →ₗ[A] N}
(hf : G.Homogeneous H d f)
(hde : d ≠ e)
:
G.homPart H e f = 0
theorem
MagnitudeConjecture.Graded.ModuleGrading.sum_homPart
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
[FiniteDimensional k N]
(f : M →ₗ[A] N)
:
∑ d ∈ G.mapDegreeSupport H.toVectorGrading, G.homPart H d f = f
theorem
MagnitudeConjecture.Graded.ModuleGrading.homPart_eq_zero_outside
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
[FiniteDimensional k N]
(d : ℤ)
(f : M →ₗ[A] N)
(hd : d ∉ G.mapDegreeSupport H.toVectorGrading)
:
G.homPart H d f = 0
theorem
MagnitudeConjecture.Graded.ModuleGrading.id_homogeneous
{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)
[FiniteDimensional k M]
:
G.Homogeneous G 0 LinearMap.id
theorem
MagnitudeConjecture.Graded.ModuleGrading.homogeneous_comp
{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)
{N : Type u_4}
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
(H : ModuleGrading R)
[FiniteDimensional k M]
{P : Type u_5}
[AddCommGroup P]
[Module k P]
[Module A P]
[IsScalarTower k A P]
(J : ModuleGrading R)
{d e : ℤ}
{f : M →ₗ[A] N}
{g : N →ₗ[A] P}
(hf : G.Homogeneous H d f)
(hg : H.Homogeneous J e g)
:
G.Homogeneous J (d + e) (g ∘ₗ f)