English
The universal property of FreeProduct provides a correspondence between families of algebra homomorphisms from A_i to B and algebra homomorphisms from FreeProduct R A to B.
Русский
Универсальная свойство FreeProduct устанавливает соответствие между семьями гомоморфизмов из A_i в B и осязаемыми гомоморфизмами из FreeProduct R A в B.
LaTeX
$$$\mathrm{lift}:\; (\{i: I\} \to A_i \to_{R}\ B) \simeq (\mathrm{FreeProduct}\; R\; A \to_{R}\ B)$$$
Lean4
/-- Universal property of the free product of algebras:
for every `R`-algebra `B`, every family of maps `maps : (i : I) → (A i →ₐ[R] B)` lifts
to a unique arrow `π` from `FreeProduct R A` such that `π ∘ ι i = maps i`. -/
@[simps]
def lift : ({i : I} → A i →ₐ[R] B) ≃ (FreeProduct R A →ₐ[R] B)
where
toFun
maps :=
RingQuot.liftAlgHom R
⟨TensorAlgebra.lift R <| DirectSum.toModule R I B <| (@maps · |>.toLinearMap), fun x y r ↦ by
cases r with
| id => simp
| prod => simp⟩
invFun π i := π ∘ₐ ι R A i
left_inv
π := by
ext i aᵢ
aesop (add simp [ι, ι'])
right_inv
maps := by
ext i a
aesop (add simp [ι, ι'])
