English
Given a family of algebra homomorphisms g_i: B →ₐ[R] A_i, there is a canonical algebra homomorphism g: B →ₐ[R] ∏ i A_i defined by (g x)_i = g_i x.
Русский
Пусть имеется семейство алгебра-хомоморфизмов g_i: B →ₐ[R] A_i; тогда существует канонический алгебрный гомоморфизм g: B →ₐ[R] ∏ i A_i, который на элементе x даёт элемент (g_i x)_i.
LaTeX
$$$ \\Pi\\!\\text{-algHom } g: B \\to_A (\\prod_i A_i),\\qquad (g x)_i = (g_i x) $$$
Lean4
/-- A family of algebra homomorphisms `g i : B →ₐ[R] A i` defines a ring homomorphism
`Pi.algHom g : B →ₐ[R] Π i, A i` given by `Pi.algHom g x i = g i x`. -/
@[simps!]
def algHom {B : Type*} [Semiring B] [Algebra R B] (g : ∀ i, B →ₐ[R] A i) : B →ₐ[R] Π i, A i
where
__ := Pi.ringHom fun i ↦ (g i).toRingHom
commutes' r := by ext; simp
