English
A monoid is finitely generated if and only if there exists a finite set S and a surjective monoid hom from the free monoid on S onto M.
Русский
Моноид FG эквивалентен существованию конечного набора S и сурьективного гомоморфизма от свободного моноида на S к M.
LaTeX
$$$\\text{Monoid.FG } M \\iff \\exists S \\text{ finite}, \\exists \\varphi: \\text{FreeMonoid } S \\to^* M \\text{ surjective}$$$
Lean4
/-- Finite product of finitely generated submonoids is finitely generated. -/
@[to_additive /-- Finite product of finitely generated additive submonoids is finitely generated. -/
]
theorem pi (hP : ∀ i, (P i).FG) : (pi Set.univ P).FG := by
classical
haveI := Fintype.ofFinite ι
choose s hs using hP
refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image, ←
MonoidHom.map_mclosure, hs, iSup_map_mulSingle]
