English
Let R be a commutative semiring and A an R-algebra with a topology. For any B and C which are R-algebras equipped with topologies, there is a natural bijection between pairs of continuous R-algebra homomorphisms A → B and A → C and continuous R-algebra homomorphisms A → B × C, given by (f, g) ↦ f × g, with inverse given by composing with the first and second projections.
Русский
Пусть R — коммутативное полукольцо, A — R-алгебра с топологией. Для любых B и C, являющихся R-алгебрами с топологиями, существует естественная биекция между парами непрерывных R-алгеб-гомоморфизмов A → B и A → C и непрерывными R-алгеб-гомоморфизмами A → B × C, задаваемая отображением (f, g) ↦ f × g, с обратным отображением через проекции fst и snd.
LaTeX
$$$\mathrm{ContinuousAlgHom}_R(A,B) \times \mathrm{ContinuousAlgHom}_R(A,C) \simeq \mathrm{ContinuousAlgHom}_R(A,B\times C)$$$
Lean4
/-- `ContinuousAlgHom.prod` as an `Equiv`. -/
@[simps apply]
def prodEquiv : (A →A[R] B) × (A →A[R] C) ≃ (A →A[R] B × C)
where
toFun f := f.1.prod f.2
invFun f := ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩
