The grading of a finite family of labelled coordinate spaces #
def
MagnitudeConjecture.Graded.VectorGrading.coordinateComponent
{k : Type u_1}
{ι : Type u_2}
[Field k]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
(d : ℤ)
:
Submodule k ((i : ι) → V i)
Vectors supported on the coordinates carrying one prescribed degree.
Instances For
def
MagnitudeConjecture.Graded.VectorGrading.coordinateProjection
{k : Type u_1}
{ι : Type u_2}
[Field k]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
(d : ℤ)
:
((i : ι) → V i) →ₗ[k] (i : ι) → V i
Keep only coordinates of one degree.
Instances For
theorem
MagnitudeConjecture.Graded.VectorGrading.coordinateProjection_mem
{k : Type u_1}
{ι : Type u_2}
[Field k]
[Fintype ι]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
(d : ℤ)
(x : (i : ι) → V i)
:
(coordinateProjection V degree d) x ∈ coordinateComponent V degree d
theorem
MagnitudeConjecture.Graded.VectorGrading.coordinateProjection_of_mem
{k : Type u_1}
{ι : Type u_2}
[Field k]
[Fintype ι]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
{d : ℤ}
{x : (i : ι) → V i}
(hx : x ∈ coordinateComponent V degree d)
:
(coordinateProjection V degree d) x = x
theorem
MagnitudeConjecture.Graded.VectorGrading.coordinateProjection_of_mem_ne
{k : Type u_1}
{ι : Type u_2}
[Field k]
[Fintype ι]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
{d n : ℤ}
{x : (i : ι) → V i}
(hx : x ∈ coordinateComponent V degree d)
(hdn : d ≠ n)
:
(coordinateProjection V degree n) x = 0
theorem
MagnitudeConjecture.Graded.VectorGrading.sum_coordinateProjection
{k : Type u_1}
{ι : Type u_2}
[Field k]
[Fintype ι]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
(x : (i : ι) → V i)
:
∑ d ∈ Finset.image degree Finset.univ, (coordinateProjection V degree d) x = x
def
MagnitudeConjecture.Graded.VectorGrading.coordinateGrading
{k : Type u_1}
{ι : Type u_2}
[Field k]
[Fintype ι]
(V : ι → Type u_3)
[(i : ι) → AddCommGroup (V i)]
[(i : ι) → Module k (V i)]
(degree : ι → ℤ)
:
VectorGrading k ((i : ι) → V i)
Grouping a finite product's coordinate spaces by their labels is an internal grading.