Magnitude conjecture

MagnitudeConjecture.Graded.FiniteVectorGrading

Finite support of an internal vector-space grading #

A finite-dimensional internally graded space has only finitely many nonzero degrees. We exhibit a support from the homogeneous supports of a finite basis, so subsequent homogeneous map constructions use finite sums.

source
structure MagnitudeConjecture.Graded.VectorGrading (k : Type u_1) (M : Type u_2) [Field k] [AddCommGroup M] [Module k M] :
Type u_2
  • component : ℤ → Submodule k M
  • internal : DirectSum.IsInternal self.component
Instances For
    source
    noncomputable def MagnitudeConjecture.Graded.VectorGrading.decompose {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) :
    M ≃ₗ[k] DirectSum ℤ fun (d : ℤ) => ↥(G.component d)
    Instances For
      source
      noncomputable def MagnitudeConjecture.Graded.VectorGrading.projection {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) (d : ℤ) :
      M →ₗ[k] M
      Instances For
        source
        theorem MagnitudeConjecture.Graded.VectorGrading.projection_mem {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) (d : ℤ) (x : M) :
        (G.projection d) x ∈ G.component d
        source
        theorem MagnitudeConjecture.Graded.VectorGrading.projection_of_mem {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) {d : ℤ} {x : M} (hx : x ∈ G.component d) :
        (G.projection d) x = x
        source
        theorem MagnitudeConjecture.Graded.VectorGrading.projection_of_mem_ne {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) {d e : ℤ} {x : M} (hx : x ∈ G.component d) (hde : d ≠ e) :
        (G.projection e) x = 0
        source
        noncomputable def MagnitudeConjecture.Graded.VectorGrading.degreeSupport {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) [FiniteDimensional k M] :
        Finset ℤ

        A finite set containing the support of every vector.

        Instances For
          source
          theorem MagnitudeConjecture.Graded.VectorGrading.projection_eq_zero_outside {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) [FiniteDimensional k M] {d : ℤ} (hd : d ∉ G.degreeSupport) :
          G.projection d = 0
          source
          theorem MagnitudeConjecture.Graded.VectorGrading.component_eq_bot_outside {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) [FiniteDimensional k M] {d : ℤ} (hd : d ∉ G.degreeSupport) :
          G.component d = ⊥
          source
          theorem MagnitudeConjecture.Graded.VectorGrading.sum_projection {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] (G : VectorGrading k M) [FiniteDimensional k M] (x : M) :
          ∑ d ∈ G.degreeSupport, (G.projection d) x = x

          The finite degree projections sum to the identity.