English
If the image of m in Submodule(span of the closure of S) lies, then m lies in the closure of S.
Русский
Если образ m лежит в span closure S, тогда m лежит в closure S.
LaTeX
$$$\\text{mem}_{\\text{span}}(\\mathrm{of}'_R M m, \\operatorname{Submonoid}.closure(\\mathrm{image}(\\mathrm{of}'_R M))) \\Rightarrow m \\in \\mathrm{closure}(S)$$$
Lean4
/-- If a set `S` generates, as algebra, `MonoidAlgebra R M`, then the set of supports of elements
of `S` generates `MonoidAlgebra R M`. -/
theorem support_gen_of_gen {S : Set (MonoidAlgebra R M)} (hS : Algebra.adjoin R S = ⊤) :
Algebra.adjoin R (⋃ f ∈ S, of R M '' (f.support : Set M)) = ⊤ :=
by
refine le_antisymm le_top ?_
rw [← hS, adjoin_le_iff]
intro f hf
have hincl : (of R M '' f.support) ⊆ ⋃ (g : MonoidAlgebra R M) (H : g ∈ S), (of R M '' g.support) :=
by
intro s hs
exact Set.mem_iUnion₂.2 ⟨f, ⟨hf, hs⟩⟩
exact adjoin_mono hincl (mem_adjoin_support f)
