Family Fibration

Definition

A family fibration is the Grothendieck Fibration over Set obtained as the Grothendieck construction of the pseudofunctor $P:{\mathbf{Set}}^{op}\Rightarrow \mathbf{Cat},P(B):={\mathbf{Set}}^B,$ with reindexing given by precomposition. Concretely, its total category has:

• Objects: pairs $(B,E)$ with a set-indexed family $E:B\to \mathbf{Set}$ (i.e. $(E_b{)}_{b\in B}$).
• Morphisms: a morphism $(u,\phi ):(B^{\prime },E^{\prime })\to (B,E)$ consists of a function $u:B^{\prime }\to B$ and a family of functions ${\phi }_b:E_{b^{\prime }}^{\prime }\to E_{u(b^{\prime })}$, equivalently a natural transformation $E^{\prime }\Rightarrow u^{\ast }E$.

The projection $p:\mathrm{Fam}(\mathbf{Set})\Rightarrow \mathbf{Set},(B,E)\mapsto B,(u,\phi )\mapsto u,$ is a Grothendieck fibration; cartesian liftings are given by reindexing families along functions.

Fibres and morphisms

• Fibre over $B\in \mathbf{Set}$: the functor category ${\mathbf{Set}}^B$ (families over $B$ and fibrewise maps).
• Vertical morphisms (over ${\mathrm{id}}_B$): pointwise functions $({\phi }_b:E_b\to E_b^{\prime }{)}_{b\in B}$.

Reindexing

For $u:B^{\prime }\to B$ and $E:B\to \mathbf{Set}$, reindexing is strict precomposition $u^{\ast }E:=E\circ u:B^{\prime }\to \mathbf{Set},(u^{\ast }E{)}_{b^{\prime }}=E_{u(b^{\prime })}.$ On morphisms, $u^{\ast }$ acts pointwise. This yields a strictly functorial action: $({\mathrm{id}}_B{)}^{\ast }={\mathrm{Id}}_{{\mathbf{Set}}^B},(u\circ v{)}^{\ast }=v^{\ast }\circ u^{\ast }.$

Cloven and split structure

With reindexing given by strict precomposition, the cleavage choosing the canonical cartesian liftings makes $p:\mathrm{Fam}(\mathbf{Set})\Rightarrow \mathbf{Set}$ a Split Fibration (hence in particular a Cloven Fibration).

Relation to set-indexed families and comprehension

• As objects, $(B,E)$ is exactly a Set-Indexed Family over $B$.
• The associated total space and projection ${\pi }_1:{\sum }_{b\in B}{E}_b\to B$ are the comprehension of the family $E$. The family fibration organises all such projections uniformly over varying bases and families.
• In logical terms, predicates over $B$ are families $E:B\to \mathbf{Set}$; reindexing $u^{\ast }$ is substitution along $u$. Left/right adjoints to $u^{\ast }$ (when they exist) model dependent sums/products.

Examples

• Constant family: for a fixed set $F$, the object $(B,\lambda b.F)$ has total space $B\times F$ and projection $B\times F\to B$.
• Pullback of families: given $u:B^{\prime }\to B$, the cartesian lift of $u$ at $(B,E)$ is $(u,\mathrm{id}):(B^{\prime },u^{\ast }E)\to (B,E)$.
• Slices via comprehension: a function ${\pi }_1:{\sum }_{b\in B}{E}_b\to B$ recovers $E$ by fibres $E_b={\pi }_1^{-1}(b)$.

Related Concepts

Fibration Grothendieck Fibration Cloven Fibration Split Fibration Set-Indexed Family Simple Fibration Codomain Fibration Opfibration Dependent Sum Dependent Product

References

jacobs1999-categorical-logic