braiding_leftUnitor — Mathlib

English

The braiding with the unit object X together with the left unitor equals the right unitor, expressing the compatibility of braiding with unitors.

Русский

Связь braiding с единицей и левой униторой равна правой униторе, выражая совместимость braiding с единицами.

LaTeX

$$$$ (β_{X, 𝟙})^{hom} \; = \; (λ_X)^{hom} \gg (ρ_X)^{-1}, $$$$

Lean4

@[reassoc]
theorem braiding_leftUnitor (X : C) : (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom = (ρ_ X).hom := by
  rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]

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