mapWhiskerRight_rightUnitor_hom — Mathlib

English

For F : A ⥤ B, the natural transformation mapWhiskerRight (F.rightUnitor.hom) satisfies a canonical decomposition through mapCompLeft and mapPair.

Русский

Для F : A ⥤ B естественная трансформация mapWhiskerRight (F.rightUnitor.hom) раскладывается через mapCompLeft и mapPair.

LaTeX

$$$\operatorname{mapWhiskerRight}\_ (F.rightUnitor.hom) = (\operatorname{mapCompLeft} C F)^{\mathrm{hom}} \circ \mathrm{whiskerLeft}(\mathrm{mapPairId}.hom) \circ (\mathrm{mapPair} F (\mathbf{1}_C)).rightUnitor.hom$$$

Lean4

theorem mapWhiskerRight_rightUnitor_hom (F : A ⥤ B) :
    mapWhiskerRight F.rightUnitor.hom _ =
      (mapCompLeft C F (𝟭 B)).hom ≫ whiskerLeft (mapPair F _) mapPairId.hom ≫ (mapPair _ (𝟭 C)).rightUnitor.hom :=
  by apply natTrans_ext <;> ext <;> simp [mapCompLeft]

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