English
If A ∈ D satisfies that the counit component at A is split epi, then j.essImage A holds.
Русский
Если у A ∈ D компонент counit является разложимым эпиморфом, то A принадлежит essImage j.
LaTeX
$$If [IsSplitEpi ((coreflectorAdjunction j).counit.app A)], then j.essImage A$$
Lean4
theorem mem_essImage_of_counit_isSplitEpi [Coreflective j] {A : D}
[IsSplitEpi ((coreflectorAdjunction j).counit.app A)] : j.essImage A :=
by
let ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
haveI : IsIso (ε.app (j.obj ((coreflector j).obj A))) := Functor.essImage.counit_isIso ((j.obj_mem_essImage _))
have : Mono (ε.app A) := by
refine @mono_of_mono _ _ _ _ _ (ε.app A) (section_ (ε.app A)) ?_
rw [show ε.app A ≫ section_ _ = _ from (ε.naturality (section_ (ε.app A))).symm]
apply mono_comp _ (ε.app (j.obj ((coreflector j).obj A)))
haveI := isIso_of_mono_of_isSplitEpi (ε.app A)
exact (coreflectorAdjunction j).mem_essImage_of_counit_isIso A
