\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{interactions of images and pre-images with unions and intersections}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{introduction}{Introduction}\dotfill \pageref*{introduction} \linebreak
\noindent\hyperlink{statements}{Statements}\dotfill \pageref*{statements} \linebreak
\noindent\hyperlink{proofs_via_adjoints}{Proofs via adjoints}\dotfill \pageref*{proofs_via_adjoints} \linebreak
\noindent\hyperlink{direct_images_preserve_unions_inverse_images_preserve_intersections}{Direct images preserve unions, inverse images preserve intersections}\dotfill \pageref*{direct_images_preserve_unions_inverse_images_preserve_intersections} \linebreak
\noindent\hyperlink{inverse_images_preserve_unions_codirect_images_preserve_intersections}{Inverse images preserve unions, codirect images preserve intersections}\dotfill \pageref*{inverse_images_preserve_unions_codirect_images_preserve_intersections} \linebreak
\noindent\hyperlink{projection_formula}{Projection formula}\dotfill \pageref*{projection_formula} \linebreak
\noindent\hyperlink{related_statements}{Related statements}\dotfill \pageref*{related_statements} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{introduction}{}\subsection*{{Introduction}}\label{introduction}

There is a battery of little [[set theory|set-theoretic]] [[lemmas]] which inevitably recur when laying the [[foundations]] of core [[mathematics]], as when teaching the standard curriculum that includes basic [[topology]], real [[analysis]], [[algebra]], and so forth. In this article we collect some of those core results having to do with the properties of [[image]] and [[pre-image]] operators, especially regarding their preservation (or not) of set-theoretic operations like [[unions]] and [[intersections]].

The attitude and approach of the mathematics professor toward such routine bread-and-butter issues is a matter of some interest. A professional, upon being presented with any one of these ``naive set theory'' [[propositions]], will probably be able to verify it on the spot using ordinary follow-your-nose logic, driven by the definitions. While being able to produce such verifications is part of basic training in mathematics, it is not quite the same as giving an \emph{explanation}, and in fact even good mathematicians trained this way may struggle to remember ``now which is it that direct images preserve, unions or intersections?''\footnote{There is a famous story of how [[Mikhail Yakovlevich Suslin|Suslin]] discovered an error in an argument of [[Lebesgue]], concerning just this type of routine set-theoretic detail (that Lebesgue perhaps just misremembered). In response, [[Mikhail Yakovlevich Suslin|Suslin]] was led to develop some of the basics of [[descriptive set theory]]. Details of the story have been told by Dave Renfro, \href{http://mathforum.org/kb/message.jspa?messageID=4966721}{here} and \href{http://mathforum.org/kb/message.jspa?messageID=4967733}{here}} 

A strong pedagogy would not only instill this sort of basic training, but make the battery of routine results more memorable by concentrating their essence in one or two basic principles that provide an explanatory basis for the rest. According to \hyperlink{Lawvere69}{Lawvere 69}, \hyperlink{Lawvere05}{Lawvere 05}, logic is an interlocking system of certain types of [[adjoint functors]], and we believe putting those [[adjunction|adjoint]] relationships front and center and seeing how the rest flows from them is an effective way to arrange the facts.

\hypertarget{statements}{}\subsection*{{Statements}}\label{statements}

\begin{prop}
\label{PreservationOfUnionsAndIntersectionsOfSets}\hypertarget{PreservationOfUnionsAndIntersectionsOfSets}{}
\textbf{([[images]] preserve [[unions]] but not in general [[intersections]])}

Let $f \colon X \longrightarrow Y$ be a [[function]] between [[sets]]. Let $\{S_i \subset X\}_{i \in I}$ be a set of [[subsets]] of $X$. Then

\begin{enumerate}%
\item $im_f\left( \underset{i \in I}{\cup}  S_i\right) = \left(\underset{i \in I}{\cup} im_f(S_i)\right)$ (the [[image]] under $f$ of a [[union]] of subsets is the union of the images)


\item $im_f\left( \underset{i \in I}{\cap}  S_i\right) \subset \left(\underset{i \in I}{\cap} im_f(S_i)\right)$ (the [[image]] under $f$ of the [[intersection]] of the subsets is contained in the intersection of the images).



\end{enumerate}
The [[injective function|injection]] in the second item is in general proper. If $f$ is an [[injective function]] then this is a [[bijection]]:

\begin{itemize}%
\item $(f\,\text{injective}) \Rightarrow \left(im_f\left( \underset{i \in I}{\cap}  S_i\right) = \left(\underset{i \in I}{\cap} im_f(S_i)\right)\right)$

\end{itemize}
\emph{provided} that $I$ is [[inhabited set|inhabited]].

\end{prop}
\begin{prop}
\label{PreImagePreservesUnionsAndIntersections}\hypertarget{PreImagePreservesUnionsAndIntersections}{}
\textbf{(pre-images preserve unions and intersections)}

Let $f \colon X \longrightarrow Y$ be a [[function]] between [[sets]]. Let $\{T_i \subset Y\}_{i \in I}$ be a set of [[subsets]] of $Y$. Then

\begin{enumerate}%
\item $f^{-1}\left( \underset{i \in I}{\cup}  T_i\right) = \left(\underset{i \in I}{\cup} f^{-1}(T_i)\right)$ (the [[pre-image]] under $f$ of a [[union]] of subsets is the union of the pre-images),


\item $f^{-1}\left( \underset{i \in I}{\cap}  T_i\right) = \left(\underset{i \in I}{\cap} f^{-1}(T_i)\right)$ (the [[pre-image]] under $f$ of the [[intersection]] of the subsets is contained in the intersection of the pre-images).



\end{enumerate}
\end{prop}
\begin{prop}
\label{}\hypertarget{}{}
\textbf{(projection formula)} Let $f: X \longrightarrow Y$ be a [[function]] between [[sets]]. Let $S \subset X$ be a [[subset]] of $X$, and $T \subseteq Y$ be a subset of $Y$. Then

\begin{displaymath}
f(S) \cap T = f(S \cap f^{-1}(T)).
\end{displaymath}
\end{prop}
\hypertarget{proofs_via_adjoints}{}\subsection*{{Proofs via adjoints}}\label{proofs_via_adjoints}

The properties 1., 2. of Proposition \ref{PreservationOfUnionsAndIntersectionsOfSets} may be proved by appeal to fundamental relationships between [[direct image]] and [[inverse image]] and the like, which [[category theory|category theorists]] call [[adjunctions]] (similar in form to adjoints in linear algebra). The advantage of this type of proof is that, despite its utter simplicity, it generalizes to much wider contexts (beyond elementary classical set theory).

\hypertarget{direct_images_preserve_unions_inverse_images_preserve_intersections}{}\subsubsection*{{Direct images preserve unions, inverse images preserve intersections}}\label{direct_images_preserve_unions_inverse_images_preserve_intersections}

The first such relationship is that, for all subsets $S \subseteq X$ and $T \subseteq Y$, we have

\begin{displaymath}
f(S) \subseteq T \qquad iff \qquad S \subseteq f^{-1}(T)
\end{displaymath}
One says in this situation that the direct image mapping $f(-)$ is \emph{[[left adjoint]]} to the inverse image mapping $f^{-1}(-)$, or that inverse image is \emph{[[right adjoint]]} to direct image. This terminology is guided by the formally similar usage in linear algebra where linear mappings $A$ and $B$ are adjoint if one has an equation

\begin{displaymath}
\langle A x, y \rangle = \langle x, B y \rangle
\end{displaymath}
for all $x, y$ in suitable [[inner product spaces]] (and in fact the analogy is not idle; see for instance \hyperlink{JB97}{Baez}).

In that case, we have the following elementary inferences:

\begin{displaymath}
\itexarray{
\bigcup_{i \in I} f(S_i) \subseteq T & iff & (\forall_{i \in I})\; f(S_i) \subseteq T \\ 
 & iff & (\forall_{i \in I})\; S_i \subseteq f^{-1}(T) \\ 
 & iff & \bigcup_{i \in I} S_i \subseteq f^{-1}(T) \\ 
 & iff & f\left(\bigcup_{i \in I} S_i\right) \subseteq T
}
\end{displaymath}
where the first and third lines use the defining [[universal property|property]] of unions. Then, putting $T = \bigcup_{i \in I} f(S_i)$ and reasoning forward, we get $f\left(\bigcup_{i \in I} S_i\right) \subseteq \bigcup_{i \in I} f(S_i)$. On the other hand, putting $T = f\left(\bigcup_{i \in I} S_i\right)$ and reasoning backward, we get $\bigcup_{i \in I} f(S_i) \subseteq f\left(\bigcup_{i \in I} S_i\right)$. These two inclusions together give $\bigcup_{i \in I} f(S_i) = f\left(\bigcup_{i \in I} S_i\right)$.

The [[duality|dual]] of this proof immediately gives the fact that inverse images preserve arbitrary intersections, but let us spell it out directly:

\begin{displaymath}
\itexarray{
S \subseteq \bigcap_{i \in I} f^{-1}(T_i) & iff & (\forall_{i \in I})\; S \subseteq f^{-1}(T_i) \\ 
 & iff & (\forall_{i \in I})\; f(S) \subseteq T_i \\ 
 & iff & f(S) \subseteq \bigcap_{i \in I} T_i \\ 
 & iff & S \subseteq f^{-1}\left(\bigcap_{i \in I} T_i \right)
}
\end{displaymath}
and again by using the reasoning forward/backward trick, we infer $\bigcap_{i \in I} f^{-1}(T_i) = f^{-1}\left(\bigcap_{i \in I} T_i\right)$.

\begin{remark}
\label{}\hypertarget{}{}
The ``reasoning forward/backward trick'' may be summarized by saying that in a [[poset]], we have $A = B$ iff ($A \leq T \Leftrightarrow B \leq T$), or dually that $A = B$ iff ($S \leq A \Leftrightarrow S \leq B$). This trick is vastly extrapolated by the [[Yoneda lemma]].

\end{remark}
\begin{remark}
\label{Lawvere}\hypertarget{Lawvere}{}
People who work with categorial forms of logic denote direct images $f(S)$ by $\exists_f(S)$. The suggestion is to view [[existential quantifier|existential quantification]] as corresponding to taking of a [[direct image]]. For example, given a property $P$ of pairs $(x, y)$, i.e. a subset $P \subseteq X \times Y$ where we write $P(x, y)$ to say $(x, y) \in P$ holds, the set of $y$ such that $(\exists_{x \in X})\; P(x, y)$ holds is exactly the direct image $\pi_2(P)$ under the [[projection map]] $\pi_2: X \times Y \to Y$. This suggests furthermore a useful extended meaning of existential quantification, by considering direct images along more general maps, not just projection maps. With this in mind, category theorists often denote $f(S) = \{y \in Y: (\exists_{x: f(x) = y})\; x \in S\}$ by $\exists_f(S)$, giving an operator $\exists_f: P(X) \to P(Y)$ between [[power sets]]. This is [[left adjoint]] to the taking of [[inverse images]] $T \mapsto f^{-1}(T)$ as an operator $f^{-1}: P(Y) \to P(X)$, also denoted by $f^\ast: P(Y) \to P(X)$. The adjointness relationship between direct image and inverse image, denoted by $\exists_f \dashv f^\ast$, is an example of a famous slogan due to [[Lawvere]]: ``Logical quantification is adjoint to substitution'' (with resonances far beyond the purview of logic as ordinarily conceived; see Remark \ref{MoreJargon}).

\end{remark}
As for direct images and intersections, we have

\begin{displaymath}
f\left(\bigcap_{i \in I} S_i\right) \subseteq \bigcap_{i \in I} f(S_i)
\end{displaymath}
because this is equivalent to $(\forall_{i \in I})\; f\left(\bigcap_{i \in I} S_i\right) \subseteq f(S_i)$, which is obvious because for all $i \in I$, we have $\bigcap_{i \in I} S_i \subseteq S_i$, and $f(A) \subseteq f(B)$ if $A \subseteq B$.

This inclusion is not usually an equality. For example, in the [[cartesian space]] $\mathbb{R}^2$ with $x y$-coordinates, the [[projection]] $(x, y) \mapsto x$ does not preserve the intersection of the lines $y = 1$ and $y = 2$.

However, if $f: X \to Y$ is injective, then the direct image operator $S \mapsto f(S)$ \emph{does} preserve intersections of subsets $(S_i)_{i \in I}$ indexed over \emph{nonempty} sets $I$. This is not difficult to check once we verify that

\begin{itemize}%
\item For any map $f: X \to Y$ (not necessarily injective) and any subset $T \subseteq Y$, we have $f(X) \cap T = f(f^{-1}(T))$.


\item If $f$ is injective, then for any subset $S \subseteq X$ we have $S = f^{-1}(f(S))$.



\end{itemize}
For then, if $T = \bigcap_{i \in I} f(S_i)$ and $I$ is inhabited, we have for some $i$ that $T \subseteq f(S_i) \subseteq f(X)$, and then

\begin{displaymath}
\itexarray{
T = f(X) \cap T & = & f(f^{-1}(T)) \\ 
 & = & f(f^{-1}(\bigcap_i f(S_i))) \\ 
 & = & f\left(\bigcap_{i \in I} f^{-1}(f(S_i))\right) \\ 
 & = & f\left(\bigcap_{i \in I} S_i\right)
}
\end{displaymath}
which was to be shown.

\hypertarget{inverse_images_preserve_unions_codirect_images_preserve_intersections}{}\subsubsection*{{Inverse images preserve unions, codirect images preserve intersections}}\label{inverse_images_preserve_unions_codirect_images_preserve_intersections}

As for the statement that inverse images of unions are unions of inverse images, it turns out this follows from a second fundamental logical adjunction. For a function $f: X \to Y$ and a subset $U \subseteq X$, define

\begin{displaymath}
\forall_f(U) = \{y \in Y: (\forall_{x: f(x) = y})\; x \in U\}
\end{displaymath}
which is analogous to the formula $\exists_f(S) = f(S) = \{y \in Y: (\exists_{x: f(x) = y})\; x \in S\}$ in Remark \ref{Lawvere}. (Alternatively, in [[classical logic]] where the [[negation]] operator $\neg$ on power sets means complementation, we have $\forall_f = \neg \exists_f \neg$.) Then it is easy to verify a second adjunction

\begin{displaymath}
f^{-1}(T) \subseteq U \qquad iff \qquad T \subseteq \forall_f (U)
\end{displaymath}
The same adjointness proof as used to prove property 1., then shows that the left adjoint part which here is the inverse image operator $f^{-1} = f^\ast: P(Y) \to P(X)$ preserves unions, and that right adjoint part which here is the ``codirect image'' operator $\forall_f: P(X) \to P(Y)$ preserves intersections.

\begin{remark}
\label{MoreJargon}\hypertarget{MoreJargon}{}
In terms of some more [[category theory]] jargon the above situation may be phrased as follows:

Subsets of some set $S$ are the [[(-1)-truncated objects]] in the [[slice category]] $Set_{/S}$ of [[Set]] over $S$. Since [[Set]] is a [[topos]], every [[morphism]], i.e. [[function]] $X \longrightarrow Y$ induces a [[base change]] [[adjoint triple]]

\begin{displaymath}
Set_{/X}
     \underoverset
       {\underset{f^\ast}{\longrightarrow}}
       {\overset{f_!}{\longrightarrow}}
       {\overset{f_\ast}{\longleftarrow}}
  Set_{/Y}
  \,.
\end{displaymath}
Here in the language of [[type theory]]

\begin{enumerate}%
\item the [[left adjoint]] $f_!$ is also called the [[dependent sum]]


\item the middle morphism is also called [[context extension]]


\item the [[right adjoint]] $f_\ast$ is also called the [[dependent product]].



\end{enumerate}
All this restricts to the (-1)-truncated objects by composing the left adjoint with [[(-1)-truncation]]. Then one also says that we are looking at a morphism in a [[hyperdoctrine]] and (under ``[[propositions as types]]'') may think of

\begin{enumerate}%
\item the left adjoint $f_!$ as the [[existential quantifier]] $\exists_f$


\item the right adjoint $f_\ast$ as the [[universal quantifier]] $\forall_f$.



\end{enumerate}
Now the fact that [[left adjoint]] $\exists_f$ preserves [[unions]] is the fact that [[left adjoints preserve colimits]], and the fact that the left- and [[right adjoint]] $f^\ast$ preserves unions and intersections is that in addition [[right adjoints preserve limits]].

\end{remark}
\hypertarget{projection_formula}{}\subsection*{{Projection formula}}\label{projection_formula}

Another useful formula for interactions between images and pre-images and intersections is the projection formula:

\begin{prop}
\label{}\hypertarget{}{}
Let $f: X \to Y$ be a function, and let $S \subseteq X, T \subseteq Y$ be subsets. Then $f(S) \cap T = f(S \cap f^{-1}(T))$.

\end{prop}
\begin{proof}
The easy direction is the inclusion $f(S \cap f^{-1}(T)) \subseteq f(S) \cap T$: by the [[universal property|defining property]] of intersections, it suffices to show $f(S \cap f^{-1}(T)) \subseteq f(S)$ and $f(S \cap f^{-1}(T)) \subset T$. The first is clear since $S \cap f^{-1}(T) \subseteq S$, and $A \subseteq B$ implies $f(A) \subseteq f(B)$. Similarly, $f(S \cap f^{-1}(T)) \subseteq f(f^{-1}(T))$, and $f(f^{-1}(T)) \subseteq T$ since this is equivalent to $f^{-1}(T) \subseteq f^{-1}(T)$ by the adjunction between direct and inverse image.

To be continued.

\end{proof}
\hypertarget{related_statements}{}\subsection*{{Related statements}}\label{related_statements}

\begin{itemize}%
\item [[countable unions of countable sets are countable]]


\item [[limits and colimits by example]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

The slogan of Lawvere on logic and adjoint functors appears in

\begin{itemize}%
\item [[F. William Lawvere]], \emph{An elementary theory of the category of sets}, Proceedings of the National Academy of Science of the U.S.A 52 (1965), 1506-1511. Reprinted in an expanded version, with commentary by Colin McLarty and by Lawvere, in Reprints in Theory and Applications of Categories, No. 11 (2005), pp. 1-35. (\href{http://www.tac.mta.ca/tac/reprints/articles/11/tr11abs.html}{link})

\end{itemize}
based on

\begin{itemize}%
\item [[William Lawvere]], \emph{[[Adjointness in Foundations]]}, (\href{http://www.emis.de/journals/TAC/reprints/articles/16/tr16abs.html}{TAC}), Dialectica 23 (1969), 281-296

\end{itemize}
The story of Lebesgue's slip that projections commute with intersections, in attempting to prove that [[projections]] of [[Borel sets]] are Borel, is well explained here:

\begin{itemize}%
\item Dave L. Renfro, \emph{Mikhail Y. Suslin and Lebesgue's error}, two Mathforum posts dated July 29, 2006 (first post \href{http://mathforum.org/kb/message.jspa?messageID=4966721}{here}).

\end{itemize}
The analogy between adjoint functors and adjoints in linear algebra becomes very strong when jacking up from Hilbert spaces to [[2-Hilbert spaces]]. See

\begin{itemize}%
\item [[John C. Baez]], \emph{Higher-Dimensional Algebra II. 2-Hilbert Spaces}, Advances in Mathematics, Volume 127 Issue 2 (10 May 1997), 125-189. \href{https://doi.org/10.1006/aima.1997.1617}{https://doi.org/10.1006/aima.1997.1617} (\href{http://www.sciencedirect.com/science/article/pii/S0001870897916170}{Elsevier link})

\end{itemize}
[[!redirects images preserve unions]]

[[!redirects the image of an intersection is contained in the intersection of the images]] [[!redirects images of unions are unions of images]]



\end{document}