submodule_span_single — Mathlib

English

For a fixed n0, F.submodule equals the span of the first n0 levels if and only if for all n ≥ n0, I • F.N(n) = F.N(n+1).

Русский

Для фиксированного порога n0 равенство подмодуля фильтрации F.submodule и соответствующей конечной суммы порождено тем, что для всех n ≥ n0 выполняется I • F.N(n) = F.N(n+1).

LaTeX

$$$F.submodule = \\operatorname{span}(_{\\le n_0}(\\{ \\mathrm{single}_R(i) '' (F.N(i) : Set M) \\})) \\iff \\forall n \\ge n_0,\\ I \\cdot F.N(n) = F.N(n+1).$$$

Lean4

theorem submodule_span_single : Submodule.span (reesAlgebra I) (⋃ i, single R i '' (F.N i : Set M)) = F.submodule :=
  by
  rw [← Submodule.span_closure, submodule_closure_single, Submodule.coe_toAddSubmonoid]
  exact Submodule.span_eq (Filtration.submodule F)

Похожие утверждения