epi_rightToLeft_app_iff_epi_map_adj₁_unit_app

English

Same as above without extra hypotheses; epi equivalence holds objectwise.

Русский

То же самое, без дополнительных предположений; эквивалентность эпиморфизмов сохраняется на каждом объекте.

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 unit of the adjunction `F ⊣ G` under `H` is. -/
theorem epi_rightToLeft_app_iff_epi_map_adj₁_unit_app {X : C} :
    Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X)) := by
  rw [← epi_comp_iff_of_isIso _ (t.adj₂.unit.app (F.obj X)), rightToLeft_app_adj₂_unit_app]

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