Internal grading of algebra-linear maps #
The homogeneous module maps form an internal direct sum of the full Hom space.
def
MagnitudeConjecture.Graded.ModuleGrading.homComponent
{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]
[AddCommGroup N]
[Module k N]
[Module A N]
[IsScalarTower k A N]
{R : VectorGrading k A}
(G : ModuleGrading R)
(H : ModuleGrading R)
(d : ℤ)
:
Submodule k (M →ₗ[A] N)
The subspace of algebra-linear maps of a given degree.
Instances For
noncomputable def
MagnitudeConjecture.Graded.ModuleGrading.homProjection
{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)
[FiniteDimensional k M]
(d : ℤ)
:
(M →ₗ[A] N) →ₗ[k] M →ₗ[A] N
Homogeneous projection is linear in the original module map.
Instances For
theorem
MagnitudeConjecture.Graded.ModuleGrading.homComponent_isInternal
{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)
[FiniteDimensional k M]
[FiniteDimensional k N]
:
DirectSum.IsInternal (G.homComponent H)
Every module map is uniquely a finite sum of homogeneous module maps.
def
MagnitudeConjecture.Graded.ModuleGrading.homGrading
{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)
[FiniteDimensional k M]
[FiniteDimensional k N]
:
VectorGrading k (M →ₗ[A] N)
The internal vector-space grading of the full module Hom space.