English
RightToLeft equals a different decomposition into left and right units/counits via associators and whiskers.
Русский
RightToLeft эквивалентно другой разложению через левую и правую единицы/ кауниты с использованием ассоциаторов и whisker-операций.
LaTeX
$$$t.rightToLeft = t.rightToLeft = H.leftUnitor^{-1} \circ inv(whiskerLeft F t.adj_2.unit) \circ (Functor.associator _ _ _).inv \circ whiskerRight t.adj_2.counit F \circ F.leftUnitor.hom$$$
Lean4
/-- The natural transformation `H ⟶ F` for an adjoint triple `F ⊣ G ⊣ H` with `G` fully faithful
is also equal to the inverse of the whiskered counit `H ⋙ G ⋙ F ⟶ H` of the first adjunction
followed by the whiskered counit `H ⋙ G ⋙ F ⟶ F` of the second. -/
theorem rightToLeft_eq_counits :
t.rightToLeft =
H.rightUnitor.inv ≫
inv (whiskerLeft H t.adj₁.counit) ≫
(Functor.associator _ _ _).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom :=
by ext X; apply G.map_injective; simp [rightToLeft]
