English
If F is fully faithful, Mono of leftToRight.app X is equivalent to Mono of adj₁.counit.app (H.obj X).
Русский
Если F полнофункторен, Mono(leftToRight.app X) эквивалентно Mono(adj₁.counit.app(H.obj X)).
LaTeX
$$$\forall X,\; Mono \big(t.leftToRight.app X\big) \iff Mono \big(t.adj_1.counit.app (H.obj X)\big)$$$
Lean4
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `F ⟶ H` is componentwise monic iff the natural transformation `G ⋙ F ⟶ G ⋙ H`
obtained from the units and counits of the adjunctions is.
Note that unlike `epi_rightToLeft_app_iff`, this equivalence does not make sense
on a per-object basis because the components of the two natural transformations are indexed by
different categories. -/
theorem mono_leftToRight_app_iff :
(∀ X, Mono (t.leftToRight.app X)) ↔ ∀ X, Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X) :=
by
refine ⟨fun h X ↦ by rw [← leftToRight_app_obj]; exact h _, fun h X ↦ ?_⟩
rw [mono_leftToRight_app_iff_mono_adj₂_unit_app]
simpa using h (F.obj X)
