full_R_of_isSplitMono_counit_app — Mathlib

English

Let L ⊣ R be an adjunction. If every counit component is a split mono, then the right adjoint R is full.

Русский

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

LaTeX

$$$\big(\forall X, \text{IsSplitMono}(\varepsilon_X)\big) \Rightarrow \text{Full}(R)$$$

Lean4

/-- If each component of the counit is a split monomorphism, then the right adjoint is full. -/
theorem full_R_of_isSplitMono_counit_app [∀ X, IsSplitMono (h.counit.app X)] : R.Full where
  map_surjective {X Y}
    f := by
    use (retraction (h.counit.app X) ≫ (h.homEquiv (R.obj X) Y).symm f)
    suffices R.map (retraction (h.counit.app X)) = h.unit.app (R.obj X) by simp [this]
    rw [← id_comp (R.map (retraction (h.counit.app X)))]
    simp only [Functor.id_obj, Functor.comp_obj, ← h.right_triangle_components X, assoc, ← Functor.map_comp,
      IsSplitMono.id, Functor.map_id, comp_id]

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