uncurry_id_eq_ev

Mathlib.CategoryTheory.Closed.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalClosed.uncurry_id_eq_ev

English

Uncurrying the identity morphism on A ⟶[C] X yields the evaluation morphism at X.

Русский

Развёртывая тождественный морфизм на A ⟶ X, получаем морфизм оценки в точке X.

LaTeX

$$$\mathrm{uncurry}(\mathbf{1}_{A \to X}) = (\mathrm{ihom.ev} A).app X$$$

Lean4

theorem uncurry_id_eq_ev : uncurry (𝟙 (A ⟶[C] X)) = (ihom.ev A).app X := by simp [uncurry_eq]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru