Magnitude conjecture

MagnitudeConjecture.Graded.FinitePiGrading

Componentwise gradings on finite products of vector spaces #

source
noncomputable def MagnitudeConjecture.Graded.VectorGrading.piSupport {k : Type u_1} {ι : Type u_2} [Field k] [Fintype ι] {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module k (M i)] [∀ (i : ι), FiniteDimensional k (M i)] (G : (i : ι) → VectorGrading k (M i)) :
Finset ℤ

The union of the finite homogeneous supports of all coordinates.

Instances For
    source
    theorem MagnitudeConjecture.Graded.VectorGrading.sum_piSupport {k : Type u_1} {ι : Type u_2} [Field k] [Fintype ι] {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module k (M i)] [∀ (i : ι), FiniteDimensional k (M i)] (G : (i : ι) → VectorGrading k (M i)) (i : ι) (x : M i) :
    ∑ d ∈ piSupport G, ((G i).projection d) x = x
    source
    def MagnitudeConjecture.Graded.VectorGrading.finitePi {k : Type u_1} {ι : Type u_2} [Field k] [Fintype ι] {M : ι → Type u_3} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module k (M i)] [∀ (i : ι), FiniteDimensional k (M i)] (G : (i : ι) → VectorGrading k (M i)) :
    VectorGrading k ((i : ι) → M i)

    The degree-d component consists of tuples whose coordinates all have degree d.

    Instances For