English
If each component G_i is a group with a distinguished basis B_i, then the free product CoprodI G has a free basis given by the union of the component bases.
Русский
Если каждый G_i — группа с заданной базой B_i, то свободное произведение CoprodI G имеет свободную базу, равную объединению баз компонент.
LaTeX
$$$\text{coprodI}(\{G_i\},\{B_i\}) : \text{FreeGroupBasis}(\Sigma i, X_i)(\mathrm{CoprodI} G)$$$
Lean4
/-- Given a family of free groups with distinguished bases, then their free product is free, with
a basis given by the union of the bases of the components. -/
def coprodI {ι : Type*} {X : ι → Type*} {G : ι → Type*} [∀ i, Group (G i)] (B : ∀ i, FreeGroupBasis (X i) (G i)) :
FreeGroupBasis (Σ i, X i) (CoprodI G) :=
⟨MulEquiv.symm <|
MonoidHom.toMulEquiv (FreeGroup.lift fun x : Σ i, X i => CoprodI.of (B x.1 x.2))
(CoprodI.lift fun i : ι => (B i).lift fun x : X i => FreeGroup.of (⟨i, x⟩ : Σ i, X i)) (by ext; simp)
(by ext1 i; apply (B i).ext_hom; simp)⟩
