whiskerLeft_δ_μ — Mathlib

English

For any X, Z in C and a morphism f: Y ⟶ Z in C, the map F.map of the whiskered morphism X ⟶ f equals a specific composite built from δ, whiskering by X, and μ.

Русский

Для любого X, Z ∈ C и морфизма f: Y ⟶ Z в C, отображение F.map от whiskerLeft X f равно определённой композиции из δ, whiskerLeft X и μ.

LaTeX

$$$$ F.map( X \\;\\whiskerLeft\\; f ) = δ F X Z \\,≫\, (F.map f) \\;\\whiskerLeft\\; F.obj Z \\,≫\, μ F Y Z $$$$

Lean4

@[reassoc (attr := simp)]
theorem whiskerLeft_δ_μ (X Y : C) (T : D) : T ◁ δ F X Y ≫ T ◁ μ F X Y = 𝟙 _ := by
  rw [← MonoidalCategory.whiskerLeft_comp, δ_μ, MonoidalCategory.whiskerLeft_id]

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