English
The generators {of j | j ∈ α} generate the whole presented group; i.e., their subgroup closure is the top subgroup.
Русский
Генераторы порождают всю представленную группу; их замыкание ровно максимальная подпгруппа.
LaTeX
$$$\operatorname{Subgroup.closure} (\{ \mathrm{PresentedGroup}.of(j) : j \in \alpha \}) = \top$$$
Lean4
/-- The generators of a presented group generate the presented group. That is, the subgroup closure
of the set of generators equals `⊤`. -/
@[simp]
theorem closure_range_of (rels : Set (FreeGroup α)) :
Subgroup.closure (Set.range (PresentedGroup.of : α → PresentedGroup rels)) = ⊤ :=
by
have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl
rw [this, Set.range_comp, ← MonoidHom.map_closure (QuotientGroup.mk' _), FreeGroup.closure_range_of, ←
MonoidHom.range_eq_map]
exact MonoidHom.range_eq_top.2 (QuotientGroup.mk'_surjective _)
