English
Let F : A → B and G : C → B be functors, and X, Y, Z objects (categories) with X, Y, Z forming small categories. For any functors U, V : X ⥤ Y and any natural transformation α : U ⟶ V, and any W : Y ⥤ Z, the map induced by precomposition commutes with whiskering on the right; i.e., the natural transformation obtained by precomposing with G and F applied to α and W equals the composite formed from the canonical comparison maps.
Русский
Пусть F : A → B и G : C → B — функторы, имеется три множества категорий X, Y, Z; для любых функторов U, V : X ⥤ Y и натурального преобразования α : U ⟶ V, и для любого W : Y ⥤ Z, отображение, индуцируемое предкомпонованием, commute с правым отождествлением; тождество натурального преобразования, полученного усреднением через (precompose F G), равняется композиции из канонических отображений.
LaTeX
$$$ (\\text{precompose } F G).\\mathrm{map}(\\mathrm{whiskerRight}\\, \\alpha\\, W) \\\\quad= \\\\ (\\text{precomposeObjComp } F G\\, U\\, W)^{\\mathrm{hom}} \\\\\\\\quad\\; \\circ\\; \\mathrm{whiskerLeft}\\Big( (\\text{precompose } F G)^{\\mathrm{obj}} W \\Big)\\Big( (\\,\\text{precompose } F G)^{\\mathrm{map}} \\alpha \\Big) \\\\\\\\quad\\circ\\; (\\text{precomposeObjComp } F G\\, V\\, W)^{\\mathrm{inv}} $$$
Lean4
theorem precompose_map_whiskerRight {U V : X ⥤ Y} (α : U ⟶ V) (W : Y ⥤ Z) :
(precompose F G).map (whiskerRight α W) =
(precomposeObjComp F G U W).hom ≫
whiskerLeft (precompose F G |>.obj W) (precompose F G |>.map α) ≫ (precomposeObjComp F G V W).inv :=
by cat_disch
