leftUnitor_tensor_hom — Mathlib

English

The left unitor on X ⊗ Y equals the inverse associator composed with the whiskering of the left unitor on X, expressed as a morphism equality.

Русский

Левый единичный элемент на X ⊗ Y равен композиции обратного ассоциатора и взятия слева от X; выражено как равенство морфизмов.

LaTeX

$$$(\\lambda_{X \\otimes Y})^{\\!\\mathrm{hom}} = α_{I,X,Y}^{-1} \\circ (λ_X)^{\\!\\mathrm{hom}} \\triangleright Y$$$

Lean4

@[reassoc]
theorem leftUnitor_tensor_hom (X Y : C) : (λ_ (X ⊗ Y)).hom = (α_ (𝟙_ C) X Y).inv ≫ (λ_ X).hom ▷ Y := by simp

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