Graded submodules and homogeneous kernels and images #
theorem
MagnitudeConjecture.Graded.ModuleGrading.projection_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)
(hf : G.Homogeneous H 0 f)
(d : ℤ)
(x : M)
:
(H.projection d) (f x) = f ((G.projection d) x)
Degree-zero module maps commute with every homogeneous projection.
def
MagnitudeConjecture.Graded.ModuleGrading.restrict
{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]
(P : Submodule A M)
(hP : G.Stable (Submodule.restrictScalars k P))
:
A submodule stable under all projections inherits the module grading.
Instances For
theorem
MagnitudeConjecture.Graded.ModuleGrading.kernel_stable
{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]
(f : M →ₗ[A] N)
(hf : G.Homogeneous H 0 f)
:
G.Stable (Submodule.restrictScalars k f.ker)
theorem
MagnitudeConjecture.Graded.ModuleGrading.range_stable
{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]
(f : M →ₗ[A] N)
(hf : G.Homogeneous H 0 f)
:
H.Stable (Submodule.restrictScalars k f.range)
def
MagnitudeConjecture.Graded.ModuleGrading.kernelGrading
{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]
(f : M →ₗ[A] N)
(hf : G.Homogeneous H 0 f)
:
The actual kernel carries the induced grading.
Instances For
def
MagnitudeConjecture.Graded.ModuleGrading.rangeGrading
{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]
(f : M →ₗ[A] N)
(hf : G.Homogeneous H 0 f)
:
The actual image carries the induced grading.