Rigidity of shifts of finite-dimensional graded spaces

noncomputable def MagnitudeConjecture.Graded.VectorGrading.support {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (G : VectorGrading k M) : Finset ℤ

The exact finite support of the grading.

theorem MagnitudeConjecture.Graded.VectorGrading.mem_support_iff {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (G : VectorGrading k M) (i : ℤ) : i ∈ G.support ↔ G.component i ≠ ⊥

theorem MagnitudeConjecture.Graded.VectorGrading.support_nonempty {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (G : VectorGrading k M) [Nontrivial M] : G.support.Nonempty

theorem MagnitudeConjecture.Graded.VectorGrading.degree_eq_zero_of_injective {k : Type u_1} {M : Type u_2} [Field k] [AddCommGroup M] [Module k M] [FiniteDimensional k M] (G : VectorGrading k M) [Nontrivial M] (d : ℤ) (f : M →ₗ[k] M) (hf : Function.Injective ⇑f) (hdegree : ∀ (i : ℤ), ∀ x ∈ G.component i, f x ∈ G.component (i + d)) : d = 0

An injective homogeneous endomorphism cannot change the degree of a nonzero finite-dimensional graded vector space.