\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*{Grothendieck universe}

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

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{universes}{}\paragraph*{{Universes}}\label{universes}

[[!include universe - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{consequences}{Consequences}\dotfill \pageref*{consequences} \linebreak
\noindent\hyperlink{terminology_smalllarge}{Terminology: Small/Large}\dotfill \pageref*{terminology_smalllarge} \linebreak
\noindent\hyperlink{axiom_of_universes}{Axiom of Universes}\dotfill \pageref*{axiom_of_universes} \linebreak
\noindent\hyperlink{large_cardinals}{Large cardinals}\dotfill \pageref*{large_cardinals} \linebreak
\noindent\hyperlink{structural_version}{Structural Version}\dotfill \pageref*{structural_version} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{applications}{Applications}\dotfill \pageref*{applications} \linebreak
\noindent\hyperlink{presheaf_categories}{Presheaf Categories}\dotfill \pageref*{presheaf_categories} \linebreak
\noindent\hyperlink{alternative_approaches}{Alternative Approaches}\dotfill \pageref*{alternative_approaches} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

Problems of set theory arise by the unjustified recursion of the naive notion of a `collection of things.' If `Col' is one notion of collections (such as `Set' or `Class'), then the notion `Col of all Cols' is in general problematic, as it is subject to the construction of Russell-style paradoxes (although it is not the only source of such paradoxes).

One way out is to consider a hierarchy of notions of collections: Postulate that the collection of all `Col's is not a `Col' itself but instead is another notion of collection, `Col+'. We may thus speak of the `Col+ of all Cols.' Similarly, the collection of all `Col+'-type collections may be taken to be `Col++,' and so on.

One formalization of this idea is that of a \emph{Grothendieck universe}. This is defined to be a set $U$ that behaves like a `set+ of all sets' in that all the standard operations of set theory (union, power set, etc.) can be performed on its elements.

Although developed for application to [[category theory]], the definition is usually given in a form that only makes sense in a membership-based [[set theory]]. On this page, we consider only that version; for a form that makes sense in structural set theory, please see [[universe in a topos]].

I don't really like how this page looks now, since it focuses once more on the `evil' set theory. I think that I'll rewrite it to talk about strongly inaccessible cardinal numbers first, which is a reasonable approach from any perspective, and then look at how you can say this more directly in both material and structural set theory. That means that I'll restore some text that was removed (not much of that was moved to [[universe in a topos]]), but this time I'll verify the correctness of the structural material (using [[universe in a topos]] as a guide) as I go. --- Toby

[[Mike Shulman|Mike]]: I'm not sure I agree. Firstly, I actually think it is better to define what you really want --- in this case, a collection of sets closed under the operations we need --- and only later observe that it may be equivalent to something in terms of inaccessible cardinals. I also expect that the equivalence between universes and inaccessibles requires the [[axiom of choice]], so wouldn't it be better to separate them? Finally, this page is called `Grothendieck universe,' not [[inaccessible cardinal]], so I think that here we should take the universes as primary, not their cardinals.

\emph{Toby}: I disagree that this is is `what we really want'; the definition below is only what we want if we're using material set theory, which for the most part we aren't in the nLab. So it's really out of place to focus on that.

But I'm not sure that you understand my intention, either. In explaining the point of universe to Urs, or more generally in explaining the point in a structural way, I find the cardinal number the easiest way to get at what matters. It is, as I said before, the bottom line for any proposed (re)definition. So I intend to define Grothendieck universes, certainly, although I intend to define them in terms of cardinal numbers. (Or rather, in terms of isomorphism classes of sets, but using cardinal arithmetic, so I'll call those cardinal numbers.) The discussion of inaccessible cardinals would be only lemmatic (if that's a word); if I get around to doing it, then you'll see what I mean.

But here's another possibility: Maybe we should reserve this page for the strict notion in material set theory and make another page, say [[universe]], for the non-evil concept. Then most (if not all) links here would really want to go there. I'm not sure that I like this, since `universe' has other meanings, but maybe there's another term that we could use that doesn't conflict with this term? In any case, if you want something like that, then I can go along with it. What I really don't want is a bunch of links on the lab implying that category theorists deal with size issues using something that's fundamentally part of material set theory.

[[Mike Shulman|Mike]]: I can definitely get behind that last sentence. `Grothendieck universe' seems to be used pretty much everywhere with the material version in mind, but this is probably just because people don't understand or trust structural set theory, and of course the structural version would be just as good for the \emph{purposes} people use them for. So I think it would be okay if we include both the material and structural versions on this page. (I definitely don't think we should include \emph{only} the structural version.)

Of course the definition below is only correct in material set theory, but there is also a straightforward structural version that you wrote down, in terms of families, that makes no reference to cardinality. What I don't see is \emph{why} the cardinal number is ``what matters'' or ``the bottom line for any proposed (re)definition.'' It seems to me that what's important for category theory is that we have a collection of sets, called `small,' which are closed under various constructions (power sets, indexed unions, etc.), so that the resulting category $Set$ of small sets behaves the way we want it to. It's completely irrelevant whether ``small'' is defined to mean `of cardinality less than $\kappa$' for some $\kappa$, or defined in some other way. If you assume the axiom of choice, then any collection of small sets closed under enough constructions \emph{will} consist precisely of the sets of cardinality $\lt \kappa$ for some $\kappa$, but in the absence of choice, I see no reason for that to be true. All of this is equally true materially and structurally.

(As an aside, I'm not so sure that on the nLab we `aren't' using material set theory; rather, I think that practically everything we do is completely agnostic as to whether the foundation is material or structural. In fact, if you assume the axioms of choice and foundation, then the two are completely equivalent --- a model of ZFC can be reconstructed, up to isomorphism, from its category of sets, and that category of sets is determined, up to equivalence, by its well-founded-set-objects.)

[[Mike Shulman|Mike]]: In fact, you yourself wrote at [[foundations]]:

\begin{quote}%
I understand all these large cardinals much better in terms of their categories of small sets.


\end{quote}
\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

A \textbf{Grothendieck universe} is a [[pure set]] $U$ such that:

\begin{enumerate}%
\item for all $u \in U$ and $t\in u$, we have $t \in U$ (i.e., $U$ is \emph{transitive});
\item for all $u \in U$, we have $\mathcal{P}(u) \in U$;
\item $\varnothing \in U$;
\item for all $I \in U$ and functions $u: I \to U$, we have $\displaystyle \bigcup_{i \in I} u_{i} \in U$.

\end{enumerate}
Some authors leave out (3), which allows the empty set $\varnothing$ itself to be a Grothendieck universe. Other authors use the set $\mathbb{N}$ of [[natural numbers]] in place of $\empty$ in (3), which prevents the countable set $V_{\omega}$ of [[hereditarily finite sets]] from being a Grothendieck universe.

\hypertarget{consequences}{}\subsection*{{Consequences}}\label{consequences}

From the definition above, one can prove additional closure properties of a universe $U$, including the usual codings in pure set theory of [[function sets]] and [[cartesian products]] and [[disjoint unions]] of sets, using the following lemmata:

\begin{lemma}
\label{}\hypertarget{}{}
If $t$ is a [[subset]] of $u$ and $u \in U$, then $t \in U$.

\end{lemma}
\begin{proof}
By (2), $\mathcal{P}(u) \in U$. Then as $t \in \mathcal{P}(u)$, we have $t \in U$ by (1).

\end{proof}
\begin{lemma}
\label{}\hypertarget{}{}
If $u, v \in U$, then $u \cup v \in U$.

\end{lemma}
\begin{proof}
As $\empty \in U$ by (3), so are $\star \stackrel{\text{df}}{=} \mathcal{P}(\empty)$ and $TV \stackrel{\text{df}}{=} \mathcal{P}(\star)$ by (2). Even in [[constructive mathematics]], $2 = \{ \bot,\top \}$ is a subset of $TV$, so $2 \in U$ by Lemma 1. Then $(\bot \mapsto u,\top \mapsto v)$ is a function from $2 \to U$, so the union $u \cup v$ in $U$ by (4).

\end{proof}
Then using their usual encodings in set theory:

\begin{itemize}%
\item the nullary cartesian product $\star$ is $\mathcal{P}(\varnothing)$ as in the previous proof;
\item the binary cartesian product $u \times v$ is a subset of $\mathcal{P}(\mathcal{P}(u \cup v))$;
\item the general cartesian product $\displaystyle \prod_{i \in I} u_{i}$ is a subset of $\displaystyle \mathcal{P} \left( I \times \bigcup_{i \in I} u_{i} \right)$;
\item the nullary disjoint union is $\varnothing$;
\item the binary disjoint union $u \uplus v$ is a subset of $2 \times (u \cup v)$;
\item the general disjoint union $\displaystyle \biguplus_{i \in I} u_{i}$ is a subset of $\displaystyle I \times \bigcup_{i \in I} u_{i}$;
\item the set of functions $u \to v$ is a subset of $\mathcal{P}(u \times v)$.

\end{itemize}
\hypertarget{terminology_smalllarge}{}\subsection*{{Terminology: Small/Large}}\label{terminology_smalllarge}

Given a universe $U$, an element of $U$ is called a \textbf{$U$-small set}, while a subset of $U$ is called \textbf{$U$-moderate}. Every $U$-small set is $U$-moderate by requirement (1) of the definition. If the universe $U$ is understood, we may simply say \textbf{small} and \textbf{moderate}.

The term \emph{$U$-large} is ambiguous; it sometimes means `not small' but sometimes means the same as `moderate' (or `moderate but not small'). The reason is that language that distinguishes `small' from `large' in terms of sets and [[proper class|proper classes]] translates fairly directly into terms of $U$-small and $U$-moderate sets. To be precise, if we redefine `set' to mean `$U$-small set,' then every proper class in this new world of sets will be represented by a $U$-moderate set (a subset of $U$). Those sets that are not even $U$-moderate are `too large' to be translated into language of proper classes.

(Note, though, that not all $U$-moderate sets represent proper classes in the language of set theory relative to the world of $U$-small sets, only those that are \emph{first-order definable} from $U$-small sets. In fact, if $\kappa$ is the [[cardinal number|cardinality]] of the universe $U$, then there are only $\kappa$ proper classes relative to $U$, but there are $2^{\kappa}$-many $U$-moderate sets.)

As defined above, these concepts violate the [[principle of equivalence]], as two sets may be [[isomorphism|isomorphic]] yet have different properties with respect to $U$. However, a set which is isomorphic to a $U$-small or $U$-moderate set is called \textbf{essentially} $U$-small or $U$-moderate; these respect the [[principle of equivalence]].

\hypertarget{axiom_of_universes}{}\subsection*{{Axiom of Universes}}\label{axiom_of_universes}

If $U$ is a Grothendieck universe, then it is easy to show that $U$ is itself a model of [[ZFC]] (minus the axiom of infinity unless you modify (3) to rule out countable universes). Therefore, one cannot prove in ZFC the existence of a Grothendieck universe containing $\mathbb{N}$, and so we need extra set-theoretic axioms to ensure that uncountable universes exist. Grothendieck's original proposal was to add the following \textbf{axiom of universes} to the usual axioms of set theory:

\begin{itemize}%
\item For every set $s$, there exists a universe $U$ that contains $s$, i.e., $s \in U$.

\end{itemize}
In this way, whenever any operation leads one outside of a given Grothendieck universe (see applications below), there is guaranteed to be a bigger Grothendieck universe in which one lands. In other words, every set is small if your universe is large enough!

Later, Mac Lane pointed out that often, it suffices to assume the existence of \emph{one} uncountable universe. In particular, any discussion of `small' and `large' that can be stated in terms of sets and proper classes can also be stated in terms of a single universe $U$ (with `large' meaning `$U$-moderate but not $U$-small').

\hypertarget{large_cardinals}{}\subsection*{{Large cardinals}}\label{large_cardinals}

If $U$ is a Grothendieck universe, then one can prove in ZFC that it must be of the form $V_{\kappa}$, where $\kappa$ is a (strongly) [[inaccessible cardinal]] (\hyperlink{Williams}{Williams}). Here, $V_{\kappa}$ is the $\kappa$-th set in the [[von Neumann hierarchy]] of pure sets. Conversely, every such $V_{\kappa}$ is a Grothendieck universe. Thus, the existence of Grothendieck universes is equivalent to the existence of inaccessible cardinals, and so the axiom of universes is equivalent to the `large cardinal axiom' that `there exist arbitrarily large inaccessible cardinals.'

It is worth noting, for those with foundational worries, that the axiom of universes is much, much weaker than many large cardinal axioms which are routinely used, and believed to be consistent, by modern set theorists. Of course, one cannot \emph{prove} the consistency of any large cardinal axiom (if it really is consistent) except by invoking a stronger one.

\hypertarget{structural_version}{}\subsection*{{Structural Version}}\label{structural_version}

An equivalent concept (at least for the purposes of category theory) can also be defined in structural set theories (like [[ETCS]]). Please see [[universe in a topos]].

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

The set $V_{\omega}$ of [[hereditarily finite sets]] (finite sets of finite sets of\ldots{}) is a Grothendieck universe, unless you phrase axiom (3) in the definition to specifically rule it out. In this way, the axiom of infinity can be seen as a simple universe axiom (stating that at least one universe exists), and Mac Lane's axiom that an uncountable universe exists is merely one step further.

If you refrain from using the axiom of universes (except perhaps once, to get $\mathbb{N}$ as above), then the set of all sets (or cardinal numbers) that you can actually construct is a Grothendieck universe. Of course, you cannot possibly have proved that this universe exists, but the intuition that you ought be able to form the collection of `everything that we've used so far' is the justification for the axiom of universes.

Similarly, if you use the axiom of universes at most $n$ times, then the set of all sets that you can construct with this restriction is a Grothendieck universe. Thus, we can find a sequence $U_{1} \in U_{2} \in U_{3} \in \ldots$ of universes. The [[axiom of replacement]] then allows us to form the union (a directed [[colimit]]) $\bigcup_{n \lt \omega} U_{n}$. This will not be a universe (it violates (4), by definition), but we can use the axiom of universes again to show that it is in some universe $U_{\omega}$. Proceeding in this way, we can construct a tower of universes indexed by the [[ordinal numbers]].

The set of all sets that can be constructed using the axioms of ZFC together with the axiom of universes is, if it exists, again a universe which contains all the $U_{\alpha}$ constructed above. Of course, it cannot be shown to exist using only ZFC and the axiom of universes; the axiom of universes is not the final word on large cardinal axioms by any means.

\hypertarget{applications}{}\subsection*{{Applications}}\label{applications}

Let $U Set$ be the [[category]] of $U$-small sets, a [[full subcategory]] of [[Set]]. It is common, especially when $U$ is understood, to redefine $Set$ to mean $U Set$; here we keep the distinction for clarity. However, when $Set$ means $U Set$, sometimes $SET$ is used to mean the category of \emph{all} sets.

A category whose set of morphisms is (essentially) $U$-small may be called a $U$-[[small category]]; it can also be thought of as an [[internal category]] in $U Set$. A category whose [[hom-sets]] are all (essentially) $U$-small may be called [[locally small category|locally]] $U$-small; it can also be thought of as an [[enriched category]] over $U Set$. Every $U$-small category is locally $U$-small.

A category whose set of morphisms is $U$-moderate may be called a $U$-[[large category|moderate category]]; again `$U$-large' may mean `not $U$-small,' `$U$-moderate,' or both. In practice, most $U$-moderate categories are locally $U$-small and vice versa, but there is no theorem that this must be true. Note that $U Set$ itself is $U$-moderate and locally $U$-small but not $U$-small.

All notions of category theory that reference size, such as [[complete category|completeness]] and [[locally presentable category|local presentability]], must then be relativized to $U$. In order to move from a category defined in one universe to another, we need a procedure of [[universe enlargement]].

\hypertarget{presheaf_categories}{}\subsubsection*{{Presheaf Categories}}\label{presheaf_categories}

Let $C$ be a $U$-small category. Then the category of $U$-[[presheaf|presheaves]] on $C$ (the [[functor category]] $[C^{op},U Set]$) is also $U$-moderate and locally $U$-small but not $U$-small unless $C$ is empty. ($U Set$ itself is the special case of this where $C$ is the [[point]].) These arguments go as follows:

\begin{itemize}%
\item $U PSh(C)$ is $U$-moderate: An upper bound for the size of $[C^{op},U Set]$, hence of the set $Obj([C^{op},U Set])$ is the size of $\{ F: Obj(C) \times Mor(C) \to U \}$, where both $Obj(C)$ and $Mor(C)$ are in $U Set$. Hence, we are looking at the cardinal number $|U|^{|u| \times |v|}$, where $u = Obj(C)$ and $v = Mor(C)$. Use the fact that any Grothendieck universe must be infinite (since it has $\varnothing$, $\mathcal{P}(\varnothing)$, etc.), and the result follows from cardinal arithmetic that $\kappa^{\lambda} = \kappa$ if $\lambda \lt \kappa$ and $\kappa$ is infinite.


\item $U PSh(C)$ is locally $U$-small: An upper bound for the size of the set of morphisms between two functors $F,G: C^{op} \to U Set$ is the disjoint union indexed by the objects $c$ of $C$ over the $U$-sets $G(c)^{F(c)}$. Now $G(c)^{F(c)} \in U$ as it is a function set and $\displaystyle \bigcup_{c \in Obj(C)} G(c)^{F(c)}$ by the assumption that unions stay in $U$.



\end{itemize}
Now let $C$ be a $U$-moderate category (and not small). Then the category of $U$-presheaves on $C$ is not even locally $U$-small, nor is it even $U$-moderate (it is `too large'). However, it is locally $U$-moderate. Also, it is quite possible, if $C$ is a $U$-[[large site|moderate site]], that the category of $U$-[[sheaf|sheaves]] on $C$ is $U$-moderate and locally $U$-small.

\emph{Note:} Here we are considering presheaves on $C$ with values in $U$-small sets. In many cases, a more appropriate notion of `$U$-small presheaf' is that discussed at [[small presheaf]], namely a presheaf that is a $U$-small colimit of representables.

\hypertarget{alternative_approaches}{}\subsection*{{Alternative Approaches}}\label{alternative_approaches}

\begin{itemize}%
\item A different, potentially much more elegant and natural proposal for solving the problem to be solved by Grothendieck universes is that described at [[michaelshulman:category of all sets|category of all sets]]. Don't get your hopes up too high, though; even if it works, it isn't quite the category theory you're used to.

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

\begin{itemize}%
\item [[Nicolas Bourbaki]], \emph{Univers}, Appendix to Expose I in [[SGA 4]].


\item [[Mike Shulman]], \emph{Set theory for category theory}, \href{http://arxiv.org/abs/0810.1279}{arXiv:0810.1279}.


\item Zhen Lin Low, \emph{Universes for category theory}, \href{http://arxiv.org/abs/1304.5227}{arxiv/1304.5227}


\item [[Daniel Murfet]], \emph{Foundations for category theory}, \href{http://therisingsea.org/notes/FoundationsForCategoryTheory.pdf}{pdf}



\end{itemize}
The proof that a Grothendieck universe is equivalently a set of $\kappa$-small sets for $\kappa$ an [[inaccessible cardinal]] is in

\begin{itemize}%
\item N. H. Williams, \emph{On Grothendieck universes}, Compositio Mathematica, tome 21 no 1 (1969) (\href{http://www.numdam.org/item?id=CM_1969__21_1_1_0}{numdam})

\end{itemize}
SGA uses universes and much of modern results in algebraic geometry use general results from SGA, including Wiles proof of Fermat's theorem. Colin McLarty discusses how to remove the need for universes in Wiles' proof in

\begin{itemize}%
\item Colin McLarty, \emph{What does it take to prove Fermat's last theorem? Grothendieck and the logic of number theory}, \href{http://www.cwru.edu/artsci/phil/Proving_FLT.pdf}{pdf}

\end{itemize}
category: foundational axiom

[[!redirects Grothendieck universe]] [[!redirects Grothendieck universes]]

[[!redirects axiom of Grothendieck universes]] [[!redirects axiom of universes]]



\end{document}