epi_rightToLeft_app_iff_epi_map_adj₂_counit_app

English

Another formulation of the same epi equivalence with adj₂.counit.

Русский

Ещё одно формулирование той же эквивалентности эпиморфизмов через counit adj₂.

LaTeX

$$$\forall X,\; \operatorname{Epi}(t.rightToLeft.app X) \iff \operatorname{Epi}\big(F.map\big(t.adj_2.counit.app X\big)\big)$$$

Lean4

/-- For an adjoint triple `F ⊣ G ⊣ H` where `G` is fully faithful, the natural transformation
`H ⟶ F` is epic at `X` iff the image of the counit of the adjunction `G ⊣ H` under `F` is. -/
theorem epi_rightToLeft_app_iff_epi_map_adj₂_counit_app {X : C} :
    Epi (t.rightToLeft.app X) ↔ Epi (F.map (t.adj₂.counit.app X)) := by
  rw [← epi_comp_iff_of_epi (t.adj₁.counit.app (H.obj X)), adj₁_counit_app_rightToLeft_app]

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