braiding_tensorUnit_left — Mathlib

English

The braiding between the tensor unit and an object X is the composition of the left unitor with the inverse right unitor, reflecting a standard unit coherence relation.

Русский

braiding между тензорной единицей и объектом X равен композиции левой унитории с обратной правой униторой, отражая стандартную когерентность единицы.

LaTeX

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

Lean4

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

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