rightUnitor_inv_braiding — Mathlib

English

The right unitor inversely composed with braiding equals a standard left-unitor relation for the object, encoding the compatibility of braiding with right unitality.

Русский

Обратная правой унитории композиция с браидингом эквивалентна стандартному отношению левой унитории, кодируя совместимость braiding с правой единицей.

LaTeX

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

Lean4

@[reassoc]
theorem rightUnitor_inv_braiding (X : C) : (ρ_ X).inv ≫ (β_ X (𝟙_ C)).hom = (λ_ X).inv :=
  by
  apply (cancel_mono (λ_ X).hom).1
  simp only [assoc, braiding_leftUnitor, Iso.inv_hom_id]

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