prodEquiv — Mathlib

English

There is a natural equivalence between pairs of StarAlgHom A →⋆ₐ[R] B and A →⋆ₐ[R] (B × C).

Русский

Существует естественное эквивалентное соответствие между парами StarAlgHom A →⋆ₐ[R] B и A →⋆ₐ[R] (B × C).

LaTeX

$$$ prodEquiv : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C) ≃ (A →⋆ₐ[R] (B × 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)

Похожие утверждения