leftUnitor_hom

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianMonoidalCategory.leftUnitor_hom

English

For any X, the left unitor hom is the projection snd from I ⊗ X to X; i.e., (λ_X).hom = snd(I, X).

Русский

Для любого объекта X гомоморфизм левого унитора равен проекции snd из I ⊗ X на X; то есть (λ_X).hom = snd(I,X).

LaTeX

$$$(\lambda_X)^{\mathrm{hom}} = \mathrm{snd}(\mathbb{1}, X)$$$

Lean4

theorem leftUnitor_hom (X : C) : (λ_ X).hom = snd _ _ := by simp [snd_def]

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

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

Разделы

Аффилиация

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