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