English
If S generates R[M] as an algebra, then the image of the union of supports of elements of S generates R[M].
Русский
Если S порождает R[M] как алгебру, то образ объединения опор элементов S порождает R[M].
LaTeX
$$$\\operatorname{adjoin}_R\\bigl(\\mathrm{of}'_R M''\\bigl(\\bigcup_{f\\in S}(\\operatorname{supp}(f))\\bigr)\\bigr) = \\top$$$
Lean4
/-- If a set `S` generates, as algebra, `R[M]`, then the image of the union of
the 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 (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⊤ :=
by
suffices (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of' R M '' (f.support : Set M)
by
rw [this]
exact support_gen_of_gen hS
simp only [Set.image_iUnion]
