Internal gradings transported through homogeneous quotients

A surjective linear map carries an internal direct-sum decomposition to the images of its pieces when its kernel is closed under homogeneous projection. This is the linear-algebra bridge used for Hom spaces of a mesh quotient.

theorem MagnitudeConjecture.Graded.span_isHomogeneous_of_forall_mem_component {k : Type u} [Field k] {M : Type v} [AddCommGroup M] [Module k M] {d : Type z} [DecidableEq d] (A : d → Submodule k M) [DirectSum.Decomposition A] (S : Set M) (hS : ∀ m ∈ S, ∃ (i : d), m ∈ A i) : DirectSum.SetLike.IsHomogeneous A (Submodule.span k S)

The span of a set of homogeneous vectors is a homogeneous submodule.

theorem MagnitudeConjecture.Graded.image_isInternal_of_surjective_of_ker_isHomogeneous {k : Type u} [Field k] {M : Type v} {N : Type w} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {d : Type z} [DecidableEq d] (A : d → Submodule k M) [DirectSum.Decomposition A] (f : M →ₗ[k] N) (hf : Function.Surjective ⇑f) (hker : DirectSum.SetLike.IsHomogeneous A f.ker) : DirectSum.IsInternal fun (i : d) => Submodule.map f (A i)

A surjective linear map whose kernel is homogeneous transports an internal decomposition to the images of its homogeneous pieces.

theorem MagnitudeConjecture.Graded.image_isInternal_of_equiv {k : Type u} [Field k] {M : Type v} {N : Type w} [AddCommGroup M] [Module k M] [AddCommGroup N] [Module k N] {d : Type z} [DecidableEq d] (A : d → Submodule k M) (hA : DirectSum.IsInternal A) (e : M ≃ₗ[k] N) : DirectSum.IsInternal fun (i : d) => Submodule.map (↑e) (A i)

A linear equivalence transports an internal decomposition to the images of its homogeneous pieces.