instEssSurjObjCompPostOfFull — Mathlib

English

If G : C → D is full, then the functor post S F G : (S, F) ⥤ (G(S), F ∘ G) is essentially surjective on objects.

Русский

Если G : C → D полнофидична, то отображение post S F G : (S, F) ⥤ (G(S), F ∘ G) по объектам является эссенциально сюръективным.

LaTeX

$$$\\mathrm{EssSurj}(\\text{post } S\\, F\\, G)$$$

Lean4

instance (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] : (post S F G).EssSurj where
  mem_essImage h := ⟨mk (G.preimage h.hom), ⟨isoMk (Iso.refl _) (by simp)⟩⟩

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