precompose_map_leftUnitor — Mathlib

English

Let X, Y be categories and U : X ⥤ Y. The map (precompose F G).map U.leftUnitor.hom is equal to a canonical composite involving precomposeObjComp with the identity on X and the left unitor on F G, illustrating compatibility with the left unit of the precomposition

Русский

Пусть X, Y — категории, U : X ⥤ Y. Отображение (precompose F G).map U.leftUnitor.hom равно канонической композиции, включающей precomposeObjComp с единицей на X и левый унитор на F G, демонстрирующей совместимость с левым унитором предкомпонования.

LaTeX

$$$ (\\text{precompose } F G).map (U.leftUnitor.hom) = (\\text{precomposeObjComp } F G \\,(U)) .hom \\\\circ \\\\ \\mathrm{whiskerLeft}(\\text{precompose } F G |>.obj U)(\\text{precomposeObjId } F G X).hom \\\\circ \\\\ (\\text{Functor.rightUnitor } _).hom $$$

Lean4

theorem precompose_map_leftUnitor (U : X ⥤ Y) :
    (precompose F G).map U.leftUnitor.hom =
      (precomposeObjComp F G (𝟭 _) U).hom ≫
        whiskerLeft (precompose F G |>.obj U) (precomposeObjId F G X).hom ≫ (Functor.rightUnitor _).hom :=
  by cat_disch

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