leftUnitor_inv_tensor_id — Mathlib

English

Another coherence relation showing how the left unitor on a tensor object relates to the tensor of left unitor and identity, via associators.

Русский

Еще одно когерентное соотношение, показывающее, как левый унитор на тензорном объекте связан с тензором левого унитора и единицы через ассоциаторы.

LaTeX

$$$ (\\lambda_{X \\otimes Y}).hom = (\\alpha_{\\mathbf{1},X,Y})^{-1} \\circ ((\\lambda_X).hom \\otimes \\mathrm{Id}_Y) $$$

Lean4

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

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