homEquivToProd — Mathlib

English

There is a natural bijection between arrows Z → X ⊗ Y and pairs of arrows Z → X and Z → Y; i.e., (Z ⟶ X ⊗ Y) ≃ (Z ⟶ X) × (Z ⟶ Y).

Русский

Существует естественная биекция между стрелами Z → X×Y и парами стрел Z → X и Z → Y; то есть (Z ⟶ X ⊗ Y) ≃ (Z ⟶ X) × (Z ⟶ Y).

LaTeX

$$$ (Z \to X \otimes Y) \simeq (Z \to X) \times (Z \to Y) $$$

Lean4

/-- Universal property of the Cartesian product: Maps to `X ⊗ Y` correspond to pairs of maps to `X`
and to `Y`. -/
@[simps]
def homEquivToProd {X Y Z : C} : (Z ⟶ X ⊗ Y) ≃ (Z ⟶ X) × (Z ⟶ Y)
    where
  toFun f := ⟨f ≫ fst _ _, f ≫ snd _ _⟩
  invFun f := lift f.1 f.2
  left_inv _ := by simp
  right_inv _ := by simp

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