whiskerRight_tensor_symm — Mathlib

English

Symmetry relation for whiskering on the right with a tensor: f ▷ Y ▷ Z equals α hom composed with whiskerRight f on Y⊗Z and the inverse of α on X' after.

Русский

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

LaTeX

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

Lean4

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

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