rightUnitor_tensor_hom — Mathlib

English

The right unitor on X ⊗ Y is given by the associator and whiskering with the right unitor on Y; a coherence statement tying ρ and α.

Русский

Правый унитор на X ⊗ Y выражается через ассоциатор и правый унитор на Y; это согласование между ρ и α.

LaTeX

$$$(\\rho_{X \\otimes Y})^{\\mathrm{hom}} = α_{X,Y, I}^{\\mathrm{hom}} ∘ (\\mathrm{whiskerLeft}\\; X\\; (\\rho_Y)^{\\mathrm{hom}})$$$

Lean4

@[reassoc]
theorem rightUnitor_tensor_hom (X Y : C) : (ρ_ (X ⊗ Y)).hom = (α_ X Y (𝟙_ C)).hom ≫ X ◁ (ρ_ Y).hom := by simp

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