Editing Adjoint functors (section)

====Categorical logic====
* '''Quantification.''' If <math>\phi_Y</math> is a unary predicate expressing some property, then a sufficiently strong set theory may prove the existence of the set <math>Y=\{y\mid\phi_Y(y)\}</math> of terms that fulfill the property. A proper subset <math>T\subset Y</math> and the associated injection of <math>T</math> into <math>Y</math> is characterized by a predicate <math>\phi_T(y)=\phi_Y(y)\land\varphi(y)</math> expressing a strictly more restrictive property. 
:The role of [[Quantifier (logic)|quantifiers]] in predicate logics is in forming propositions and also in expressing sophisticated predicates by closing formulas with possibly more variables. For example, consider a predicate <math>\psi_f</math> with two open variables of sort <math>X</math> and <math>Y</math>. Using a quantifier to close <math>X</math>, we can form the set
::<math>\{y\in Y\mid \exists x.\,\psi_f(x,y)\land\phi_{S}(x)\}</math>
:of all elements <math>y</math> of <math>Y</math> for which there is an <math>x</math> to which it is <math>\psi_f</math>-related, and which itself is characterized by the property <math>\phi_{S}</math>. Set theoretic operations like the intersection <math>\cap</math> of two sets directly corresponds to the conjunction <math>\land</math> of predicates. In [[categorical logic]], a subfield of [[topos theory]], quantifiers are identified with adjoints to the pullback functor. Such a realization can be seen in analogy to the discussion of propositional logic using set theory but the general definition make for a richer range of logics.

:So consider an object <math>Y</math> in a category with pullbacks. Any morphism <math>f:X\to Y</math> induces a functor 
::<math>f^{*} : \text{Sub}(Y) \longrightarrow \text{Sub}(X)</math> 
:on the category that is the preorder of [[subobject | subobjects]]. It maps subobjects <math>T</math> of <math>Y</math> (technically: monomorphism classes of <math>T\to Y</math>) to the pullback <math>X\times_Y T</math>. If this functor has a left- or right adjoint, they are called <math>\exists_f</math> and <math>\forall_f</math>, respectively.<ref>[[Saunders Mac Lane|Mac Lane, Saunders]]; Moerdijk, Ieke (1992) ''Sheaves in Geometry and Logic'', Springer-Verlag. {{ISBN|0-387-97710-4}} ''See page 58''</ref> They both map from <math>\text{Sub}(X)</math> back to <math>\text{Sub}(Y)</math>. Very roughly, given a domain <math>S\subset X</math> to quantify a relation expressed via <math>f</math> over, the functor/quantifier closes <math>X</math> in <math>X\times_Y T</math> and returns the thereby specified subset of <math>Y</math>.

: '''Example''': In <math>\operatorname{Set}</math>, the category of sets and functions, the canonical subobjects are the subset (or rather their canonical injections). The pullback <math>f^{*}T=X\times_Y T</math> of an injection of a subset <math>T</math> into <math>Y</math> along <math>f</math> is characterized as the largest set which knows all about <math>f</math> and the injection of <math>T</math> into <math>Y</math>. It therefore turns out to be (in bijection with) the inverse image <math>f^{-1}[T]\subseteq X</math>.
:For <math>S \subseteq X</math>, let us figure out the left adjoint, which is defined via
::<math>{\operatorname{Hom}}(\exists_f S,T) 
\cong 
{\operatorname{Hom}}(S,f^{*}T),</math>
:which here just means
::<math>\exists_f S\subseteq T
\leftrightarrow 
S\subseteq f^{-1}[T]</math>.

:Consider <math> f[S] \subseteq T </math>. We see <math>S\subseteq f^{-1}[f[S]]\subseteq f^{-1}[T]</math>. Conversely, If for an <math>x\in S</math> we also have <math>x\in f^{-1}[T]</math>, then clearly <math> f(x)\in T </math>. So <math> S \subseteq f^{-1}[T] </math> implies <math> f[S] \subseteq T </math>. We conclude that left adjoint to the inverse image functor <math>f^{*}</math> is given by the direct image. Here is a characterization of this result, which matches more the logical interpretation: The image of <math>S</math> under <math>\exists_f </math> is the full set of <math>y</math>'s, such that <math> f^{-1} [\{y\}] \cap S</math> is non-empty. This works because it neglects exactly those <math>y\in Y</math> which are in the complement of <math>f[S]</math>. So
::<math>
\exists_f S 
= \{ y \in Y \mid \exists (x \in f^{-1}[\{y\}]).\, x \in S \; \}
= f[S].
</math>
:Put this in analogy to our motivation <math>\{y\in Y\mid\exists x.\,\psi_f(x,y)\land\phi_{S}(x)\}</math>.
:The right adjoint to the inverse image functor is given (without doing the computation here) by
::<math>
\forall_f S 
= \{ y \in Y \mid \forall (x \in f^{-1} [\{y\}]).\, x \in S \; \}.
</math>
: The subset <math>\forall_f S</math> of <math>Y</math> is characterized as the full set of <math>y</math>'s with the property that the inverse image of <math>\{y\}</math> with respect to <math>f</math> is fully contained within <math>S</math>. Note how the predicate determining the set is the same as above, except that <math>\exists</math> is replaced by <math>\forall</math>.

:''See also [[powerset]].''