Notes on Category Theory, 5: Fibers

References:

As a study note, there is nothing nontrivially original. Currently the references include Categorical Logic and Type Theory(by Jacobs).

This post is mostly about Fibration.

Fibration & Category

In Jacobs, the starting point is just fibrational category theory. Even though, as nlab suggests, to have a categorical model for STLC(Simply Typed Lambda Calculus) or Dependent Typed Lambda Calculus, a (locally) closed cartesian category is basically enough. But no one can stop Jacobs using more modern language.

A functor $p:\mathbb{E} \rightarrow \mathbb{B}$ is a fibration if for every $Y \in \mathbb{E}$ and $u (\in \mathbb{B}): I \rightarrow pY$, there is a Cartesian Morphism $f (\in \mathbb{E}):X\rightarrow Y$ above $u$ (i.e. $pf = u$).

With functor $p:\mathbb{E} \rightarrow \mathbb{B}$, an arrow $f:X\rightarrow Y$ is Cartesian over $u :I \rightarrow J$ if

1. $pf = u$

2. for every $g: Z \rightarrow Y$ with the property that $pg$ can be composed by $u$, (i.e. there is a $w$ s.t. $pg = u \circ w$) we have a unique arrow $h$ s.t. $g = f \circ h$ and $ph = w$

and if $f$ is cartesian over $u$, we call $f$ as $u$’s cartesian lifting.

The definition of cartesian morphism is easily demonstrated by the following diagram in the original book.

This uniqueness is talking about the up-to-isomorphism; and there are many more trivial properties to see:

1. if $f,f’$ are both the cartesian lifting of $u$, then there is isomorphism $i$ s.t. $f = f’ \circ i$
2. Given $u,v$ above same map, a cartsian morphism $f$, if $f \circ u = f \circ v$ then $u = v$
3. Cartesian morphism is closed under composition

<summary>To find the isomorphism:</summary>
<p>
    It is easy to see $pf = pf'$ and thus $pf = pf' \circ id$ and $pf' = pf \circ id$. Thus we have two unique arrows $a,b$ s.t. $f = f' \circ a$ and $f' = f \circ b$. Similarly, we can have two unique arrows $i, d$ s.t. $f = f \circ i$ and $f' = f' \circ d$. It is easy to see $i = id, d = id$. and thus $b \circ a = id$, $a \circ b = id$. 
</p>

Example : Codomain Fibration

In this example, we can see our old friends arrow category and slice category.

$cod: \mathbb{B}^\rightarrow \rightarrow \mathbb{B}$ is a fibration

iff the $\mathbb{B}$ has pullback

<summary>Carteisan morphism gives a pullback:</summary>
<p>
    Given $A \xrightarrow{f} X \xleftarrow{g} B$ in ${\cal B}$, we have a cartesian lifting of $f$ to ${\cal B}^ \rightarrow$, denoted $(f', f) : (g' : {\LARGE \downarrow}^C_ A) \rightarrow (g : {\LARGE \downarrow}^B_ X)$. 

    <br/>

    It is easy to see $(f', f)$ as a pullback. Consider $A \xleftarrow{u} C' \xrightarrow{v} B$, and $f \circ u = g \circ v$, we get an another object and an arrow $u \in {\cal B^\rightarrow_0}$ and $(v, f): u \rightarrow g$. Due to the cartesian lifting $f'$ and the fact that $f = f \circ id$, there will be a unique arrow from $u$ to $g'$. The 'domain' part of the unique arrow is obviously the mediating arrow $C' \rightarrow C$ we want.

    <br/>

    Uniqueness is ensured by the uniqueness of the cartesian morphism. 
</p>

<summary>A pullback gives cartesian morphism:</summary>
<p>
    
    <!-- ![](assets/img/2019-10-13-16-48-57.png) -->
    <img src="/assets/img/2019-10-13-16-48-57.png">

    <br/>

    Note that the uniqueness is ensured by the pullback, and also note that the uniqueness means 

    <br/>

    we have a unique arrow $h$ s.t. $g = f \circ h$ and ${\LARGE ph = w}$

</p>

Observe that given a functor $F:{\mathbb{C}} \rightarrow \mathbb{D}$, if we denote $F^{-1}(X)$ as the collection of objects in $\mathbb{C}$ that will be mapped to $X$.

Now for a fixed $X$, $F^{-1}(X)$ can actually become a category, by taking the arrows to be $F^{-1}(id_X)$. This category will be called fibre category.

Now consider if the above $F$ is the codomain fiberation, what is the category constructed? Slice Category!

Example : Set Indexed Category ($Fam$)

$Fam(\mathbb{C})$ is a category

objects: $(I,X)$ where $I \in$ Set and $X: I \rightarrow \mathbb{C_0}$ (that maps elements in $I$ to objects in $\mathbb{C}$). We most of the time will use $X_i$ to denote $X(i)$ and thus an object is denoted as $\{X_i\}_{i\in I}$

arrows : $(u: I \rightarrow J$, {$f_i: X_i \rightarrow X_{u(i)}$} where $i \in I$) as a tuple of arrows and collections of arrows.

We would have a fibration $Fam(\mathbf{Set}) \rightarrow \mathbf{Set}$ s.t. mapping objects $\{X_i\}_{i \in I} \mapsto I$

Claim : That is really a fibration (i.e. cartesian lifting exists.)

Cloven & Split

Recall the definition of substitution functor:

Given fibre ${\LARGE{\downarrow}}^{\cal E}_ {\cal B}$ and $u : I \rightarrow J \in {\cal B_1}$

$u$ can have several cartesian lifting, in which if we fix one as the choice then we get the lifting $\bar{u}(X): u^{*}(X) \rightarrow X$

In this context,

• after this fixing, we call this fibration cloven with a cleavage
• $u^{*}$ is an induced functor ${\cal E}_ J \rightarrow {\cal E}_ I$ since it preserves the composition of the arrows (because of cartesian morphism)

Surprisingly, $u^{*} \circ v^{*}$ is naturally isomorphic to $(v \circ u)^{*}$, mostly because cartesian morphism is closed under composition. We also have $id \cong id^{*}$.

<summary>To Show they are both naturally isomorphism:</summary>
$u^{\\*} \circ v^{\\*} \cong (v \circ u)^{\\*}$
<br/>
For arbitrary $X$, $\bar{u} \circ \bar{v} (X) : u^{\\*} \circ v^{\\*}(X) \rightarrow X$ is a cartesian morphism because cartesian morphism closed under composition. Of course, so is $\bar{v \circ u}$. We can also easily see both cartesian morphism are above same map, so there is an iso between $u^{\\*} \circ v^{\\*}$ and $ (v \circ u)^{\\*}$
<br/>
$id \cong id^{\\*}$
<br/>
Because $id$, $id^{\\*}$ are both cartesian morphism over $id$.

<br/>
Natruality: The following diagram commutes, 
<br/>
<!-- ![](assets/img/2019-10-13-21-48-44.png) -->
<img src="/assets/img/2019-10-13-21-48-44.png">
<br/>

Thus we can conclude $f \circ (\bar{u} \circ \bar{v}(X)) = (\bar{u} \circ \bar{v}(Y)) \circ d^{-1} \circ  (v \circ u)^*(f) \circ c$, and due to the definition of $u^* \circ v^*(f)$, (the unique arrow that makes the left square commutes), we can conclude $u^* \circ v^*(f) = d^{-1} \circ  (v \circ u)^*(f) \circ c$, which is exactly the naturality.

if $u^{*} \circ v^{*} \xrightarrow{\cong} (v \circ u)^{*}$ and $id \xrightarrow{\cong} id^{*}$ are identities, then this fibration is split

Example: Show that fibration ${\LARGE{\downarrow}}^{\mathbf{Set^\rightarrow}}_ {\mathbf{Set}}$ defined by the canonical pullback is a split fibration.

Example: Show that fibration ${\Large \downarrow}^{\mathbf{Fam}({\cal C})}_ {\mathbf{Set}}$ is a split by lifting $I \xrightarrow{u} J$ to $(I, (Y_ {u(i)})_ {i \in I} \xrightarrow{(u, id)} (J, (Y_ j)_{j \in J})$

It is easy to notice that $X \mapsto {\cal E}_ X$ and $u \mapsto u^{*}$ can together become a pseudo-functor. It is almost a functor since $u^{*} \circ v^{*} {\cong} (v \cdot u)^{*}$ instead of equal. In other words, a split fibration can induce a real functor. This pseudo-functor/functor ${\cal B}^{op} \rightarrow \mathbf{Cat}$ induces the concept of ${\cal B}$-indexed category/split ${\cal B}$-indexed category.

Change-of-Base

Recall

Given $\mathbb{A} \xrightarrow{f} \mathbb{C} \xleftarrow{g} \mathbb{B}$ where $\mathbb{A}, \mathbb{B}, \mathbb{C}$ are categories

an ordinary pullback is an object (category) $\mathbb{X}$

where objects are ${(A, B): f(A) = g(B)}$

and arrows are ${(u,v): f(u) = g(v)}$

It can easily proved that an ordinary pullback is a pullback.

<summary>To Show it is a pullback:</summary>
<p>

</p>

Now we can give a definition on Change-of-base.

(Change-of-Base) Given $\mathbb{A} \xrightarrow{f} \mathbb{B} \xleftarrow{p} \mathbb{E}$ where $p$ is a fibration, then we have the ordinary pullback $\mathbb{A} \xleftarrow{\pi_1} \mathbb{X} \xrightarrow{\pi_2} \mathbb{E}$

and also $\pi_1$ is a fibration, which is cloven/split given $p$ is cloven/split.

<summary>To Show it is a fibration:</summary>
<p>

</p>

Fibrations $\mathbf{Set}^\rightarrow \rightarrow \mathbf{Set}$ and $Fam(\mathbf{Set}) \rightarrow \mathbf{Set}$ are very much the same.

The formal statement is as below:

Exercises, mostly repeating the book, and exaggerate the details

Some exercises are put here.

There is an equivlanece of categories in the following commutative diagram

where $Fam(\mathbf{Sets}) \xrightarrow{\simeq} \mathbf{Sets}$ :=

$(X_ i)_ {i \in I} \mapsto$ [the arrow $(\coprod_ {i \in I} X_ i) \xrightarrow{\pi} I$]

<summary>To Show it is an equivalence:</summary>

    Denote the mapping $Fam(\mathbf{Sets}) \xrightarrow{\simeq} \mathbf{Sets}$ as $F$,

    <br/>
    
    Denote the mapping [the arrow $X \xrightarrow{f} I$] $ \mapsto (f^{-1}(i))_ {i \in I}$ as $G$

    <br/>

    Let $F$ become a functor by throwing the arrow $(u, (f_ i: X_ i \rightarrow Y_ {u(i)})_ {i \in I})$ to $(\coprod_ {i \in I}f_i, u)$. For the former one (in the tuple), it is obviously mapping $\coprod X$ to $\coprod Y$. It is easy to check commutativity and see that is an arrow in the arrow category and thus $F$ is a functor.

    <br/>

    Let $G$ become a functor by throwing the commutative arrow (in the arrow category) $(v:X\rightarrow Y, u:I \rightarrow J)$ to $(u, (v)_ {i \in I})$ since it is easy to prove $v : f^{-1}(i) \rightarrow g^{-1}(u(i))$

    <br/>

    Now we have to give $\eta : G\circ F \rightarrow Id$ and $\gamma :F \circ G \rightarrow Id$.

    Given $(X_ i)_{i \in I}$, $\eta((X_ i)_{i \in I}) : G(F((X_ i)_{i \in I})) \rightarrow (X_ i)_{i \in I} = (i, X_ i)_{i \in I} \rightarrow (X_ i)_{i \in I}$. Thus $\eta(X) = \pi_2$.

    <br/>

    Given $X \xrightarrow{f} I$, $\gamma(f): F(G(f)) \rightarrow f = [\coprod_ {i \in I} f^{-1}(i) \rightarrow I] \rightarrow [X \xrightarrow{f} I]$.
    Thus $\gamma(f) = (\pi_2, id)$

    <br/>

    Now we need to check commutativity for the natrual transformations.

    <!-- ![](/assets/img/2019-09-30-21-24-50.png) -->
    <!-- <img src="/assets/img/2019-09-30-21-24-50.png"> -->
     <img src="/assets/img/2019-09-30-21-48-03.png">
    <br/>

    The other one is similar.

Recall the definition of $\omega$-Set:

objects are $(X \in \mathbf{Set_0}, E_X : X \rightarrow \mathbb{N})$.

arrows are $f: X \rightarrow Y$ such that there exists a natural number $e$ tracking $f$, i.e. for all $x \in X$, $\varphi_ e(E_ X(x)) \subseteq E_ Y(f(x))$ (can you see a commutative diagram here?)

Here $\varphi_e$ is the $e$-th partial recursive function (since partial recursive function is enumerable just like turing machines are enumerable, details please see any recursion theory)

Notice that the existence of the number is enough, we don’t care about what the tracking number actually is. In other words, two arrows are equal when they are same functions in Set, even if they have different tracking number.

$\omega$-Set has finite limit and exponential.

<summary>To Show it has finite limit and exponential:</summary>

    Recall that if a category has finite product and equalizers, then it has finite limit.

    <br/>

    Note that in the $\omega$-**Set**, you can informally see that the arrows are just "the same as" the arrows in the underlying **Set**. Thus the construction of the finite product, equalizers and exponentials are the same as **Set**, the only question is the tracking number.

    <br/>

    <strong>How to construct finite product.</strong>

    <br/>

    We claim that $(X, E_ X) \times (Y, E_ Y) \cong (X \times_{\mathbf{Set}} Y, E_ {X \times Y})$, where $E_ {X \times Y}(x,y) = ${ $ \langle n, m \rangle: n \in E_ X(x), m \in E_ Y(y) $ } and $\langle \rangle$ is effective encoding. 

    <br/>
    
    Let P be arbitrary and $ (X, E_ X) \xleftarrow{f} (P, E_ P) \xrightarrow{g} (Y, E_ Y)$. 
    <br/>
    We would have $ [ f, g ] : P \rightarrow (X \times_{\mathbf{Set}} Y, E_ {X \times Y})$ defined in the obvious way. The only thing non-obvious is the tracking number. Note we have partial recursive functions $\varphi_ f$ and $\varphi_ g$, in which case, $\forall p \in P, \varphi_ f(E_ P (p)) \subseteq E_ X(f(p)) $ and $\varphi_ g(E_ P (p)) \subseteq E_ Y(g(p)) $ thus we have $\varphi_ {\langle f, g\rangle}$ as a partial recrusive function $\varphi_ {\langle f, g\rangle} (x) := \langle \varphi_ f(x),\varphi _g (x)  \rangle$ (here $\langle \rangle$ is effective encoding) and thus $\varphi_ {\langle f, g\rangle}(E_ P(p)) \subseteq E_ {X \times Y}(f(p),g(p)) = E_ {X \times Y}([ f,g ] (p))$.

    <br/>
    Uniqueness of the arrow is ensured by the definition since any two arrows are equal when they are some **Set**-functions (don't care tracking number); and also this is the construction introduced in **Set**, thus it is unique even in the context of **Set**. 

    <br/>
    <strong> How to construct equalizer. </strong>
    <br/>

    Let $f, g : (X, E_ X) \rightarrow (Y, E_ Y)$ be two arrows on two arbitrary objects.  We have a set $S :=$ {$ x:f(x) = g(x)$}. We can see there is an object $(S, E_ S)$ s.t. $E_ S(x) := E_ X(x)$ and we have an arrow $e : (S, E_ S) \hookrightarrow (X, E_ X)$ (actually inclusion), with partial recursive function $\varphi_ e(n) := n$. 

    <br/>

    We also have to show that its universal property, where 
    the reason for uniqueness is the same as above. What remains is the reason for existence (and its tracking number). The thing is, given arbitrary $k$ s.t. $f \circ k = g \circ k$, the arrow points to the $S$ is exactly $k$ itself. The tracking number is also given by $k$.

    <br/>


    <br/>
    <strong> How to construct exponential. </strong>
    <br/>

    The construction is not so obvious. Because we are dealing with computable(recursion theory/computablity theory) function, not arbitrary function any more.

Recall the definition of $PER$:

objects are partial equivalence relations (relations transitive and symmetric)

arrows are

$PER$ is thought to be a complete lattice: $\bigvee_ i S_ i = \bigcap \{ R \in PER : R \supseteq \bigcup_ i S_ i \} $.

Question: Why not $\bigvee_ i S_ i = \bigcup_ i S_ i $.

It is also said it is easy to see $PER$ is closed under intersection.

Recall the definition of subobject, which is basically an equivalence class of monos. Then recall the definition that a relation on an object $I$ in category ${\cal B}$ with finite limits is a subobject $R \rightarrowtail I \times I$; and a category $Rel({\cal B})$ is

objects: subobjects with codomain of $I \times I$ for some object $I$ in ${\cal B}$

arrows: an arrow $u: I \rightarrow J \in {\cal B_0}$ that satisfies the following commutative diagram

After categorify the relations, the reflectivity, symmetricity and transitivity are:

Let’s verify the transitivity in Set context: (TBD).