associator_naturality_right — Mathlib

English

Naturality of associator on the right: (X ⊗ Y) ◁ f with α-hom equals α-hom with whiskering on Z.

Русский

Естественность ассоциатора справа: (X ⊗ Y) ◁ f с α-ом сохраняется под правым whisker.

LaTeX

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

Lean4

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

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