id_tensorHom_id — Mathlib

English

The unit constraints of the tensor functor satisfy canonical identities: ε(tensor) equals the inverse left unitor and η(tensor) equals the left unitor itself.

Русский

Единичные констрейнты тензорной функции удовлетворяют каноническим тождествам: ε(tensor) равен обратному левому унитору, η(tensor) равен самому левому унитору.

LaTeX

$$$$ η(tensor C) = (\lambda_{(tensor C)}).hom \quad and \quad ε(tensor C) = (\lambda_{(tensor C)}).inv $$$$

Lean4

theorem id_tensorHom_id (X Y : C) : tensorHom ℬ (𝟙 X) (𝟙 Y) = 𝟙 (tensorObj ℬ X Y) :=
  (ℬ _ _).isLimit.hom_ext <| by rintro ⟨_ | _⟩ <;> simp [tensorHom]

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