Magnitude conjecture

MagnitudeConjecture.Graded.LinearMapComponents

Homogeneous components of linear maps #

For an internally graded finite-dimensional source, each degree component of a linear map is a finite sum of source and target projections.

source
noncomputable def MagnitudeConjecture.Graded.VectorGrading.mapPart {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) (d : ℤ) (f : M →ₗ[k] N) :
M →ₗ[k] N

The degree d part of a linear map.

Instances For
    source
    theorem MagnitudeConjecture.Graded.VectorGrading.mapPart_apply_of_mem {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) (d : ℤ) (f : M →ₗ[k] N) {i : ℤ} {x : M} (hx : x ∈ G.component i) :
    (G.mapPart H d f) x = (H.projection (i + d)) (f x)

    On a vector of degree i, the component takes the target projection in degree i+d.

    source
    theorem MagnitudeConjecture.Graded.VectorGrading.mapPart_mem {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) (d : ℤ) (f : M →ₗ[k] N) {i : ℤ} {x : M} (hx : x ∈ G.component i) :
    (G.mapPart H d f) x ∈ H.component (i + d)
    source
    noncomputable def MagnitudeConjecture.Graded.VectorGrading.mapDegreeSupport {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) [FiniteDimensional k N] :
    Finset ℤ

    The possible degrees of a map are target degrees minus source degrees.

    Instances For
      source
      theorem MagnitudeConjecture.Graded.VectorGrading.mapPart_eq_zero_outside {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) [FiniteDimensional k N] (d : ℤ) (f : M →ₗ[k] N) (hd : d ∉ G.mapDegreeSupport H) :
      G.mapPart H d f = 0
      source
      theorem MagnitudeConjecture.Graded.VectorGrading.sum_shifted_projections {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) [FiniteDimensional k N] (i : ℤ) (hi : i ∈ G.degreeSupport) (y : N) :
      ∑ d ∈ G.mapDegreeSupport H, (H.projection (i + d)) y = y
      source
      theorem MagnitudeConjecture.Graded.VectorGrading.sum_mapPart {k : Type u_1} {M : Type u_2} {N : Type u_3} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] [AddCommGroup N] [Module k N] (G : VectorGrading k M) (H : VectorGrading k N) [FiniteDimensional k N] (f : M →ₗ[k] N) :
      ∑ d ∈ G.mapDegreeSupport H, G.mapPart H d f = f

      The finite homogeneous components reconstruct every linear map.