leftUnitor_inv_braiding — Mathlib

English

The inverse left unitor composed with braiding equals a simple braiding-left relation with the unit, expressing a basic coherence between left unitor and braiding.

Русский

Обратная левая унитория с braiding даёт простое тождество левого braiding с единицей, выражая когерентность.

LaTeX

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

Lean4

@[reassoc]
theorem leftUnitor_inv_braiding (X : C) : (λ_ X).inv ≫ (β_ (𝟙_ C) X).hom = (ρ_ X).inv := by simp

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