English
If F and H are fully faithful, leftToRight equals the composite built from left unitor, whiskers of counits/units and associators as shown.
Русский
Если F и H полнофункциональны, leftToRight равен композиции, составленной из левого унитора, whisker-операций каунитов/единиц и ассоциаторов, как показано.
LaTeX
$$$t.leftToRight = F.leftUnitor^{-1} \circ inv \big( \mathrm{whiskerRight}(t.adj_2.unit, F) \big) \circ (\mathrm{Functor.associator}\_\_\_).hom \circ whiskerLeft H t.adj_1.counit \circ H.rightUnitor.hom$$$
Lean4
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the components of the
natural transformation `F ⟶ H` at `G` are precisely the components of the natural transformation
`G ⋙ F ⟶ G ⋙ H` obtained from the units and counits of the adjunctions. -/
@[simp, reassoc]
theorem leftToRight_app_obj {X : D} : t.leftToRight.app (G.obj X) = t.adj₁.counit.app X ≫ t.adj₂.unit.app X :=
by
refine (((t.adj₂.homEquiv _ _).apply_symm_apply _).symm.trans ?_).symm
rw [homEquiv_symm_apply, map_comp, Category.assoc, left_triangle_components, homEquiv_apply, leftToRight_app, ←
H.map_inv]
congr
simpa using IsIso.eq_inv_of_hom_inv_id (t.adj₁.right_triangle_components _)
