Evaluation on the graded regular module #
def
MagnitudeConjecture.Graded.VectorGrading.regularModuleGrading
{k : Type u_1}
{A : Type u_2}
[Field k]
[Ring A]
[Algebra k A]
(R : VectorGrading k A)
(hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j))
:
The algebra grading regarded as the grading of the left regular module.
Instances For
theorem
MagnitudeConjecture.Graded.VectorGrading.regular_homogeneous_iff
{k : Type u_1}
{A : Type u_2}
[Field k]
[Ring A]
[Algebra k A]
(R : VectorGrading k A)
(hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j))
{M : Type u_3}
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
(G : ModuleGrading R)
(h1 : 1 ∈ R.component 0)
(d : ℤ)
(f : A →ₗ[A] M)
:
(R.regularModuleGrading ⋯).Homogeneous G d f ↔ f 1 ∈ G.component d
Evaluation at one detects the degree of a map out of the regular module.
def
MagnitudeConjecture.Graded.VectorGrading.regularHomEquiv
{k : Type u_1}
{A : Type u_2}
[Field k]
[Ring A]
[Algebra k A]
(R : VectorGrading k A)
(hmul : ∀ {i j : ℤ} {a b : A}, a ∈ R.component i → b ∈ R.component j → a * b ∈ R.component (i + j))
{M : Type u_3}
[AddCommGroup M]
[Module k M]
[Module A M]
[IsScalarTower k A M]
(G : ModuleGrading R)
(h1 : 1 ∈ R.component 0)
(d : ℤ)
:
↥((R.regularModuleGrading ⋯).homComponent G d) ≃ₗ[k] ↥(G.component d)
Homogeneous maps out of the regular module are exactly homogeneous vectors.