English
There is a natural equivalence between pairs of nonunital star algebra homomorphisms A →⋆ₙₐ[R] B and A →⋆ₙₐ[R] C, and a single homomorphism A →⋆ₙₐ[R] (B × C), given by f,g ↦ f.prod g with inverse h ↦ (fst ∘ h, snd ∘ h).
Русский
Существует естественное эквивалентное соответствие между парами неполных звёздно-алгебра-гомоморфизмов A →⋆ₙₐ[R] B и A →⋆ₙₐ[R] C и одним гомоморфизмом A →⋆ₙₐ[R] (B × C), задаваемым f,g ↦ f.prod g, с обратной стороной h ↦ (fst ∘ h, snd ∘ h).
LaTeX
$$$ prodEquiv : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C) \\simeq (A →⋆ₙₐ[R] (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)
