faithful_R_of_epi_counit_app — Mathlib

English

Let L ⊣ R be an adjunction. If every counit component is an epimorphism, then R is faithful.

Русский

Пусть L ⊣ R — адъюнкция. Если каждый компонент вывода эпи-морфизм, то R верный функтор.

LaTeX

$$$\big(\forall X, \text{Epi}(\varepsilon_X)\big) \Rightarrow \forall X,Y,\ f,g:\ R X \to R Y,\ f=g \Rightarrow f=g$$$

Lean4

/-- If each component of the counit is an epimorphism, then the right adjoint is faithful. -/
theorem faithful_R_of_epi_counit_app [∀ X, Epi (h.counit.app X)] : R.Faithful where
  map_injective {X Y f g}
    hfg := by
    apply Epi.left_cancellation (f := h.counit.app X)
    apply (h.homEquiv (R.obj X) Y).injective
    simpa using hfg

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