English
Finitely generated as a subgroup is equivalent to finitely generated as a submonoid.
Русский
Конечнопорожденность как подгруппы эквивалентна конечнопорожденности как подмонойда.
LaTeX
$$$\forall P : Subgroup G, P.FG \iff P.toSubmonoid.FG$$$
Lean4
/-- A subgroup is finitely generated if and only if it is finitely generated as a submonoid. -/
@[to_additive /-- An additive subgroup is finitely generated if
and only if it is finitely generated as an additive submonoid. -/
]
theorem fg_iff_submonoid_fg (P : Subgroup G) : P.FG ↔ P.toSubmonoid.FG :=
by
constructor
· rintro ⟨S, rfl⟩
rw [Submonoid.fg_iff]
refine ⟨S ∪ S⁻¹, ?_, S.finite_toSet.union S.finite_toSet.inv⟩
exact (Subgroup.closure_toSubmonoid _).symm
· rintro ⟨S, hS⟩
refine ⟨S, le_antisymm ?_ ?_⟩
· rw [Subgroup.closure_le, ← Subgroup.coe_toSubmonoid, ← hS]
exact Submonoid.subset_closure
· rw [← Subgroup.toSubmonoid_le, ← hS, Submonoid.closure_le]
exact Subgroup.subset_closure
