English
A monoid M is finitely generated iff its monoid algebra R[M] is of finite type over R.
Русский
Моноид M конечен порождён тогда и только тогда, когда R[M] конечного типа над R.
LaTeX
$$$\\mathrm{FiniteType}(R,R[M]) \\iff \\mathrm{FG}(M)$$$
Lean4
/-- An additive monoid `M` is finitely generated if and only if `R[M]` is of
finite type. -/
theorem finiteType_iff_fg [CommRing R] [Nontrivial R] : FiniteType R R[M] ↔ AddMonoid.FG M :=
by
refine ⟨fun h => ?_, fun h => @AddMonoidAlgebra.finiteType_of_fg _ _ _ _ h⟩
obtain ⟨S, hS⟩ := @exists_finset_adjoin_eq_top R M _ _ h
refine AddMonoid.fg_def.2 ⟨S, (eq_top_iff' _).2 fun m => ?_⟩
have hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S)) := by
simp only [hS, top_toSubmodule, Submodule.mem_top]
rw [adjoin_eq_span] at hm
exact mem_closure_of_mem_span_closure hm
