English
If S generates R[M] as an algebra, then the union of the supports of elements of S, via the natural embedding, generates R[M].
Русский
Если множество S порождает R[M] как алгебру, то объединение опор элементов S порождает R[M].
LaTeX
$$$\\operatorname{adjoin}_R S = \\top \\Rightarrow \\operatorname{adjoin}_R\\bigl(\\bigcup_{f\\in S} \\mathrm{of}'_R M''(\\operatorname{supp}(f))\\bigr) = \\top$$$
Lean4
/-- If a set `S` generates, as algebra, `R[M]`, then the set of supports of
elements of `S` generates `R[M]`. -/
theorem support_gen_of_gen {S : Set 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 : R[M]) (_ : 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)
