English
The submodule selecting elements whose support lies in a fixed grade index via f: M → ι.
Русский
Подмодуль, выделяющий элементы, поддержка которых вложена в фиксированную степень, заданную f: M → ι.
LaTeX
$$$\\text{gradeBy}(f,i) := \\{ a \\in R[M] \\mid \\forall m, m \\in \\operatorname{supp}(a) \\Rightarrow f(m) = i\\}$$$
Lean4
/-- The submodule corresponding to each grade given by the degree function `f`. -/
abbrev gradeBy (f : M → ι) (i : ι) : Submodule R R[M]
where
carrier := {a | ∀ m, m ∈ a.support → f m = i}
zero_mem' m h := by cases h
add_mem' {a b} ha hb m h := by classical exact (Finset.mem_union.mp (Finsupp.support_add h)).elim (ha m) (hb m)
smul_mem' _ _ h := Set.Subset.trans Finsupp.support_smul h
