2.9. Full subfibrations and figure shapes [002J]

In a category $E$, a morphism $f : x\to y$ can be thought of as a “figure” of shape $x$ drawn in $y$. For instance, if $x$ is the point (i.e. $x=\ObjTerm{E}$) then a morphism $x\to y$ is a “point” of the “space” $y$. We refer to $x$ as the figure-shape in any such scenario. The perspective of morphisms as figures is developed in more detail by Lawvere and Schanuel (Conceptual Mathematics: A First Introduction to Categories, 2009).

It often happens that a useful class of figure shapes can be arranged into a set-indexed family $\prn{u\Sub{i}}\Sub{i\in I}$; viewed from the perspective of the family fibration $\FAM{E}$ (Section 2.7 [0006]), this family is just a displayed object $\bar{u}$ over $I$ and then a figure shape “in” this family is given by any cartesian morphism $\bar{z}\to\bar{u}$. We will generalize this situation to the case of an arbitrary fibration, by constructing the full subfibration spanned by displayed objects equipped with a cartesian morphism into $\bar{u}$ in Construction 2.9·a [0010] below.

[0010] Construction 2.9·a (The full subfibration associated to a displayed object).

Let $E$ be a cartesian fibration over $B$; then any displayed object $\bar{x} \in E\Sub{x}$ induces a full subfibration $\FullSubfib{\bar{u}}\subseteq E$ spanned by displayed objects that are classified by $\bar{u}$, i.e. arise from $\bar{u}$ by cartesian lift.

1. An object of $\FullSubfib{\bar{u}}\Sub{x}$ is specified by an object $\bar{x}\in E\Sub{x}$ together with a cartesian morphism $\bar{x}\to \bar{u}$.

2. Given $f:x\to y\in B$, a morphism from $\bar{x}\to \bar{u}$ to $\bar{y}\to\bar{u}\in$ over $f$ is given by any displayed morphism $\bar{x}\to\Sub{f}\bar{y}$.

[002K] Definition 2.9·b (Figures and figure shapes in the full subfibration).

Let $E$ be a cartesian fibration and let $\FullSubfib{\bar{s}}\subseteq E$ be the full subfibration determined by a displayed object $\bar{s}\in E$ as in Construction 2.9·a [0010]. We now develop the following vocabulary:

1. We will refer to each object of $\FullSubfib{\bar{s}}$ as a $\bar{s}$-figure shape.

2. A displayed morphism $\bar{z}\to \bar{x}$ is called a $\bar{s}$-figure whenever $\bar{z}\in\FullSubfib{\bar{s}}$.