\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*{Cantor-Schroeder-Bernstein theorem}

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

\noindent\hyperlink{statement}{Statement}\dotfill \pageref*{statement} \linebreak
\noindent\hyperlink{proof}{Proof}\dotfill \pageref*{proof} \linebreak
\noindent\hyperlink{alt}{Alternative construction of a fixed point}\dotfill \pageref*{alt} \linebreak
\noindent\hyperlink{beta_reduced_proof}{Beta reduced proof}\dotfill \pageref*{beta_reduced_proof} \linebreak
\noindent\hyperlink{failure_in_toposes_and_constructive_mathematics}{Failure in toposes and constructive mathematics}\dotfill \pageref*{failure_in_toposes_and_constructive_mathematics} \linebreak
\noindent\hyperlink{in_other_categories}{In other categories}\dotfill \pageref*{in_other_categories} \linebreak
\noindent\hyperlink{name}{Name}\dotfill \pageref*{name} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{statement}{}\subsection*{{Statement}}\label{statement}

The \emph{Cantor--Schroeder--Bernstein} theorem says that the usual [[order relation]] on [[cardinalities]] of [[set]]s is [[antisymmetric relation|antisymmetric]]. In other words, define an order on sets by $X \leq Y$ if there exists a [[monomorphism]] $f\colon X \to Y$. Then, if both $X \leq Y$ and $Y \leq X$, there exists an [[isomorphism]] of sets $X \cong Y$.

The result is really only interesting in the absence of the [[axiom of choice]] ($AC$). With $AC$, it is a trivial corollary of the [[well-ordering theorem]]. However, the theorem actually requires only [[excluded middle]], although it does not hold in [[constructive mathematics]] --- indeed, it is actually \emph{equivalent} to excluded middle (at least assuming the [[axiom of infinity]]).

\hypertarget{proof}{}\subsection*{{Proof}}\label{proof}

We prove that the Cantor--Schroeder--Bernstein theorem holds in a [[Boolean topos]]. The theorem is not however [[intuitionistic logic|intuitionistically]] valid, in that it fails in some [[topos]]es, such as the topos $Set^{\bullet \to \bullet}$ (the [[arrow category]] of $Set$); see Example \ref{counterexample} below.

Throughout we use ordinary [[set theory|set-theoretic]] reasoning which can be translated into the formal theory of toposes. (This can be formalized via the [[Mitchell–Benabou language]], for instance.)

First, let's try a little pedagogy. Somehow functions $h: X \to Y, h^{-1}: Y \to X$ are to be cooked up from injections $f: X \to Y$ and $g: Y \to X$, so we might guess $h$ is to be defined as $f$ at least part of the time, and $h^{-1}$ as $g$ another part of the time. An ideal situation would be to have a set-up

\begin{displaymath}
f: A \stackrel{\sim}{\longrightarrow} B
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
C \stackrel{\sim}{\longleftarrow} D: g
\end{displaymath}
where $A, C$ are complementary subsets in $X$ and $B, D$ are complementary subsets in $Y$; then $h$ could be defined as $f$ on $A$ and as $g^{-1}$ on $C$, and everything works out fine. How can we achieve this?

If we have this situation, then apparently $B = f(A)$ (the direct image of $A$), and $D = \neg B = \neg f(A)$ (the complement of $f(A)$), and then $C = g(D) = g(\neg f(A))$, and finally $A, C$ are required to be complementary, so we would need

\begin{displaymath}
A = \neg g(\neg f(A)).
\end{displaymath}
In other words, $A$ would be a [[fixed point]] of a suitable operation built from direct image and complementation operators. In fact, if we find such a fixed point $A$, then the plan above would work without a hitch.

Perhaps the simplest fixed-point theorem for this purpose on the market is

\begin{lemma}
\label{}\hypertarget{}{}
Let $\phi\colon P X \to P X$ be an order-preserving map. Then there exists $A$ in $P X$ for which $\phi(A) = A$.

\end{lemma}
\begin{proof}
Let $A$ be the (internal) [[intersection]] of $U = \{T \in P X : \phi(T) \leq T\}$. Since $A \leq T$ for every $T$ in $U$, we have $\phi(A) \leq \phi(T) \leq T$ for every $T$ in $U$. Hence $\phi(A) \leq A$ by definition of $A$. Applying $\phi$ again, we get $\phi \phi(A) \leq \phi(A)$. Hence $\phi(A)$ belongs to $U$. But then $A \leq \phi(A)$ by definition of $A$.

\end{proof}
\begin{remark}
\label{term}\hypertarget{term}{}
The preceding proof is valid in \emph{any} topos (and so holds for $Set$ even intuitionistically). It can be seen as a specialization to posets of a result of Lambek on the [[initial algebra|initial]] [[algebra of an endofunctor]], saying that the structure maps of such initial algebras are necessarily isomorphisms. Here the initial algebra $A$ is (by construction) an initial fixed point.

\end{remark}
\begin{proof}
Suppose given two monos $f: X \to Y$, $g: Y \to X$. Let $\exists_f: P X \to P Y$ denote direct image or [[existential quantification]] along $f$, and let $\neg_X: P X \to P X$ denote [[negation]]. Then the composite

\begin{displaymath}
\phi = \neg_X \exists_g \neg_Y \exists_f: P X \to P X
\end{displaymath}
is order-preserving, and so has a fixed point $A$ by the Knaster-Tarski lemma. Now define $h: X \to Y$ by the rule

\begin{displaymath}
\itexarray{
h(x) & = & f(x) & \text{ if }\; x \in A \\
h(x) & = & g^{-1}(x) & \text{ if }\; x \notin A 
}
\end{displaymath}
(the multi-line definition is where we use the Boolean condition). The second line makes sense because $\neg A$ is in the image of $g$. The inverse of $h$ is

\begin{displaymath}
\itexarray{
j(y) & = & f^{-1}(y) & \; \text{if} \; y \in \exists_f(A) \\
j(y) & = & g(y) & \; \text{if} \; y \notin \exists_f(A)
}
\end{displaymath}
That $j$ is inverse to $h$ uses the fact that $\neg A = \exists_g \neg \exists_f(A)$. The rest is obvious.

\end{proof}
This classic proof is substantially the proof given in Johnstone's [[Elephant]], D4.1.11. The Boolean condition is not \emph{strictly speaking} necessary, i.e., the [[principle of excluded middle]] ($EM$) does not logically follow from the Cantor--Schroeder--Bernstein statement since, for example, the latter holds vacuously (every mono is an iso) in the non-Boolean topos

\begin{displaymath}
FinSet^C
\end{displaymath}
where $C$ is any nontrivial [[finite category]]. But $EM$ is certainly the most natural supposition to make. In fact EM does constructively follow from the Cantor-Schroeder-Bernstein statement provided that a [[natural numbers object]] exists; see \hyperlink{PB19}{Pradic and Brown, 2019}.

\hypertarget{alt}{}\subsubsection*{{Alternative construction of a fixed point}}\label{alt}

In some schools of thought, the proof using the Knaster-Tarski lemma would be criticized because that lemma makes use of an [[impredicative]] construction. However, the application made of it in the proof of the CSB theorem is only to ensure that the operator $\neg_X \exists_g \neg_Y \exists_f: P X \to P X$ has a fixed point. This objection can be countered by shopping around for a different fixed-point theorem, one which is predicatively and constructively valid.

A time-honored way of constructing a fixed point of an operator $\phi$ is by taking a limit of a sequence of iterates of $\phi$ that converges, provided that $\phi$ preserves the limit. To this end, we find that specializing Ad\'a{}mek's theorem (see [[initial algebra of an endofunctor]]) suits our purposes perfectly.

\begin{lemma}
\label{chain}\hypertarget{chain}{}
If $g: Y \to X$ is monic, then the operator $\exists_g: P Y \to P X$ preserves limits of inverse chains $\omega^{op} \to P Y$ (i.e. intersections of decreasing sequences).

\end{lemma}
\begin{proof}
More generally, $\exists_g$ preserves [[connected limits]], because it lifts through the inclusion $i: P X \downarrow \exists_g(1) \hookrightarrow P X$ to an isomorphism $P Y \stackrel{\sim}{\to} P X \downarrow \exists_g(1)$ (here $1$ denotes the top element of $P Y$, aka $Y$), and $i$ preserves connected limits.

In more detail: by [[Frobenius reciprocity]], we have $\exists_g T \wedge S = \exists_g(T \wedge g^\ast S)$ for elements $S$ of $P X$ and $T$ of $P Y$. Putting $T = 1$, we get $\exists_g 1 \wedge S = \exists_g g^\ast S$, and so the composite

\begin{displaymath}
P X \downarrow \exists_g 1 \stackrel{g^\ast}{\to} P Y \stackrel{\exists_g}{\to} P X \downarrow \exists_g 1
\end{displaymath}
is the identity. But since $g$ is monic, $g^\ast \exists_g: P Y \to P Y$ is also the identity, which completes the proof.

\end{proof}
\begin{cor}
\label{}\hypertarget{}{}
$\forall_g = \neg_X \exists_g \neg_Y: P Y \to P X$ preserves colimits of $\omega$-chains.

\end{cor}
Naturally the left adjoint $\exists_f$ also preserves such colimits. So by the corollary, the composite $\neg_X \exists_g \neg_Y \exists_f: P X \to P X$ preserves colimits of $\omega$-chains.

Putting now $A_0 = 0$ (the bottom element of $P X$), $A_1 = \neg_X \exists_g \neg_Y \exists_f(0)$, and generally

\begin{equation}
A_n = (\neg_X \exists_g \neg_Y \exists_f)^n(0),
\label{An}\end{equation}
we have $A_n \subseteq A_{n+1}$ (apply the monotone operator $(\neg_X \exists_g \neg_Y \exists_f)^n$ to the inclusion $A_0 = 0 \subseteq A_1$), and so $\neg_X \exists_g \neg_Y \exists_f$ preserves the union of the chain $A_0 \subseteq A_1 \subseteq \ldots$,

\begin{equation}
A = \bigcup_{n \geq 0} (\neg_X \exists_g \neg_Y \exists_f)^n(0),
\label{A}\end{equation}
which implies that $A$ is a fixed point of $\neg_X \exists_g \neg_Y \exists_f$, as desired. In fact this $A$ is the minimal fixed point, just as in the conclusion of the Knaster-Tarski lemma. (Cf. [[initial algebra of an endofunctor]], especially Ad\'a{}mek's theorem.)

\hypertarget{beta_reduced_proof}{}\subsubsection*{{Beta reduced proof}}\label{beta_reduced_proof}

The preceding proofs are sometimes considered too abstract to easily visualize, but this is slightly misleading: the second proof, involving the construction of a minimal fixed point as a countable limit, can be ``[[beta-reduced]]'' to produce one of the standard ``concrete'' proofs.

In a nutshell, the minimal fixed point of the operator $\neg \exists_g \neg \exists_f: P X \to P X$ can be expressed as an alternating series of iterated direct images:

\begin{equation}
X - g Y + g f X - g f g Y + \ldots
\label{series}\end{equation}
where $-$ stands for set-theoretic difference $\setminus$ and $+$ stands for the union $\cup$. The meaning of the infinite series is that we have a increasing sequence of those finite alternating sums with an even number of terms, starting with the empty sum (which is $0$, the empty set):

\begin{displaymath}
0
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
X - g Y,
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
X - g Y + g f X - g f g Y,
\end{displaymath}
etc., and the infinite series is interpreted as the countable union of this increasing sequence. Note that we have to be careful about the order of the appearance of $+$ and $-$, but alternatively, letting $\oplus$ be the addition in the Boolean \emph{ring} $P X$ (symmetric difference), we could write also the series as $X \oplus g Y \oplus g f X \oplus \ldots$ in the ring, where we do not need to be fussy about order.

Most of this is a routine calculation, which for the most part boils down to the following observation:

\begin{lemma}
\label{}\hypertarget{}{}
If $B, D$ are elements of $P Y$, with $D \leq B$, then $\exists_g(B - D) = \exists_g B - \exists_g D$. (With a similar statement for $\exists_f$.)

\end{lemma}
The proof is left to the reader, but in brief, the injectivity of $g$ implies that $\exists_g$ preserves binary intersections and relative complements.

From here, if we write

\begin{displaymath}
\neg \exists_g \neg \exists_f(B) = X - g(Y - f B) = X - g Y + g f B = X \oplus g Y \oplus g f B,
\end{displaymath}
then it is easily verified by induction that, referring to equation \eqref{An},

\begin{displaymath}
A_n = (\neg \exists_g \neg \exists_f)^n 0 = \bigoplus_{j=0}^n (g f)^j X \oplus \bigoplus_{j=0}^n g(f g)^j Y.
\end{displaymath}
Thus, according to equation \eqref{A}, the minimal fixed point $A$ is the union of the $A_n$ which is how we are interpreting the series \eqref{series}.

Now we set up a comparison with one of the standard proofs involving a [[back-and-forth argument]], say the one given in \href{https://en.wikipedia.org/wiki/Schr%C3%B6der%E2%80%93Bernstein_theorem#Proof}{Wikipedia} that is attributed to Julius K\"o{}nig. The minimal fixed point is a union of finitary approximations

\begin{displaymath}
A_1 = X - g Y,
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
A_2 = X - g Y + g f X - g f g Y,
\end{displaymath}
etc. Elements in $A_1$ are those which have no inverse images under $g$. Elements in $A_2$ are elements in $X$ to which $(g f)^{-1}$ can be applied at most once before we hit an element of $X$ with no inverse image under $g^{-1}$. Elements in the union $A_1 \cup A_2 \cup \ldots$ are those which survive at most finitely many applications of $(g f)^{-1}$ before hitting an element of $X$ with no inverse image under $g$. In the terminology of the Wikipedia article, such elements $x$ in $X$ are called ``$X$-stoppers'', and these are exactly the elements for which $h(x)$ (where recall $h$ is the bijection under construction) is defined to be $f(x)$ in the Wikipedia article. For elements $x$ not in this fixed point $A$ (the non-$X$-stoppers), our proof of CSB (via a minimal fixed point) defined $h(x)$ to be $g^{-1}(x)$, the same prescription that is used in the Wikipedia article.

Other prescriptions are possible. For example, one could dually construct a \emph{maximal} fixed point of the operator $\neg \exists_g \neg \exists_f: P X \to P X$, using Lemma \ref{chain} to note that $\exists_f$ and the right adjoint $\forall_g = \neg \exists_g \neg$ preserve limits of inverse $\omega$-chains, so that the maximal fixed point or terminal algebra of the endofunctor $\neg \exists_g \neg \exists_f$ could be constructed as an intersection $\bigcap_{n \geq 1} (\neg \exists_g \neg \exists_f)^n(1)$. This could also be written as a series

\begin{displaymath}
X - g Y + g f X - g f g Y + g f g f X - \ldots
\end{displaymath}
except this time the series is interpreted as an \emph{intersection} of a \emph{decreasing} sequence whose partial sums have an \emph{odd} number of terms:

\begin{displaymath}
1 = X,
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
\neg \exists_g \neg \exists_f(1) = X - g Y + g f X,
\end{displaymath}
\begin{displaymath}
\,
\end{displaymath}
\begin{displaymath}
(\neg \exists_g \neg \exists_f)^2(1) = X - g Y + g f X - g f g Y + g f g f X,
\end{displaymath}
etc. The difference between this and the minimal fixed point is the set $\bigcap_{n \geq 1} (g f)^n(X)$, consisting of elements $x$ of $X$ that belong to a doubly infinite sequence or a cyclic sequence (in the terminology of the Wikipedia article). As remarked in that article, for such $x$ we have an option to define $h(x)$ as $f(x)$ or $g^{-1}(x)$; in the present article we defined $h(x) = f(x)$ for all $x$ belonging to whichever fixed point $A$ is used, which includes points in doubly infinite sequences or cyclic sequences if $A$ is the maximal fixed point. In that case the remaining $x$ (belonging to the complement of the maximal fixed point) are mapped to $g^{-1}(x)$.

\hypertarget{failure_in_toposes_and_constructive_mathematics}{}\subsection*{{Failure in toposes and constructive mathematics}}\label{failure_in_toposes_and_constructive_mathematics}

\begin{example}
\label{Top}\hypertarget{Top}{}
Counterexample \ref{counterexample2} below shows that the CSB theorem fails in Brouwer's [[intuitionistic mathematics]] even for $Set$ (since every function between the sets $[0, 1]$ and $\mathbb{R}$ must be continuous by Brouwer's continuity principle!). See also the discussion in \hyperlink{MM}{Mac Lane-Moerdijk}, VI.9, on toposes that realize Brouwer's theorem.

\end{example}
\begin{example}
\label{counterexample}\hypertarget{counterexample}{}
As mentioned above, the Cantor-Schroeder-Bernstein theorem fails in the arrow category $Set^\to$, whose objects are functions $X_0 \to X_1$ between sets and whose morphisms are commutative squares. For example, let $X$ be the object $f: \mathbb{N} \to \mathbb{N}$ that takes $n \in \mathbb{N}$ to $\mathrm{int}(n/2)$, where $\mathrm{int}(x)$ is the greatest integer less than or equal to $x$; let $Y$ be the object $g: \mathbb{N} \to \mathbb{N}$ that takes $n$ to $\mathrm{Int}((n+1)/2)$, where $\mathrm{Int}(x)$ is the least integer greater than or equal to $x$. Pretty clearly $X$ and $Y$ are non-isomorphic, because $g^{-1}(0)$ has cardinality $1$ whereas all fibers of $f$ have cardinality $2$. But, just by drawing pictures of these objects, it is easy to construct monomophisms $i: X \to Y$ and $j: Y \to X$ (e.g., define $i_0(n) = n+1$ and $i_1(n) = n+1$ for all $n$, and define $j_0(n) = n+1$ for $n \gt 0$, $j_0(0) = 0$, and $j_1(n) = n$ for all $n$).

\end{example}
Nor can one have internal existence of an isomorphism between $X$ and $Y$ in this last example, since internal existence implies external existence as soon as the terminal object is (externally) projective.

In fact, the CSB theorem is equivalent in [[constructive mathematics]] (with the [[axiom of infinity]]) to the [[law of excluded middle]]. This was shown in \hyperlink{PB19}{Pradic and Brown, 2019} using the [[principle of omniscience]] for the [[extended natural numbers]].

\hypertarget{in_other_categories}{}\subsection*{{In other categories}}\label{in_other_categories}

The CSB property holds in some other [[categories]] of interest (but arguably fails in many more). Some examples follow:

\begin{example}
\label{model}\hypertarget{model}{}
The CSB property holds in the category of [[vector spaces]] and in the category of [[algebraically closed field]]s. See also this \href{http://mathoverflow.net/questions/1058/when-does-cantor-bernstein-hold}{MO post} by John Goodrick, where model-theoretic criteria come into play, sometimes under strengthenings of the notion of monomorphism (e.g., [[elementary embedding]], [[split monomorphism]]) Some slides by Goodrick \href{http://settheory.mathtalks.org/wp-content/uploads/2012/06/jonh_goodrick.pdf}{here} go into more detail, giving connections between CSB and [[stability theory|stable theories]] in the sense of [[Shelah]].

\end{example}
\begin{example}
\label{counterexample2}\hypertarget{counterexample2}{}
On the other hand, the CSB property obviously fails in [[Top]], since we have [[embeddings]] $\mathbb{R} \cong (0,1) \to [0,1] \to \mathbb{R}$, yet $[0,1] \ncong \mathbb{R}$. It fails in [[Grp]] (e.g., the free group on countably many generators embeds in the free group on two generators).

\end{example}
More examples and discussion can be found at this Secret Blogging Seminar \href{http://sbseminar.wordpress.com/2007/10/30/theme-and-variations-schroeder-bernstein/}{post}.

In a \hyperlink{Gowers}{celebrated work}, [[Timothy Gowers]] gave a negative solution in the case of [[Banach spaces]].

\hypertarget{name}{}\subsection*{{Name}}\label{name}

The CSB theorem was first stated by [[Georg Cantor]], but his proof relied on the [[well-ordering theorem]]. The modern (choice-free) theorem was proved (independently) by [[Felix Bernstein]] and [[Ernst Schröder]]. It has been variously named after two or three of these in almost every possible combination, although Cantor (when mentioned at all) seems always to be mentioned first.

\href{http://en.wikipedia.org/wiki/Cantor%E2%80%93Bernstein%E2%80%93Schroeder_theorem#History}{Wikipedia} reports that [[Richard Dedekind]] had an (unpublished) proof in 1887, well before any announced proofs by Cantor, Schroeder, or Bernstein in 1895, 1896, 1897 respectively.

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

\begin{itemize}%
\item [[Peter Johnstone]], \emph{[[Sketches of an Elephant]]: A Topos Theory Conpendium}, Vol. I, Clarendon Press, Oxford (2002)


\item [[Timothy Gowers]], \emph{A Solution to the Schroeder-Bernstein Problem for Banach Spaces}, Bulletin of the London Mathematical Society, Volume 28, Issue 3 (1996), 297-304 \href{http://blms.oxfordjournals.org/content/28/3/297.abstract}{(abstract)}



\end{itemize}
\begin{itemize}%
\item [[Saunders Mac Lane]] and [[Ieke Moerdijk]], \emph{Sheaves in Geometry and Logic}, Springer-Verlag 1992.

\end{itemize}
\begin{itemize}%
\item Pierre Pradic, Chad E. Brown, \emph{Cantor-Bernstein implies Excluded Middle}, \href{https://arxiv.org/abs/1904.09193}{arxiv}, 2019

\end{itemize}
[[!redirects Cantor-Schroeder-Bernstein theorem]] [[!redirects Cantor–Schroeder–Bernstein theorem]] [[!redirects Cantor--Schroeder--Bernstein theorem]] [[!redirects Cantor-Schroeder-Bernstein Theorem]] [[!redirects Cantor–Schroeder–Bernstein Theorem]] [[!redirects Cantor--Schroeder--Bernstein Theorem]] [[!redirects Cantor-Schröder-Bernstein theorem]] [[!redirects Cantor–Schröder–Bernstein theorem]] [[!redirects Cantor--Schröder--Bernstein theorem]] [[!redirects Cantor-Schröder-Bernstein Theorem]] [[!redirects Cantor–Schröder–Bernstein Theorem]] [[!redirects Cantor--Schröder--Bernstein Theorem]] [[!redirects Schroeder-Bernstein theorem]] [[!redirects Schroeder–Bernstein theorem]] [[!redirects Schroeder--Bernstein theorem]] [[!redirects Schroeder-Bernstein Theorem]] [[!redirects Schroeder–Bernstein Theorem]] [[!redirects Schroeder--Bernstein Theorem]] [[!redirects Schröder-Bernstein theorem]] [[!redirects Schröder–Bernstein theorem]] [[!redirects Schröder--Bernstein theorem]] [[!redirects Schröder-Bernstein Theorem]] [[!redirects Schröder–Bernstein Theorem]] [[!redirects Schröder--Bernstein Theorem]]



\end{document}