English
Exists f is the left adjoined image-like functor on subobjects given by mono over f.
Русский
Exists f — левый адъюнкт образов подобъектов по отношению к f.
LaTeX
$$$\text{exists } f : \mathrm{Subobject}(X) \to \mathrm{Subobject}(Y)$$$
Lean4
/-- The functor from subobjects of `X` to subobjects of `Y` given by
sending the subobject `S` to its "image" under `f`, usually denoted $\exists_f$.
For instance, when `C` is the category of types,
viewing `Subobject X` as `Set X` this is just `Set.image f`.
This functor is left adjoint to the `pullback f` functor (shown in `existsPullbackAdj`)
provided both are defined, and generalises the `map f` functor, again provided it is defined.
-/
def «exists» (f : X ⟶ Y) : Subobject X ⥤ Subobject Y :=
lower (MonoOver.exists f)
