English
Let F : A → B and G : C → B be functors, with X, Y, Z categories, U : X ⥤ Y, V : Y ⥤ Z, and W : Z ⥤ T. For α : U ⟶ V, the map (precompose F G).map (U.associator V W).hom is equal to a specific composite built from precomposeObjComp and whisker transformations, showing compatibility with the associator structure under precomposition.
Русский
Пусть F : A → B и G : C → B — функторы; категории X, Y, Z; U : X ⥤ Y, V : Y ⥤ Z, W : Z ⥤ T; и α : U ⟶ V. Тогда отображение (precompose F G).map (U.associator V W).hom равно определённой композиции, построенной из precomposeObjComp и whisker-трансформаций, что демонстрирует совместимость с ассоциаторной структурой при предкомпоновании.
LaTeX
$$$ (\\text{precompose } F G).map (U.associator V W).hom = (\\text{precomposeObjComp } F G (U \\circ V) W).hom \\\\; \\circ \\\\ \\mathrm{whiskerLeft}(\\text{precompose } F G |>.obj W)(\\text{precomposeObjComp } F G U V).hom \\\\; \\circ \\\\ ((\\text{precompose } F G |>.obj W).associator _ _).inv \\\\; \\circ \\\\ \\mathrm{whiskerRight}(\\text{precomposeObjComp } F G V W).inv(\\text{precompose } F G |>.obj U) \\\\; \\circ \\\\ (\\text{precomposeObjComp } F G _ W).inv $$$
Lean4
theorem precompose_map_associator {T : Type u₇} [Category.{v₇} T] (U : X ⥤ Y) (V : Y ⥤ Z) (W : Z ⥤ T) :
(precompose F G).map (U.associator V W).hom =
(precomposeObjComp F G (U ⋙ V) W).hom ≫
whiskerLeft (precompose F G |>.obj W) (precomposeObjComp F G U V).hom ≫
((precompose F G |>.obj W).associator _ _).inv ≫
whiskerRight (precomposeObjComp F G V W).inv (precompose F G |>.obj U) ≫ (precomposeObjComp F G _ _).inv :=
by cat_disch
