English
The product of two morphisms f: A → B and g: A → C is a morphism A → B × C defined by a ↦ (f(a), g(a)).
Русский
Произведение двух морфизмов f: A → B и g: A → C задаёт морфизм A → B × C, определённый как a ↦ (f(a), g(a)).
LaTeX
$$$\text{prod}(f,g): A \to_{R} B \times C\quad\text{defined by}\quad (\text{prod}(f,g))(a)=(f(a),g(a)).$$$
Lean4
/-- The prod of two morphisms is a morphism. -/
@[simps]
def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C
where
toFun := Pi.prod f g
map_zero' := by simp only [Pi.prod, Prod.mk_zero_zero, map_zero]
map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add]
map_mul' x y := by simp only [Pi.prod, Prod.mk_mul_mk, map_mul]
map_smul' c x := by simp only [Pi.prod, map_smul, MonoidHom.id_apply, Prod.smul_mk]
