mono_leftToRight_app_iff_mono_adj₂_unit_app

English

Yet another restatement: epi of rightToLeft.app X iff epi of H.map(adj₁.unit.app X).

Русский

Ещё одно утверждение: эпиморфизм rightToLeft.app X эквивалентен эпиморфизму H.map(adj₁.unit.app X).

LaTeX

$$$\forall X,\; \operatorname{Epi}(t.rightToLeft.app X) \iff \operatorname{Epi}\big(H.map( t.adj_1.unit.app X)\big)$$$

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 unit of the adjunction `G ⊣ H` is monic
at `F.obj X`. -/
theorem mono_leftToRight_app_iff_mono_adj₂_unit_app {X : C} :
    Mono (t.leftToRight.app X) ↔ Mono (t.adj₂.unit.app (F.obj X)) := by
  rw [← leftToRight_app_map_adj₁_unit_app, mono_comp_iff_of_mono]

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