English
The exponential comparison map is natural in A; for a morphism f:A' → A, the corresponding whiskerings commute as indicated by expComparison_whiskerLeft.
Русский
Сопоставляющее отображение экспоненциального коэффициента естественно по A: для морфизма f:A'→A соответствующие отбивки совместимы.
LaTeX
$$$ \\forall {A,A'} (f: A' \\to A):\\ (\\mathrm{expComparison}(F,A)).\\whiskerBottom(\\mathrm{pre}(F.map f)) = (\\mathrm{expComparison}(F,A')).\\whiskerTop(\\mathrm{pre} f). $$$
Lean4
/-- The exponential comparison map is natural in `A`. -/
theorem expComparison_whiskerLeft {A A' : C} (f : A' ⟶ A) :
(expComparison F A).whiskerBottom (pre (F.map f)) = (expComparison F A').whiskerTop (pre f) :=
by
unfold expComparison pre
have vcomp1 :=
mateEquiv_conjugateEquiv_vcomp (exp.adjunction A) (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))
((prodComparisonNatIso F A).inv) (((curriedTensor D).map (F.map f)))
have vcomp2 :=
conjugateEquiv_mateEquiv_vcomp (exp.adjunction A) (exp.adjunction A') (exp.adjunction (F.obj A'))
(((curriedTensor C).map f)) ((prodComparisonNatIso F A').inv)
rw [← vcomp1, ← vcomp2]
unfold TwoSquare.whiskerLeft TwoSquare.whiskerRight
congr 1
apply congr_arg
ext B
simp only [Functor.comp_obj, curriedTensor_obj_obj, prodComparisonNatIso_inv, NatTrans.comp_app,
Functor.whiskerLeft_app, curriedTensor_map_app, NatIso.isIso_inv_app, Functor.whiskerRight_app, IsIso.eq_inv_comp,
prodComparisonNatTrans_app]
rw [← prodComparison_inv_natural_whiskerRight F f]
simp
