lift_comp_ι — Mathlib

English

The lift is the unique algebra homomorphism from FreeProduct R A to B that agrees with maps on each A_i.

Русский

Поднятие уникально как гомоморфизм из FreeProduct R A в B, который согласуется с отображениями на каждом A_i.

LaTeX

$$$\forall f:\mathrm{FreeProduct} \,R\,A \to_{R} B,\ \text{if } f\circ ι_i = maps_i \text{ for all } i, \text{ then } f = lift\; maps$$$

Lean4

/-- Universal property of the free product of algebras, property:
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`. -/
@[simp↓]
theorem lift_comp_ι : lift R A maps ∘ₐ ι R A i = maps := by
  ext a
  simp [lift_apply, ι]

Похожие утверждения