English
For any X, Y categories and U : X ⥤ Y, the map (precompose F G).map U.rightUnitor.hom equals a composite built from precomposeObjComp and whiskerRight with the identity on Y and the left and right unitor components, expressing compatibility with the right unitor under precomposition.
Русский
Для категорий X, Y и функторов U : X ⥤ Y отображение (precompose F G).map U.rightUnitor.hom выражается как композиция из precomposeObjComp и whiskerRight с единицей на Y и компонентами левого и правого униторов, демонстрируя совместимость с правым унитором при предкомпоновании.
LaTeX
$$$ (\\text{precompose } F G).map U.rightUnitor.hom = (\\text{precomposeObjComp } F G U (\\mathbf{1})).hom \\\\circ \\\\ \\mathrm{whiskerRight}(\\text{precomposeObjId } F G Y).hom(\\text{precompose } F G |>.obj U) \\\\circ \\\\ (\\mathrm{Functor.leftUnitor } _).hom $$$
Lean4
theorem precompose_map_rightUnitor (U : X ⥤ Y) :
(precompose F G).map U.rightUnitor.hom =
(precomposeObjComp F G U (𝟭 _)).hom ≫
whiskerRight (precomposeObjId F G Y).hom (precompose F G |>.obj U) ≫ (Functor.leftUnitor _).hom :=
by cat_disch
