English
Let P be a morphism property on a category T and X an object. The forgetful functor Forget from the Under category over X along P is full; equivalently, for any objects A, B in Under(P) with apex X and any morphism f: Forget(A) → Forget(B) in T, there exists a morphism g: A → B in Under(P)TopX such that Forget(g) = f.
Русский
Пусть P — свойство морфизмов в категории T, и пусть X — объект. Функтор забывания из категории Under(P) над X является полным; эквивалентно: для любых объектов A, B из Under(P) над X и любой морфизм f: Forget(A) → Forget(B) в T существует морфизм g: A → B в Under(P) над X such that Forget(g) = f.
LaTeX
$$$\\text{Forget}_{P,\\top X}:\\mathrm{Under}(P)_{\\top X}\\to T$ is full, i.e. for all $A,B\\in \\mathrm{Under}(P)_{\\top X}$ and all $f:\\forget(A)\\to \\forget(B)$ in $T$, there exists $g:A\\to B$ with $\\forget(g)=f$.$$
Lean4
instance : (Under.forget P ⊤ X).Full :=
inferInstanceAs <| (Comma.forget _ _ _ _ _).Full
