English
There is a universal property: a family fi of monoid homomorphisms fi: M_i →* N corresponds to a unique monoid homomorphism CoprodI(M) →* N, given by lifting across all summands.
Русский
Существует универсальное свойство: семейство fi: M_i →* N эквивалентно единому гомоморфизму CoprodI(M) →* N, получаемому протягиванием через все слагаемые.
LaTeX
$$$ (\\forall i, M_i \\to* N) \\cong (CoprodI(M) \\to* N) $ via lift fi.$$
Lean4
/-- A map out of the free product corresponds to a family of maps out of the summands. This is the
universal property of the free product, characterizing it as a categorical coproduct. -/
@[simps symm_apply]
def lift : (∀ i, M i →* N) ≃ (CoprodI M →* N)
where
toFun
fi :=
Con.lift _ (FreeMonoid.lift fun p : Σ i, M i => fi p.fst p.snd) <|
Con.conGen_le <| by
simp_rw [Con.ker_rel]
rintro _ _ (i | ⟨x, y⟩) <;> simp
invFun f _ := f.comp of
left_inv := by
intro fi
ext i x
rfl
right_inv := by
intro f
ext i x
rfl
