English
Let A,B,C be algebras over a commutative semiring R. There is a natural equivalence between the pair of R-algebra homomorphisms A →ₐ[R] B and A →ₐ[R] C, and the R-algebra homomorphisms A →ₐ[R] (B × C), given by (f,g) ↦ (a ↦ (f(a), g(a))) with inverse h ↦ (fst ∘ h, snd ∘ h).
Русский
Пусть A, B, C — алгебры над коммутативной полукольцом R. Существует естественная эквивалентность между пары R-алгебраических гомоморфизмов A → B и A → C и алгебраическим гомоморфизмом A → B × C, заданная (f,g) ↦ (a ↦ (f(a), g(a))) с обратной стороной h ↦ (fst ∘ h, snd ∘ h).
LaTeX
$$$$ (\\mathrm{AlgHom}_R(A,B) \\times \\mathrm{AlgHom}_R(A,C)) \\cong \\mathrm{AlgHom}_R(A, B \\times C). $$$$
Lean4
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains. -/
@[simps]
def prodEquiv : (A →ₐ[R] B) × (A →ₐ[R] C) ≃ (A →ₐ[R] B × C)
where
toFun f := f.1.prod f.2
invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)
