map_leftUnitor — Mathlib

English

The image under F of the left unitor equals a canonical composite involving δ, whiskering by the unit, and μ.

Русский

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

LaTeX

$$$$ F(\\lambda_X) = δ F (I, X) \\;≫\\; F.obj I \\triangleright F.map X \\;≫\\; μ F I X $$$$

Lean4

@[reassoc]
theorem map_leftUnitor (X : C) : F.map (λ_ X).hom = δ F (𝟙_ C) X ≫ η F ▷ F.obj X ≫ (λ_ (F.obj X)).hom := by simp

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