English
The coproduct CoprodI G of a family of groups G_i naturally carries a group structure; the inverse, product, and identity are defined componentwise via the universal lift.
Русский
Копродукт CoprodI G семейства групп G_i естественным образом образует группу; обратное, произведение и нейтральный элемент определены компонентно через каноническое поднятие.
LaTeX
$$$ \\text{Group}(\\mathrm{CoprodI} \\; G)$$$
Lean4
instance : Group (CoprodI G) :=
{
inv_mul_cancel := by
intro m
rw [inv_def]
induction m using CoprodI.induction_on with
| one => rw [MonoidHom.map_one, MulOpposite.unop_one, one_mul]
| of m ih =>
change of _⁻¹ * of _ = 1
rw [← of.map_mul, inv_mul_cancel, of.map_one]
| mul x y ihx ihy =>
rw [MonoidHom.map_mul, MulOpposite.unop_mul, mul_assoc, ← mul_assoc _ x y, ihx, one_mul, ihy] }
