full_L_of_isSplitEpi_unit_app — Mathlib

English

Let L ⊣ R be an adjunction. If every unit component is a split epi, then L is full.

Русский

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

LaTeX

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

Lean4

/-- If each component of the unit is a split epimorphism, then the left adjoint is full. -/
theorem full_L_of_isSplitEpi_unit_app [∀ X, IsSplitEpi (h.unit.app X)] : L.Full where
  map_surjective {X Y}
    f := by
    use ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y))
    suffices L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y) by simp [this]
    rw [← comp_id (L.map (section_ (h.unit.app Y)))]
    simp only [Functor.comp_obj, Functor.id_obj, ← h.left_triangle_components Y, ← assoc, ← Functor.map_comp,
      IsSplitEpi.id, Functor.map_id, id_comp]

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