English
Let f: A →ₐ[R] B and g: C →ₐ[R] D be algebra homomorphisms. There exists a product map prodMap f g: A × C →ₐ[R] B × D defined by prodMap f g (a,c) = (f(a), g(c)).
Русский
Пусть f: A →ₐ[R] B и g: C →ₐ[R] D — алгебраические гомоморфизмы. Существует картаprodMap f g: A × C →ₐ[R] B × D, заданная prodMap f g (a,c) = (f(a), g(c)).
LaTeX
$$$$ \\mathrm{prodMap}(f,g): A \\times C \\to_R B \\times D, \\quad (a,c) \\mapsto (f(a), g(c)). $$$$
Lean4
/-- `Prod.map` of two algebra homomorphisms. -/
def prodMap {D : Type*} [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) : A × C →ₐ[R] B × D :=
{ toRingHom := f.toRingHom.prodMap g.toRingHom
commutes' := fun r => by simp [commutes] }
