We assume knowledge of basic categorical concepts such as categories, functors,
and natural transformations. The purpose of this lecture is to develop the
notion of a category over another category.
We will draw on the following materials:
We introduce and develop the notion of displayed categories. A displayed category over a category C
is equivalent to “a category D
and functor F : D \to C
, but instead of having a single collection of “objects of D
” with a map to the objects of C
, the objects are given as a family indexed by objects of C
, and similarly for the morphisms. This encapsulates a common way of building categories in practice, by starting with an existing category and adding extra data/properties to the objects and morphisms. The interest of this seemingly trivial reformulation is that various properties of functors are more naturally defined as properties of the corresponding displayed categories. Grothendieck fibrations, for example, when defined as certain functors, use equality on objects in their definition. When defined instead as certain displayed categories, no reference to equality on objects is required. Moreover, almost all examples of fibrations in nature are, in fact, categories whose standard construction can be seen as going via displayed categories. We therefore propose displayed categories as a basis for the development of fibrations in the type-theoretic setting, and similarly for various other notions whose classical definitions involve equality on objects. Besides giving a conceptual clarification of such issues, displayed categories also provide a powerful tool in computer formalisation, unifying and abstracting common constructions and proof techniques of category theory, and enabling modular reasoning about categories of multi-component structures. As such, most of the material of this article has been formalised in Coq over the UniMath library, with the aim of providing a practical library for use in further developments.
Jean Bénabou.
Fibered categories and the foundations of naïve category theory.
[benabou-1985]
En hommage à Alexandre Grothendieck.
Francis Borceux.
Handbook of Categorical Algebra 2: Categories and Structures.
[borceux-hca-2]
A Handbook of Categorical Algebra is designed to give, in three volumes, a detailed account of what should be known by everybody working in, or using, category theory. As such it will be a unique reference. The volumes are written in sequence, with the first being essentially self-contained, and are accessible to graduate students with a good background in mathematics. Volume 1, which is devoted to general concepts, can be used for advanced undergraduate courses on category theory. After introducing the terminology and proving the fundamental results concerning limits, adjoint functors and Kan extensions, the categories of fractions are studied in detail; special consideration is paid to the case of localizations. The remainder of the first volume studies various ‘refinements’ of the fundamental concepts of category and functor.
Bart Jacobs.
Categorical logic and type theory.
Studies in Logic and the Foundations of Mathematics.
Jan 14, 1999.
[jacobs-1999]
This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.
These are notes about the theory of Fibred Categories as I have learned it from Jean Benabou. I also have used results from the Thesis of Jean-Luc Moens from 1982 in those sections where I discuss the fibered view of geometric morphisms. Thus, almost all of the contents is not due to me but most of it cannot be found in the literature since Benabou has given many talks on it but most of his work on fibered categories is unpublished. But I am solely responsible for the mistakes and for misrepresentations of his views. And certainly these notes do not cover all the work he has done on fibered categories. I just try to explain the most important notions he has come up with in a way trying to be as close as possible to his intentions and intuitions. I started these notes in 1999 when I gave a course on some of the material at a workshop in Munich. They have developed quite a lot over the years and I have tried to include most of the things I want to remember.
These lecture notes are deeply influenced by Thomas Streicher.
A meta-category \mathfrak{C}
is defined by explaining what
an object of \mathfrak{E}
is, and, given two objects x,y\in \mathfrak{E}
,
what a morphism from x
to y
is, together with the following operations:
- for each object x\in \mathfrak{E}
, an identity map \Idn{x} : x \to x
,
- for any two maps f:x\to y
and g:y\to z
, a composite map f;g : x \to z
,
- such that the following equations hold:
\Idn{x};h = h\qquad
h;\Idn{y} = h\qquad
f;(g;h) = (f;g);{h}
In the definition of meta-category, we have not imposed any restrictions on what kinds of things the objects and morphisms are; our definition is pre-mathematical, so we do not assume beforehand that there is a such thing as a collection of “all” meta-categories.
We may define analogous notions of meta-functor, etc. But we do not
assume that the notion of “all meta-functors \mathfrak{C}\to\mathfrak{D}
” is well-defined; the notion is entirely schematic.
Assumption. We assume a meta-category \BoldSymbol{\mathfrak{Coll}}
whose objects we will refer to as “collections”. We assume that the meta-category of all collections satisfies the axioms of Lawvere’s ETCS.
A
category E
is defined to be a
meta-category whose objects
are defined to be the elements of some collection, and for any two objects
x,y\in E
the morphisms
x\to y
are defined to be the elements of some
collection.
Remark
(cartesian closure of the meta-category of all categories)
[frct-003K]
Consequently there exists a meta-category \BoldSymbol{\mathfrak{Cat}}
of all
categories. Following Lawvere (but deviating from some other authors that
ground the notion of meta-categories in classes) we notice that
\BoldSymbol{\mathfrak{Cat}}
is cartesian closed; in other words, all functor
categories exist regardless of size.
Assumption. At times we may assume that there exists a category
\SET\subseteq\BoldSymbol{\mathfrak{Coll}}
of collections that we will refer
to as sets, such that \SET
is closed under the axioms of ETCS. Rather than work with \SET
at all
times, our approach is to use the tools of relative category theory to
objectify the notions of “small” and “locally small” category over any category
B
, generalizing the role of \SET
from classical category theory.
Let B
be a category. A displayed category E
over B
is defined by the following data according to (Ahrens and Lumsdaine):
for each object x\in B
, a collection of displayed objects E\Sub{x}
,
for each morphism \Mor{f}{x}{y}\in B
and displayed objects \bar{x}\in E\Sub{x}
and \bar{y}\in E\Sub{y}
, a family of collections of displayed morphisms \Hom{E\Sub{f}}{\bar{x}}{\bar{y}}
, an element of which shall denote by \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
,
for each x\in B
and \bar{x}\in E\Sub{x}
, a displayed morphism \DispMor{\Idn{\bar{x}}}{\Idn{x}}{\bar{x}}{\bar{x}}
,
for each \Mor{f}{x}{y}
and \Mor{g}{y}{z}
in B
and objects \bar{x}\in E\Sub{x}, \bar{y}\in E\Sub{y}, \bar{z}\in E\Sub{z}
, a function
\Hom{E\Sub{f}}{\bar{x}}{\bar{y}} \times \Hom{E\Sub{g}}{\bar{y}}{\bar{z}} \to \Hom{E\Sub{f;g}}{\bar{x}}{\bar{z}}
that we will denote like ordinary (diagrammatic) function composition,such that the following equations hold:
\Idn{\bar{x}};\bar{h} = \bar{h}\qquad
\bar{h};\Idn{\bar{y}} = \bar{h}\qquad
\bar{f};(\bar{g};\bar{h}) = (\bar{f};\bar{g});\bar{h}
Note that these are well-defined because of the corresponding laws for the base category B
.
When we have too many subscripts, we will write E[x]
instead of E\Sub{x}
.
Let E
be displayed over B
, and let \Mor{f}{x}{y} \in B
; a morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in E
is called cartesian over f
when for any \Mor{m}{u}{x}
and \DispMor{\bar{h}}{m;f}{\bar{u}}{\bar{y}}
there exists a unique \DispMor{\bar{m}}{m}{\bar{u}}{\bar{x}}
with \bar{m};\bar{f} = \bar{h}
. We visualize this unique factorization of \bar{h}
through \bar{f}
over m
as follows:
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
west/style = lies over,
east/style = lies over,
north/node/style = upright desc,
height = 1.5cm,
nw = \bar{x},
ne = \bar{y},
sw = x,
north = \bar{f},
south = f,
se = y,
nw/style = pullback,
}
\node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
\node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
\draw[lies over] (u') to (u);
\draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
\draw[->] (u) to node [sloped,below] {$m$} (sw);
\draw[->,exists] (u') to node [desc] {$\bar{m}$} (nw);
\end{tikzpicture}](/forest/latex/frct-0001-cba8e5796900bbef92c0e497611454bd.svg)
Above we have used the “pullback corner” to indicate \bar{x}\to\bar{y}
as a
cartesian map. We return to this in our discussion of the self-indexing (the fundamental self-indexing)
of a category.
A displayed category E
over B
is said to be a cartesian fibration, when
for each morphism \Mor{f}{x}{y}
and displayed object \bar{y}\in E\Sub{y}
, there
exists a displayed object \bar{x}\in E\Sub{x}
and a cartesian morphism
\DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in the sense of cartesian morphisms. Note that the pair (\bar{x},\bar{f})
is unique up to
unique isomorphism, so being a cartesian fibration is a property of a displayed category.
There are other variations of fibration. For instance, E
is said to be an isofibration when the condition above holds just for isomorphisms f : x\cong y
in the base.
Construction
(the fundamental self-indexing)
[frct-001X]
Let B
be an ordinary category; there is an important displayed category \SelfIx{B}
over B
given fiberwise by the slices of B
.
- For x\in B
, we define \SelfIx{B}\Sub{x}
to be the collection \Sl{B}{x}
of pairs (\bar{x}\in B,\Mor{p\Sub{x}}{\bar{x}}{x})
.
- For \Mor{f}{x}{y}\in B
, we define \SelfIx{B}\Sub{f}
to be the collection of commuting squares in the following configuration:
In light of the fundamental self-indexing, the following result for displayed categories generalizes
the ordinary “pullback lemma.”
Let \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
, and suppose that \DispMor{\bar{g}}{g}{\bar{y}}{\bar{z}}
is cartesian over g
. Then
\bar{f};\bar{g}
is cartesian over f;g
if and only if \bar{f}
is cartesian
over f
.
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
height = 1.5cm,
west/style = lies over,
east/style = lies over,
nw/style = pullback,
sw = y,
nw = \bar{y},
se = z,
ne = \bar{z},
south = g,
north = \bar{g},
}
\node (x*) [dotted pullback, left = of nw] {$\bar{x}$};
\node (x) [left = of sw] {$x$};
\draw[->] (x*) to node [above] {$\bar{f}$} (nw);
\draw[lies over] (x*) to (x);
\draw[->] (x) to node [below] {$f$} (sw);
\end{tikzpicture}](/forest/latex/frct-001H-05046432d2823c4c5ddc7bc58375cf56.svg)
Proof.
Suppose first that \bar{f}
is cartesian. To see that \bar{f};\bar{g}
is cartesian, we must construct a unique factorization as follows:
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
west/style = lies over,
east/style = lies over,
north/node/style = upright desc,
height = 1.5cm,
nw = \bar{x},
ne = \bar{y},
sw = x,
north = \bar{f},
south = f,
se = y,
nw/style = pullback,
ne/style = pullback,
}
\node (z') [right = 2cm of ne] {$\bar{z}$};
\node (z) [right = 2cm of se] {$z$};
\draw[lies over] (z') to (z);
\draw[->] (se) to node [below] {$g$} (z);
\draw[->] (ne) to node [desc] {$\bar{g}$} (z');
\node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
\node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
\draw[lies over] (u') to (u);
\draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (z');
\draw[->] (u) to node [sloped,below] {$m$} (sw);
\draw[->,exists] (u') to (nw);
\end{tikzpicture}](/forest/latex/frct-001H-88a74b6f1359eed6bbdd21ffc4ab884b.svg)
Because \bar{g}
is cartesian, we can factor \bar{h} = i;\bar{g}
for a unique \DispMor{i}{m;f}{\bar{u}}{\bar{y}}
. Then, because \bar{f}
is cartesian, we can further factor i = j;\bar{f}
for a unique \DispMor{j}{m}{\bar{u}}{\bar{x}}
. We conclude that there is a unique \DispMor{j}{m}{\bar{u}}{\bar{x}}
for which \bar{h} = j;\bar{f};\bar{g}
, as required.
Conversely, suppose that \bar{f};\bar{g}
is cartesian. To see that \bar{f}
is cartesian, we must construct a unique factorization as follows:
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
west/style = lies over,
east/style = lies over,
north/node/style = upright desc,
height = 1.5cm,
nw = \bar{x},
ne = \bar{y},
sw = x,
north = \bar{f},
south = f,
se = y,
ne/style = pullback,
}
\node (z') [right = 2cm of ne] {$\bar{z}$};
\node (z) [right = 2cm of se] {$z$};
\draw[lies over] (z') to (z);
\draw[->] (se) to node [below] {$g$} (z);
\draw[->] (ne) to node [desc] {$\bar{g}$} (z');
\node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
\node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
\draw[lies over] (u') to (u);
\draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
\draw[->] (u) to node [sloped,below] {$m$} (sw);
\draw[->,exists] (u') to (nw);
\end{tikzpicture}](/forest/latex/frct-001H-b2e8d70a0f78b21957db84ee03e5d64a.svg)
Because \bar{f};\bar{g}
is cartesian, we can factor \bar{h};\bar{g} = i;\bar{f};\bar{g}
for a unique \DispMor{i}{m}{\bar{u}}{\bar{x}}
. On the other hand, because \bar{g}
is cartesian, there is a unique \DispMor{j}{m;f}{\bar{u}}{\bar{y}}
for which \bar{h};\bar{g} = j;\bar{g}
; as both \bar{h}
and i;\bar{f}
satisfy this condition, we conclude \bar{h}=i;\bar{f}
. Therefore, there is a unique \DispMor{i}{m}{\bar{u}}{\bar{x}}
for which
\bar{h} = i;\bar{f}
, as required.
Warning. Some authors including Grothendieck give an
equivalent definition of cartesian fibration that factors through a
nonequivalent definition of cartesian morphisms. Such authors refer to our
notion of cartesian morphism as hypercartesian (see Streicher).
Let E
be displayed over B
, and let f:x\to y \in B
; a morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in E
is called hypocartesian over f
when for any \bar{u}\in E\Sub{x}
and \DispMor{\bar{h}}{f}{\bar{u}}{\bar{y}}
there exists a
unique \DispMor{i}{\Idn{x}}{\bar{u}}{\bar{x}}
with i;\bar{f} = \bar{h}
as follows:
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
west/style = lies over,
east/style = lies over,
north/node/style = upright desc,
height = 1.5cm,
nw = \bar{x},
ne = \bar{y},
sw = x,
north = \bar{f},
south = f,
se = y,
}
\node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
\node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$x$};
\draw[lies over] (u') to (u);
\draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
\draw[double] (u) to (sw);
\draw[->,exists] (u') to node [desc] {$i$} (nw);
\end{tikzpicture}](/forest/latex/frct-002A-a0b3c939d89133d8009535f2819443c0.svg)
Cartesian morphisms are clearly hypocartesian (setting u=x
and m=\Idn{x}
),
but the converse does not hold. The problem is that in an arbitrary displayed
category, hypocartesian morphisms may not be closed under composition.
Lemma
(hypocartesian = cartesian in a cartesian fibration)
[frct-002C]
Let E
be a cartesian fibration in the sense of cartesian fibration, and let \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
be displayed over \Mor{f}{x}{y}
. The displayed morphism \bar{f}
is cartesian if and only if it is hypocartesian.
Proof.
Any cartesian map is clearly hypocartesian. To see that a hypocartesian map \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
in a cartesian fibration is cartesian, we consider the cartesian lift of \Mor{f}{x}{y}
under \bar{y}
:
As the cartesian lift \bar{x}\tick\to \bar{y}
is also hypocartesian, it follows that there is a unique vertical isomorphism identifying \bar{x}
with \bar{x}\tick
factoring \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
through \DispMor{\bar{f}\tick}{f}{\bar{x}\tick}{\bar{y}}
. Being cartesian over f
is clearly stable under isomorphism, hence we conclude that \bar{f}
is cartesian from the fact that \bar{f}\tick
is cartesian.
Grothendieck defines a fibration in terms of (what we refer
to as) hypocartesian morphisms rather than (what we refer to as) cartesian
morphisms, and therefore imposes the additional constraint that the
hypocartesian morphisms be closed under composition. In equivalence with Grothendieck's fibrations below, we
verify that these two definitions of cartesian fibration coincide.Lemma
(equivalence with Grothendieck's fibrations)
[frct-002B]
Let E
be displayed over B
. Then E
is a cartesian fibration if and only if the following two conditions hold:
- Hypocartesian lifts. For each f:x\to y\in B
and \bar{y}\in E\Sub{y}
there
exists a displayed object \bar{x}\in E\Sub{x}
and hypocartesian morphism
\bar{f}:\bar{x}\DispTo{f}\bar{y}
.
- Closure under composition. If \bar{f}:\bar{x}\DispTo{f}\bar{y}
and
\bar{g}:\bar{y}\DispTo{g}\bar{z}
are hypocartesian, then \bar{f};\bar{g}
is hypocartesian.
Proof.
Suppose first that E
is a cartesian fibration in our sense. Then
E
has hypocartesian lifts because it has cartesian lifts. For closure under composition, fix hypocartesian \bar{f},\bar{g}
; because hypocartesian and cartesian maps coincide in a cartesian fibration we know that \bar{f},\bar{g}
are also cartesian and hence by the generalized pullback lemma so is the composite \bar{f};\bar{g}
; therefore it follows that \bar{f};\bar{g}
is also hypocartesian.
Conversely, suppose that E
is a cartesian fibration in the sense of Grothendieck, and let \bar{f}:\bar{x}\DispTo{f}\bar{y}
be the hypocartesian lift of f:x\to y
at \bar{y}\in E\Sub{y}
; we shall see that \bar{f}
is also a cartesian lift of f
at \bar{y}
by constructing a unique factorization as follows:
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
west/style = lies over,
east/style = lies over,
north/node/style = upright desc,
height = 1.5cm,
nw = \bar{x},
ne = \bar{y},
sw = x,
north = \bar{f},
south = f,
se = y,
}
\node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
\node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
\draw[lies over] (u') to (u);
\draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
\draw[->] (u) to node [sloped,below] {$m$} (sw);
\draw[->,exists] (u') to (nw);
\end{tikzpicture}](/forest/latex/frct-002B-df65d0d94f88de391280feaedc1faf90.svg)
Let \bar{m}:\bar{u}\tick\DispTo{m}\bar{x}
be the hypocartesian lift of m
at \bar{x}
, where \bar{u}\tick\in E\Sub{u}
. By hypothesis, the composite \bar{m};\bar{f} : \bar{u}\tick\DispTo{m;f}\bar{y}
is hypocartesian, so \bar{h}
factors uniquely through \bar{m};\bar{f}
over \Idn{u}
:
![\begin{tikzpicture}[diagram]
\SpliceDiagramSquare{
west/style = lies over,
east/style = lies over,
north/node/style = upright desc,
height = 1.5cm,
nw = \bar{u}',
ne = \bar{y},
sw = u,
north = \bar{m};\bar{f},
south = m;f,
se = y,
}
\node (u') [above left = 1.5cm of nw,xshift=-.5cm] {$\bar{u}$};
\node (u) [above left = 1.5cm of sw,xshift=-.5cm] {$u$};
\draw[lies over] (u') to (u);
\draw[->,bend left=30] (u') to node [sloped,above] {$\bar{h}$} (ne);
\draw[double] (u) to (sw);
\draw[->,exists] (u') to node [desc] {$i$} (nw);
\end{tikzpicture}](/forest/latex/frct-002B-40bea5f931bd435e6a4c164b15aff57c.svg)
The composite i;\bar{m} : \bar{u}\DispTo{m}\bar{x}
is the required (cartesian) factorization of \bar{h}
through \bar{f}
over m
. To see that i;\bar{m}
is the unique such map, we observe that all morphisms \bar{u}\DispTo{m}\bar{x}
factor uniquely through \bar{m}
over \Idn{u}
as a consequence of \bar{m}
being hypocartesian.
Hypocartesian and
cartesian
morphisms can be thought
of as two distinct ways to generalize the concept of a pullback, depending on
what one considers the essential properties of pullbacks. Hypocartesian
morphisms more directly generalize the “little picture” universal property of
pullbacks as limiting cones, whereas cartesian morphisms generalize the “big
picture” dynamics of the pullback pasting lemma. As we have seen in
hypocartesian = cartesian in a cartesian fibration these two notions coincide in any cartesian fibration; the instance of
this result for the
fundamental self-indexing verifies that
pullbacks can be equivalently presented in terms of cartesian morphisms, as we
have pointed out in
#frct-001Y.
Let E
be displayed over B
and let F
be displayed over C
. If \Mor{U}{B}{C}
is an ordinary functor, than a displayed functor from E
to F
over U
is given by the following data:
for each displayed object \bar{x}\in E\Sub{x}
, a displayed object \bar{U}\bar{x}\in F\Sub{Ux}
,
for each displayed morphism \DispMor{\bar{f}}{f}{\bar{x}}{\bar{y}}
, a displayed morphism \DispMor{\bar{U}\bar{f}}{Uf}{\bar{U}\bar{x}}{\bar{U}\bar{y}}
,
such that the assignment \bar{U}f
preserves displayed identities and displayed composition.
From this notion, we can see that the variation of displayed categories over their base categories itself has a “displayed categorical” structure; up to size issues, we could speak of the displayed bicategory of displayed categories.
Note. The correct notion of morphism between cartesian fibrations is given by displayed functors that preserve cartesian maps. We will call these fibered functors.
Let E
be a category displayed over B
. A vertical map in E
is defined to be one that lies over the identity map in B
. For every