Isomorphisms of free products of monoids

A family of isomorphisms M i ≃* N i induces an isomorphism CoprodI M ≃* CoprodI N of the free products, acting on each factor by the given isomorphism. This is the indexed counterpart of Mathlib's MulEquiv.coprodCongr for the free product of two monoids. It is used to rewrite a free product of fundamental groups one factor at a time, for instance to recognise the fundamental group of a wedge of circles as a free group.

Main declarations

• MulEquiv.coprodICongr: the isomorphism of free products induced by a family of isomorphisms.

def MulEquiv.coprodICongr {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Monoid (M i)] [(i : ι) → Monoid (N i)] (e : (i : ι) → M i ≃* N i) : Monoid.CoprodI M ≃* Monoid.CoprodI N

A family of isomorphisms of monoids M i ≃* N i induces an isomorphism of their free products, acting on the i-th factor by the i-th isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MulEquiv.coprodICongr_apply_of {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Monoid (M i)] [(i : ι) → Monoid (N i)] (e : (i : ι) → M i ≃* N i) {i : ι} (m : M i) : (coprodICongr e) (Monoid.CoprodI.of m) = Monoid.CoprodI.of ((e i) m)

@[simp]

theorem MulEquiv.coprodICongr_symm {ι : Type u_1} {M : ι → Type u_2} {N : ι → Type u_3} [(i : ι) → Monoid (M i)] [(i : ι) → Monoid (N i)] (e : (i : ι) → M i ≃* N i) : (coprodICongr e).symm = coprodICongr fun (i : ι) => (e i).symm