whisker_assoc_symm — Mathlib

English

Symmetry relation for whiskering and associator: X ◁ f ▷ Z equals α^{-1} ∘ (X ◁ f) ▷ Z ∘ α on Y'.

Русский

Относительная симметрия whisker и ассоциатора: X ◁ f ▷ Z = α^{-1} ∘ (X ◁ f) ▷ Z ∘ α на Y'.

LaTeX

$$$ X \triangleleft f \triangleright Z = (\alpha_{X Y Z})^{-1} \circ (X \triangleleft f) \triangleright Z \circ \alpha_{X Y' Z}. $$$

Lean4

@[reassoc]
theorem whisker_assoc_symm (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
    X ◁ f ▷ Z = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z ≫ (α_ X Y' Z).hom := by simp

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