Split Fibration

Definition

A split fibration is a Grothendieck Fibration $p:\mathcal{E}\Rightarrow \mathcal{B}$ equipped with a cleavage whose induced reindexing is strictly functorial. Concretely, a cleavage assigns to every $e\in \mathcal{E}$ and $u\in \mathcal{B}[b^{\prime },p(e)]$ a cartesian lift $\chi (u,e)\in \mathcal{E}[u^{\ast }e,e]\text{with}p(\chi (u,e))=u,$ and the fibration is split when these choices satisfy the strict laws $({\mathrm{id}}_b{)}^{\ast }={\mathrm{Id}}_{{\mathcal{E}}_b},(u\circ v{)}^{\ast }=v^{\ast }\circ u^{\ast }$ on the nose (no coherence isomorphisms needed).

Equivalently, writing ${\mathcal{E}}_b=\{e\in \mathcal{E}\mid p(e)=b\}$, a split fibration determines a strict functor $(-{)}^{\ast }:{\mathcal{B}}^{op}\Rightarrow \mathbf{Cat},b\mapsto {\mathcal{E}}_b,u\in \mathcal{B}[b^{\prime },b]\mapsto u^{\ast }:{\mathcal{E}}_b\Rightarrow {\mathcal{E}}_{b^{\prime }}.$

Properties

• Strict functorial reindexing: identities and composition in the base are preserved strictly by $(-{)}^{\ast }$.
• Canonical in the discrete case: every Discrete Fibration is split, since cartesian lifts (hence reindexing) are unique.
• Split replacement: every Grothendieck Fibration is equivalent over $\mathcal{B}$ to a split one (via the Grothendieck construction of an equivalent strict functor ${\mathcal{B}}^{op}\Rightarrow \mathbf{Cat}$).
• Stability:
  • Pullback of a split fibration along any functor is split (with the pulled-back cleavage).
  • Products and retracts of split fibrations are split.
• Beck–Chevalley on the nose: for strictly commuting pullback squares in the base, naturality and base-change identities for $(-{)}^{\ast }$ hold as equalities rather than up to isomorphism.

Relation to Cloven Fibration

A split fibration is a cloven fibration whose chosen lifts compose strictly:

• $\chi ({\mathrm{id}}_b,e)={\mathrm{id}}_e$,
• $\chi (u\circ v,e)=\chi (v,e)\circ \chi (u,v^{\ast }e)$. Thus, “split” is extra structure/strictness on top of being cloven, not a different kind of fibration.

The dual notion is a split Opfibration, with strictly functorial pushforwards $({\mathrm{id}}_b{)}_{!}=\mathrm{Id}$ and $(v\circ u{)}_{!}=v_{!}\circ u_{!}$.

Examples

• Simple Fibration: If $P:{\mathcal{B}}^{op}\Rightarrow \mathbf{Cat}$ is a strict functor, its Grothendieck construction $\int P\Rightarrow \mathcal{B}$ is a split fibration with reindexing given by $P(u)$.
• Family Fibration over Set: For $E:B\to \mathbf{Set}$, substitution along functions is strictly functorial, yielding a split fibration ${\pi }_1:{\sum }_{b\in B}{E}_b\to B$.
• Codomain Fibration: If a category has a strictly functorial choice of pullbacks, then $p:{\mathcal{C}}^{\to }\Rightarrow \mathcal{C}$ is split, with cartesian morphisms the chosen pullback squares.

Related Concepts

• Fibration
• Grothendieck Fibration
• Cloven Fibration
• Opfibration
• Discrete Fibration
• Family Fibration
• Simple Fibration
• Codomain Fibration
• Street Fibration
• Cartesian Fibration
• Cocartesian Fibration

References

jacobs1999-categorical-logic riehl2014-categorical-homotopy-theory