associator_inv_naturality — Mathlib

English

A slight variant of the triangle identity equating a whiskered left unitor with a composition involving the associator and right unitor.

Русский

Небольшая вариация треугольной идентичности, приравнивающая левый унитор через обрамление к композиции с ассоциатором и правым унитором.

LaTeX

$$$$ (ρ_X)^{-1} \triangleright Y \circ (α_{X, 𝟙, Y}).hom = X \triangleleft (λ_Y)^{-1} $$$$

Lean4

@[reassoc]
theorem associator_inv_naturality {X Y Z X' Y' Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z') :
    (f ⊗ₘ g ⊗ₘ h) ≫ (α_ X' Y' Z').inv = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) := by simp [tensorHom_def]

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