English
Let F be an I.Filtration on M and consider the polynomial-module M → M[X] with coefficients in R. The submodule F.submodule consists exactly of those polynomials f with coefficients f(i) lying in F.N(i) for every i.
Русский
Пусть F — I-фильтрация M. Подмодуль F.submodule состоит из таких полиномов f, для которых каждый коэффициент f(i) принадлежит F.N(i) для всех i.
LaTeX
$$$f \\in F.submodule \\iff \\forall i,\\ f(i) \\in F.N(i).$$$
Lean4
/-- The `R[IX]`-submodule of `M[X]` associated with an `I`-filtration. -/
protected noncomputable def submodule : Submodule (reesAlgebra I) (PolynomialModule R M)
where
carrier := {f | ∀ i, f i ∈ F.N i}
add_mem' hf hg i := Submodule.add_mem _ (hf i) (hg i)
zero_mem' _ := Submodule.zero_mem _
smul_mem' r f hf
i := by
rw [Subalgebra.smul_def, PolynomialModule.smul_apply]
apply Submodule.sum_mem
rintro ⟨j, k⟩ e
rw [Finset.mem_antidiagonal] at e
subst e
exact F.pow_smul_le j k (Submodule.smul_mem_smul (r.2 j) (hf k))
