instFullObjPostOfFaithful — Mathlib

English

If F is faithful and full, then (Under.post (X := X) F) is full on objects.

Русский

Если F полного и верного, то Under.post полон на объектах.

LaTeX

$$F is faithful and full ⇒ (Under.post(X) F).Full$$

Lean4

instance [F.Faithful] [F.Full] : (Under.post (X := X) F).Full where
  map_surjective {A B}
    f := by
    obtain ⟨a, ha⟩ := F.map_surjective f.right
    dsimp at a
    have w : A.hom ≫ a = B.hom := F.map_injective <| by simpa [ha] using Under.w f
    exact ⟨Under.homMk a, by ext; simpa⟩

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