English
The app of the ε natural transformation for a given localized adjunction equals a composite built from unit, isomorphisms F and G, and the forgetful functor.
Русский
Применение натрансформации ε для локализованной адъукции равно композиции, включающей единицу, изоморфизмы F и G и забывающий функтор.
LaTeX
$$$\\epsilon\\,adj\,L_1\,W_1\,L_2\,G'\\,F'\\text{ satisfies explicit composite formula.}$$$
Lean4
theorem ε_app (X₁ : C₁) :
(ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
L₁.map (adj.unit.app X₁) ≫
(CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁) :=
by
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso.symm
simp only [ε, liftNatTrans_app, Lifting.iso, Iso.symm, Functor.id_obj, Functor.comp_obj, Functor.rightUnitor_hom_app,
whiskerRight_app, CatCommSq.hComp_iso_hom_app, id_comp]
