leftUnitor_tensor_hom'' — Mathlib

English

In a monoidal category, the left unitor on the tensor object X ⊗ Y is equal to the composition of the inverse associator with the tensor of the left unitor on X and the identity on Y, up to reassociation.

Русский

В моноидальной категории левый унитор на тензорный объект X ⊗ Y равен композиции инверсного ассоциатора и тензорного произведения левого унитора на X с тождественным на Y, с учётом перераспределения скобок.

LaTeX

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

Lean4

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

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