Grading finitely supported functions by assigned degrees

For an arbitrary assignment g : I → ℤ, InternalGrading.finsupp A g grades the free A-module on I by placing its i-th basis vector in degree g i. A homogeneous element has support in a single fibre of g. No finiteness or injectivity of g is required.

The internal direct sum gives every finitely supported function a unique finite homogeneous decomposition, including when several basis vectors have the same degree. This construction also applies after a linear change of coordinates, via InternalGrading.map.

The construction uses Mathlib's Finsupp.supported submodules and DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top.

noncomputable def TauCeti.InternalGrading.finsupp (A : Type u_1) [Ring A] {I : Type u_2} (g : I → ℤ) : InternalGrading A (I →₀ A)

The internal grading of the free module on I assigning its i-th basis vector degree g i. The degree-p piece consists of functions supported in the fibre of p.

Equations

• TauCeti.InternalGrading.finsupp A g = { piece := fun (p : ℤ) => Finsupp.supported A A {i : I | g i = p}, isInternal := ⋯ }

theorem TauCeti.InternalGrading.finsupp_piece (A : Type u_1) [Ring A] {I : Type u_2} (g : I → ℤ) (p : ℤ) : (finsupp A g).piece p = Finsupp.supported A A {i : I | g i = p}

The homogeneous piece is the supported submodule on the corresponding degree fibre.

@[simp]

theorem TauCeti.InternalGrading.mem_finsupp_piece_iff {A : Type u_1} [Ring A] {I : Type u_2} {g : I → ℤ} {p : ℤ} {c : I →₀ A} : c ∈ (finsupp A g).piece p ↔ ∀ (i : I), c i ≠ 0 → g i = p

A finitely supported function has degree p exactly when every nonzero coordinate has assigned degree p.

theorem TauCeti.InternalGrading.single_mem_finsupp_piece {A : Type u_1} [Ring A] {I : Type u_2} {g : I → ℤ} (i : I) (a : A) : Finsupp.single i a ∈ (finsupp A g).piece (g i)

A single coordinate is homogeneous in its assigned degree, including a zero coefficient.

theorem TauCeti.InternalGrading.single_mem_finsupp_piece_iff {A : Type u_1} [Ring A] {I : Type u_2} {g : I → ℤ} (i : I) (a : A) (p : ℤ) : Finsupp.single i a ∈ (finsupp A g).piece p ↔ a = 0 ∨ g i = p

A single coordinate belongs to a homogeneous piece precisely when its coefficient vanishes or its assigned degree is that of the piece.