English
Let F,G: WalkingReflexivePair ⥤ C be functors and e0: F.obj zero ⟶ G.obj zero, e1: F.obj one ⟶ G.obj one such that the obvious coherence equalities hold. Then for any functor H: C ⥤ D, the whiskering of the natural transformation mkNatTrans e0 e1 by H equals the natural transformation mkNatTrans (H.map e0) (H.map e1) with the same coherence data.
Русский
Пусть F, G: WalkingReflexivePair ⥤ C — пару функторов, и данные e0: F.obj zero ⟶ G.obj zero, e1: F.obj one ⟶ G.obj one удовлетворяют соответствующим условиям совместимости. Тогда для любого H: C ⥤ D композиция (вправое взвешивание) естественного преобразования mkNatTrans e0 e1 на H равна естественному преобразованию mkNatTrans (H.map e0) (H.map e1) с той же связочной информацией.
LaTeX
$$$\\mathrm{Functor.whiskerRight}(\\mathrm{mkNatTrans}(e_0,e_1),H)=\\mathrm{mkNatTrans}(H.map\,e_0\\,)(H.map\,e_1)\\,\\text{with the coherence data } (h_1,h_2,h_3).$$$
Lean4
theorem whiskerRightMkNatTrans {F G : WalkingReflexivePair ⥤ C} (e₀ : F.obj zero ⟶ G.obj zero)
(e₁ : F.obj one ⟶ G.obj one) {h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left} {h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right}
{h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion} {D : Type u₂} [Category.{v₂} D] (H : C ⥤ D) :
Functor.whiskerRight (mkNatTrans e₀ e₁ : F ⟶ G) H =
mkNatTrans (H.map e₀) (H.map e₁) (by simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₁])
(by simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₂])
(by simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₃]) :=
by ext x; cases x <;> simp
