English
If F is fully faithful, Mono of leftToRight.app X is equivalent to Mono of adj₂.unit.app (F.obj X).
Русский
Если F полнофункторен, монотонность компоненты leftToRight.app X эквивалентна монотонности adj₂.unit.app (F.obj X).
LaTeX
$$$\forall X,\; Mono\big(t.leftToRight.app X\big) \iff Mono\big(t.adj_2.unit.app (F.obj X)\big)$$$
Lean4
/-- The natural transformation `F ⟶ H` for an adjoint triple `F ⊣ G ⊣ H` with `F` and `H`
fully faithful is also equal to the inverse of the whiskered counit `H ⋙ G ⋙ F ⟶ F` of the second
adjunction followed by the whiskered counit `H ⋙ G ⋙ F ⟶ H` of the first. -/
theorem leftToRight_eq_counits :
t.leftToRight =
F.leftUnitor.inv ≫
inv (whiskerRight t.adj₂.counit F) ≫
(Functor.associator _ _ _).hom ≫ whiskerLeft H t.adj₁.counit ≫ H.rightUnitor.hom :=
by
ext X; dsimp [leftToRight]; simp only [Category.id_comp, Category.comp_id, NatIso.isIso_inv_app]
rw [IsIso.comp_inv_eq, Category.assoc, IsIso.eq_inv_comp]
refine Eq.trans ?_ (t.adj₁.counit_naturality <| (whiskerRight t.adj₁.unit H).app X)
rw [whiskerRight_app _ H,
(asIso (t.adj₂.counit.app (G.obj _))).eq_comp_inv.2 (t.adj₂.counit_naturality (t.adj₁.unit.app X)), ←
(asIso _).comp_hom_eq_id.1 <| t.adj₂.left_triangle_components (F.obj X)]
simp
