The degree filtration of a symmetric algebra and its grading

The degree filtration of SymmetricAlgebra R M is the word filtration TauCeti.Algebra.wordFiltration of the generator map: its k-th step is spanned by the products of at most k generators. Since every such product is homogeneous of degree at most k, an element of the k-th step has no homogeneous component of degree above k (TauCeti.SymmetricAlgebra.coe_decompose_eq_zero_of_mem_wordFiltration). In particular a nonzero homogeneous element of degree n does not have degree below n (TauCeti.SymmetricAlgebra.disjoint_homogeneousSubmodule_wordFiltrationPrevious), which is how leading terms are read off in degree inductions on the symmetric algebra.

Main results

• TauCeti.SymmetricAlgebra.coe_decompose_eq_zero_of_mem_wordFiltration: an element of degree at most k has zero homogeneous component in every degree above k.
• TauCeti.SymmetricAlgebra.disjoint_homogeneousSubmodule_wordFiltrationPrevious: the homogeneous elements of degree n meet the elements of degree below n only in zero.

theorem TauCeti.SymmetricAlgebra.coe_decompose_eq_zero_of_mem_wordFiltration {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] {k n : ℕ} (hkn : k < n) {x : SymmetricAlgebra R M} (hx : x ∈ Algebra.wordFiltration (SymmetricAlgebra.ι R M) k) : ↑(((DirectSum.decompose (homogeneousSubmodule R M)) x) n) = 0

An element of degree at most k has no homogeneous component above k: if x lies in the k-th step of the degree filtration of the symmetric algebra and k < n, then the degree-n homogeneous component of x is zero.

theorem TauCeti.SymmetricAlgebra.disjoint_homogeneousSubmodule_wordFiltrationPrevious {R : Type u} {M : Type v} [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : Disjoint (homogeneousSubmodule R M n) (Algebra.wordFiltrationPrevious (SymmetricAlgebra.ι R M) n)

A homogeneous element of degree n has degree below n only if it is zero: the degree-n homogeneous submodule of the symmetric algebra is disjoint from the step of the degree filtration preceding degree n.