English
The app of the η natural transformation for a given localized adjunction equals a composite built from the inverse isomorphisms G' and G and the counit.
Русский
Применение натрансформации η для локализованной адъукции равно композиции обратных изоморфизмов G' и G и единицы.
LaTeX
$$$\\eta\\,adj\,L_1\,L_2\,W_2\,G'\\,F'\\text{ satisfies explicit composite formula.}$$$
Lean4
theorem η_app (X₂ : C₂) :
(η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
(CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂) :=
by
letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso.symm
simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso_inv_app, whiskerRight_app,
Functor.rightUnitor_inv_app, comp_id, assoc]
