instEssSurjObjPostOfFull — Mathlib

English

If F is full and ess-surjective, then (Under.post F) is ess-surjective.

Русский

Если F полная и эс-сюръективна, то Under.post F эс-сюръективен.

LaTeX

$$Under.post F is ess-surjective$$

Lean4

instance [F.Full] [F.EssSurj] : (Under.post (X := X) F).EssSurj where
  mem_essImage
    B := by
    obtain ⟨B', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.right
    obtain ⟨f, hf⟩ := F.map_surjective (B.hom ≫ e.inv)
    exact ⟨Under.mk f, ⟨Under.isoMk e⟩⟩

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