English
Let rels define a presented monoid on α by generators with relations rels. Then the submonoid generated by the images of the generators equals the whole presented monoid.
Русский
Пусть задан представленный моноид на α с образами генераторов и отношениями rels. Тогда порожденный ими подмоноид образов генераторов равен всей представленной моноидальной структурe.
LaTeX
$$$\operatorname{Submonoid.closure}(\operatorname{Set.range}(\operatorname{PresentedMonoid.of}(rel s))) = \top$$$
Lean4
/-- The generators of a presented monoid generate the presented monoid. That is, the submonoid
closure of the set of generators equals `⊤`. -/
@[to_additive (attr := simp) /-- The generators of a presented additive monoid generate the
presented additive monoid. That is, the additive submonoid closure of the set of generators equals
`⊤`. -/
]
theorem closure_range_of (rels : FreeMonoid α → FreeMonoid α → Prop) :
Submonoid.closure (Set.range (PresentedMonoid.of rels)) = ⊤ :=
by
rw [Submonoid.eq_top_iff']
intro x
induction x with
| _ a
induction a with
| one => exact Submonoid.one_mem _
| of x => exact subset_closure <| by simp [range, of]
| mul x y hx hy => exact Submonoid.mul_mem _ hx hy
