braiding_rightUnitor — Mathlib

English

The braiding with the unit object X on the left satisfies a dual relation with the right unitor, expressing another facet of braiding-unit compatibility.

Русский

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

LaTeX

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

Lean4

@[reassoc]
theorem braiding_rightUnitor (X : C) : (β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom = (λ_ X).hom := by
  rw [← whiskerLeft_iff, whiskerLeft_comp, braiding_rightUnitor_aux₂]

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