English
If AddMonoidAlgebra R M is finite type, there exists a finite subset G of M such that the images of G generate R[M].
Русский
Если R[M] конечного типа, то существует конечное подмножество G M, чьи образы порождают R[M].
LaTeX
$$$\\exists G\\; \\text{Finset}(M),\\; \\operatorname{adjoin}_R(\\mathrm{of}'_R M''(G)) = \\top$$$
Lean4
/-- If `R[M]` is of finite type, then there is a `G : Finset M` such that its
image generates, as algebra, `R[M]`. -/
theorem exists_finset_adjoin_eq_top [h : FiniteType R R[M]] : ∃ G : Finset M, Algebra.adjoin R (of' R M '' G) = ⊤ :=
by
obtain ⟨S, hS⟩ := h
letI : DecidableEq M := Classical.decEq M
use Finset.biUnion S fun f => f.support
have : (Finset.biUnion S fun f => f.support : Set M) = ⋃ f ∈ S, (f.support : Set M) := by
simp only [Finset.set_biUnion_coe, Finset.coe_biUnion]
rw [this]
exact support_gen_of_gen' hS
