Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It only takes a minute to sign up.
Sign up to join this community
I stumbled upon the "fibration of points" in the definition of a protomodular category and apparently this is indeed an instance of a fibration.
What are fibrations intuition-wise and how are they important?
I would like to have an answer that can be comprehended by an undergraduate, who knows a bit of category theory (but almost no higher category theory or topology), if that is at all possible.
Context: This answer discusses the view of categorical logic on fibrations, not the one of topology.
Summary: In categorical logic, a fibration formalizes the idea of logical propositions varying with the contexts in which they are defined: If $p: E\to B$ is a (Cartesian) fibration, the base category $B$ is thought of as a category of contexts, and for any context $b\in B$, the fiber $X_b$ of $p$ over $b$ is thought of as the category of propositions in the context $b$ (with morphisms being proofs, potentially all identified to collaps the category to a preordered set).
Let's look at this principle in the most well-known example of first order predicate logic.
Example: In first order predicate logic, you have a set of sorts, sets of constants and function symbols, and a set of relation symbols. From the sorts, you can form the contexts in which to formulate first order propositions: such a context is just a finite sequence of 'free variables', each of which has some fixed sort. Given such a set of free variables, you can build formulas using the constant, function and relation symbols, plus the usual connectives and the quantifiers.
If you state it like this, this sounds like one big blob, but what's actually going on can be dissected into three clearly separated pieces each of which has a simple categorical description: Context, Logic, and Quantifiers:
Contexts: When precisely defining formulas of predicate logic, one usually starts with the notion of a term: A term on some context of free variables is a well-typed expression built from the function and constant symbols. For example, if we consider the signature of the theory of groups with a single sort $\ast$ for the abstract group, then $(x\cdot e)\cdot y$ would be a term in the context $(x,y)\in\ast\times\ast$.
With your categorical background, you will notice that these notions of context and terms together constitute the free category with finite products over a given set of objects and morphisms. Call it ${\mathbb C}$.
So much for the contextual part - no logic until here!
Logic: Given the notion of terms, formulas can be defined as built from the logical connectives and quantifiers on the basis of the given relational symbols into which terms have been plugged.
Forgetting about terms and quantifiers for a second, over some context $\Gamma=(S_1, ..., S_n)\in{\mathbb C}$ this in particular includes propositional logic over the usual connectives, using the given relation symbols of signature $\Gamma$ as their atomics - again, no terms or quantifiers here.
So, at this point, you have your base category $\mathbb C$ of contexts, and for any context $\Gamma$, you have the Boolean algebra ${\mathbb P}_\Gamma$ of propositions over the matching relation symbols.
How do propositions including non-trivial terms enter this picture? They arise naturally from the idea that if you have some proposition $P$ in a context $\Gamma$ and a morphism of contexts $f: \Gamma^{\prime}\to\Gamma$, you should be able to form a new proposition in context $\Gamma^{\prime}$ by substituting $f$ into $P$. So, you want to connect the Boolean algebra propositions ${\mathbb P}_\Gamma$ over $\Gamma$ to the Boolean algebra of proposition ${\mathbb P}_{\Gamma^{\prime}}$ over $\Gamma^{\prime}$ through a substitution morphisms, call it $f^{\ast}: {\mathbb P}_{\Gamma}\to {\mathbb P}_{\Gamma^{\prime}}$.
With this at hand, you can even define the notion of morphism between propositions over different contexts: If $P\in {\mathbb P}_{\Gamma^{\prime}}$ and $Q\in {\mathbb P}_{\Gamma}$, a morphism $P\to Q$ is a substitution of contexts $f: \Gamma^{\prime}\to \Gamma$ such that $P\Rightarrow f^{\ast}Q$ in the Boolean algebra ${\mathbb P}_{\Gamma^{\prime}}$. In particular, any such morphism has an underlying substitution morphism of contexts, so if we make the union of all ${\mathbb P}_{\Gamma}$ into a category $\mathbb P$ by means of the just described morphisms, we have a functor ${\mathbb P}\to {\mathbb C}$.
Let's analyze what we've actually built here: A functor $p: {\mathbb B}\to {\mathbb C}$ with the following properties:
Calling this a fibration for propositional logic, what we have built is the initial one.
Quantifiers: Finally, how do quantifiers enter the picture?
Regardless of whether it's $\exists$ or $\forall$, a quantifier transforms statements $P\in {\mathbb P}_\Gamma$ in some context $\Gamma=(S_0,S_1,...,S_n)$ into statements over the smaller context $\partial\Gamma := (S_1,...,S_n)$, i.e. they constitute morphisms/functors $\exists_{S_0},\forall_{S_0}: {\mathbb P}_{\Gamma}\to {\mathbb P}_{\partial\Gamma}$. On the other hand, we have the projection morphism $\pi: \Gamma\to\partial\Gamma$, and associated to it the substitution morphism $\pi^{\ast}: {\mathbb P}_{\partial\Gamma}\to {\mathbb P}_{\Gamma}$ formally introducing a new free variable of sort $S_0$ which however does not occurr in the formula.
How do these relate? A moment's thought will reveal that they are categorically adjoint: The implication $(\exists_{S_0} P)\Rightarrow Q$ over $\partial\Gamma$ is equivalent to the implication $P\Rightarrow\pi^{\ast}Q$ over $\Gamma$ (usually the $\pi^{\ast}$ is suppressed); similarly $Q\Rightarrow (\forall_{S_0} P)$ over $\partial\Gamma$ is equivalent to $\pi^{\ast} Q\Rightarrow P$ over $\Gamma$.
Hence, from the categorical point of view, adding quantifiers means requiring/forcing the presence of left and right adjoints to the pullback functors. For the existential quantifier, for example, this means that $p: {\mathbb P}\to {\mathbb C}$ is not only Cartesian, but also coCartesian.
In the end, first order predicate logic yields the initial Cartesian fibration with left- and right adjoints over the given set of contexts, functions and relations.
That got longer than planned, but the punchline is simple: Logical systems give rise to initial categorical fibrations, in which contexts are reflected in the base, the core logic is reflected in the fibres, and the quantifiers are reflected in the presence of adjoints.
With this in mind, you can begin to think of fibrations coming from other fields, e.g. geometry, in a logical way, and maybe gain some better intuitive understanding for them. For example, you might find the similarity of the logical equivalence of $(\exists_{S} P)\wedge Q\Leftrightarrow \exists_S (P\wedge \pi^{\ast} Q)$ and the projection formula $f_!{\mathscr F}\otimes {\mathscr G}\cong f_!({\mathscr F}\otimes f^{\ast}{\mathscr G})$ from geometry interesting. See https://mathoverflow.net/questions/18799/ubiquity-of-the-push-pull-formula
If you find this interesting, have a look in Bart Jacob's Categorical Logic and Type Theory.
A classical example of a fibration is the codomain fibration on a finitely complete category $\mathcal{C}$-- that is, the functor from the arrow category $cod:\mathcal{C}^\to \to \mathcal{C}$ with action on objects $(f:c\to d)\mapsto d$ and action on morphisms taking $\langle g_0:c\to c',g_1:d\to d'\rangle:(f:c\to d)\to(f':c'\to d')$ to $g_1$. Note that for any $c\in\mathcal{C}$, the collection of objects $f\in\mathcal{C}^\to$ with $cod(f)=c$ and morphisms with $cod(\langle g_0,g_1\rangle)=id_c$ forms a category (called the fibre over $c$); in fact, the category $(\mathcal{C}\downarrow c)$. Moreover, pullback along a morphism $h:d\to c$ in $\mathcal{C}$ allows you to take an object of $(\mathcal{C}\downarrow c)$ to one in $(\mathcal{C}\downarrow d)$, and similarly for morphisms.
Here one would like to say that $cod$ is actually encoding a functor $(\mathcal{C}\downarrow-):\mathcal{C}^{op}\to\mathbf{Cat}$; morally, this is what's going on, but there are two problems that prevent me from dropping the qualifier "morally". First, a composition and pullback don't strictly commute: $f^*g^*(x)$ is not generally identical to $(gf)^*(x)$ (though they're isomorphic), so the proposed functor to $\mathbf{Cat}$ isn't strictly functorial. Second, a morphism $f$ may have many pullbacks along a given morphism $h$. So the "pullback along $h^*$" operation that we want to think of as a functor (a morphism in $\mathbf{Cat}$) isn't actually even functorial unless we're able to choose a particular pullback for every pullback diagram.
Nevertheless, we can say intelligible things about codomain fibrations, even talk about "right adjoints" to pullback, as in the case of locally Cartesian closed categories, when what we have a right adjoint to isn't strictly even a functor.
Why have I talked so much about the codomain fibration? You have probably been exposed to the notion that you can think of a morphism $d\to c$ as an abstract family indexed by by $c$, and pullback is a reindexing operation (like the operation where, given a family of sets $\{A_i\}_{i\in I}$ and a function $f:J\to I$, you can make a new family $\{A_{f(j)}\}_{j\in J}$). The codomain fibration is a nice example of a situation where it's easy to use the metaphor of indexed families and reindexing, while finding easy examples of where the reindexing operation isn't quite as nice as the case of set-indexed families. This is what fibrations are meant to model in their full generality-- given a fibration $p:\mathcal{E}\to\mathcal{C}$, we think of the fibre over an object of $\mathcal{C}$ as a category structures indexed by that object, and we are given a contravariant "reindexing" operation which is well behaved enough to work with, but general enough that we're not tossing out perfectly good examples like codomain fibrations. They also give you a venue to think about things like $\mathcal{E}$-valued functors on categories internal to $\mathcal{C}$, when this might otherwise be hard to even phrase.
I haven't gone into the details of exactly what makes a fibration because the definition is perfectly available, but references like Borceux's Handbook of Categorical Algebra, vol 2, or Jacobs are good places to learn more.
