faithful_L_of_mono_unit_app — Mathlib

English

Let L ⊣ R be an adjunction. If every component of the unit η is a monomorphism, then L is faithful.

Русский

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

LaTeX

$$$\big(\forall X,\ \text{Mono}(\eta_X)\big) \Rightarrow \big(\forall X,Y,f,g,\ L.map f = L.map g \Rightarrow f=g\big)$$$

Lean4

/-- If each component of the unit is a monomorphism, then the left adjoint is faithful. -/
theorem faithful_L_of_mono_unit_app [∀ X, Mono (h.unit.app X)] : L.Faithful where
  map_injective {X Y f g}
    hfg := by
    apply Mono.right_cancellation (f := h.unit.app Y)
    apply (h.homEquiv X (L.obj Y)).symm.injective
    simpa using hfg

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