mono_leftToRight_app_iff_mono_adj₁_counit_app

English

The op of leftToRight equals leftToRight in the opposite setting.

Русский

Опперация leftToRight равна преобразованию в противоположной обстановке.

LaTeX

$$$t.op.leftToRight = NatTrans.op t.leftToRight$$$

Lean4

/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `F ⟶ H` is monic at `X` iff the counit of the adjunction `F ⊣ G` is monic
at `H.obj X`. -/
theorem mono_leftToRight_app_iff_mono_adj₁_counit_app {X : C} :
    Mono (t.leftToRight.app X) ↔ Mono (t.adj₁.counit.app (H.obj X)) := by
  rw [← map_adj₂_counit_app_leftToRight_app, mono_comp_iff_of_isIso]

Похожие утверждения