associator_naturality_left — Mathlib

English

Naturality of associator on the left: for f: X ⟶ X', and Y, Z, the morphism f ▷ Y ▷ Z composed with α_{X' Y Z}.hom equals α_{X Y Z}.hom composed with f ▷ (Y ⊗ Z).

Русский

Естественность ассоциатора слева: для f: X ⟶ X' выполняется f ▷ Y ▷ Z ∘ α_{X' Y Z} = α_{X Y Z} ∘ f ▷ (Y ⊗ Z).

LaTeX

$$$ f \triangleright Y \triangleright Z \; \circ \alpha_{X' Y Z}^{\mathrm{hom}} = \alpha_{X Y Z}^{\mathrm{hom}} \circ f \triangleright (Y \otimes Z). $$$

Lean4

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

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