instEssSurjObjPostOfFull — Mathlib

English

If F is full and essentially surjective, then Over.post F is essentially surjective.

Русский

Если F полно и эcсенциально сюръективен, то Over.post F эcсенциально сюръективен.

LaTeX

$$$(F.\\text{Full} \\land F.\\text{EssSurj}) \\Rightarrow \\operatorname{EssSurj}(\\mathrm{Over.post}\\ (X:=X)\, F)$$$

Lean4

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

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