homEquiv_apply_eq — Mathlib

English

For a fixed A, the forward direction of the adjunction between tensoring with A and the internal hom sends a morphism f: A ⊗ Y → X to its curry; i.e., the hom-equivalence maps f to curry f.

Русский

Для фиксированного A отражение в адъюнкции между тензорингом на A и внутренним гомом равносильно переводит отображение f: A ⊗ Y → X в curry f.

LaTeX

$$$ (\ihom.adjunction A).homEquiv Y X (f) = \mathrm{curry}(f) $$$

Lean4

theorem homEquiv_apply_eq (f : A ⊗ Y ⟶ X) : (ihom.adjunction A).homEquiv _ _ f = curry f :=
  rfl

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