map_whiskerLeft — Mathlib

English

The inverse image of the associator under F is a certain composite involving δ, whiskering by tensor, the image associator, and μ.

Русский

Обратный образ ассоциатора под F задаётся композициией из δ, whiskerLeft, μ и инверсии ассоциатора изображения.

LaTeX

$$$$ F(\\alpha_{X Y Z})^{-1} = δ F X (Y ⊗ Z) \\;≫\\; F.obj X \\;\\triangleleft\\; δ F Y Z \\;≫\\; (\\alpha_{F X, F Y, F Z})^{-1} \\;≫\\; μ F X Y \\;\\triangleright\\; F.obj Z \\;≫\\; μ F (X ⊗ Y) Z $$$$

Lean4

@[reassoc]
theorem map_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) : F.map (X ◁ f) = δ F X Y ≫ F.obj X ◁ F.map f ≫ μ F X Z := by simp

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