English
There is a canonical isomorphism between the free group on ι and the coproduct of FreeGroup Unit indexed by ι.
Русский
Существует каноническое изоморфизм между свободной группой на ι и копродуктом FreeGroup Unit по индексу ι.
LaTeX
$$$\mathrm{FreeGroup}(\iota) \cong \mathrm{CoprodI}_{i\in \iota}(\mathrm{FreeGroup}(\mathrm{Unit}))$$$
Lean4
/-- A free group is a free product of copies of the free_group over one generator. -/
@[simps!]
def _root_.freeGroupEquivCoprodI {ι : Type u_1} : FreeGroup ι ≃* CoprodI fun _ : ι => FreeGroup Unit :=
by
refine MonoidHom.toMulEquiv ?_ ?_ ?_ ?_
· exact FreeGroup.lift fun i => @CoprodI.of ι _ _ i (FreeGroup.of Unit.unit)
· exact CoprodI.lift fun i => FreeGroup.lift fun _ => FreeGroup.of i
· ext; simp
· ext i a; cases a; simp
