map_whiskerRight — Mathlib

English

The image under F of the left unitor equals a canonical composite built from δ, whiskering by X, and μ.

Русский

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

LaTeX

$$$$ F(map(\\lambda_X)^{-1}) = δ F (I, X) \\;≫\\; F.obj I \\;\\triangleleft\\; F.map X \\;≫\\; μ F I X $$$$

Lean4

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

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