δ_comp_whiskerLeft_δ — Mathlib

English

Coherence between δ, the tensor of a map, and the unit η.

Русский

Кохерентность δ, тензорного отображения и единичного η.

LaTeX

$$$δ F X (I) \\circ (f ⊗ η F) = F.map (ρ_X) \\circ (ρ_{F X})^{-1} \\circ f$$$

Lean4

@[reassoc]
theorem δ_comp_whiskerLeft_δ (X Y Z : C) :
    δ F X (Y ⊗ Z) ≫ F.obj X ◁ δ F Y Z =
      F.map (α_ X Y Z).inv ≫ δ F (X ⊗ Y) Z ≫ δ F X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom :=
  by rw [associativity, ← F.map_comp_assoc, Iso.inv_hom_id, Functor.map_id, Category.id_comp]

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