English
For any liftable pair of functors with respect to L and W, the app at L.obj X of the lifted natural transformation equals the prescribed iso composition: hom_L1^X · τ.app X · inv_L2^X.
Русский
Для пар восстанавливаемых функторов относительно L и W компонент приложения при L.obj X от поднятого натуралного преобразования равен композиции гомоморфизма из изоморфиса и τ.app X и обратно.
LaTeX
$$$(\\text{liftNatTrans } L W F_1 F_2 F_1' F_2' \\tau).\\text{app}(L\\,\\mathrm{obj}\\,X) = (\\text{Lifting.iso } L W F_1 F_1').\\mathrm{hom}.app X \\;\\circ\\; \\tau.\\mathrm{app} X \\;\\circ\\; (\\text{Lifting.iso } L W F_2 F_2').inv.\\mathrm{app} X$$$
Lean4
@[simp]
theorem liftNatTrans_app (F₁ F₂ : C ⥤ E) (F₁' F₂' : D ⥤ E) [Lifting L W F₁ F₁'] [Lifting L W F₂ F₂'] (τ : F₁ ⟶ F₂)
(X : C) :
(liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) =
(Lifting.iso L W F₁ F₁').hom.app X ≫ τ.app X ≫ (Lifting.iso L W F₂ F₂').inv.app X :=
congr_app (Functor.map_preimage (whiskeringLeftFunctor' L W E) _) X
