English
There exists a finite subset S of M whose closure equals the top submonoid, and S is minimal with this closure property.
Русский
Существует конечное подмножество S ⊆ M такое, что closure S = ⊤ и S минимально по этому свойству.
LaTeX
$$$\\exists S : Finset M, Minimal (\\mathrm{Submonoid.closure} \\; S.toSet = ⊤) S$$$
Lean4
/-- A monoid is finitely generated iff there exists a surjective homomorphism from a `FreeMonoid`
on finitely many generators. -/
@[to_additive /-- A additive monoid is finitely generated iff there exists a surjective homomorphism
from a `FreeAddMonoid` on finitely many generators.-/
]
theorem fg_iff_exists_freeMonoid_hom_surjective :
Monoid.FG M ↔ ∃ (S : Set M) (_ : S.Finite) (φ : FreeMonoid S →* M), Function.Surjective φ :=
by
refine ⟨fun ⟨S, hS⟩ ↦ ⟨S, S.finite_toSet, FreeMonoid.lift Subtype.val, ?_⟩, ?_⟩
· rwa [← MonoidHom.mrange_eq_top, ← Submonoid.closure_eq_mrange]
· rintro ⟨S, hfin : Finite S, φ, hφ⟩
refine fg_iff.mpr ⟨φ '' Set.range FreeMonoid.of, ?_, Set.toFinite _⟩
simp [← MonoidHom.map_mclosure, hφ, FreeMonoid.closure_range_of, ← MonoidHom.mrange_eq_map]
