English
If FiniteType for MonoidAlgebra holds, there exists a finite set G ⊆ M with adjoin of images equal to top.
Русский
Если MonoidAlgebra R M конечного типа, существует конечное множество G ⊆ M, порождающее R[M].
LaTeX
$$$\\exists G: \\mathrm{Finset}(M),\\; \\operatorname{adjoin}_R\\bigl(\\mathrm{of}_R M '' G\\bigr) = \\top$$$
Lean4
/-- If `MonoidAlgebra R M` is of finite type, then there is a `G : Finset M` such that its image
generates, as algebra, `MonoidAlgebra R M`. -/
theorem exists_finset_adjoin_eq_top [h : FiniteType R (MonoidAlgebra 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
