essential fiber



Category theory

Homotopy theory

homotopy theory, (∞,1)-category theory, homotopy type theory

flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed

models: topological, simplicial, localic, …

see also algebraic topology



Paths and cylinders

Homotopy groups

Basic facts





The notion of essential fiber of a functor is an enhancement of the naive notion of fiber which, for functors, would violate the principle of equivalence. It is a category-theoretic version of a homotopy fiber.


Let p:EBp:E\to B be a functor and bBb\in B an object. The essential fiber of pp over bb is the following category:

  • its objects are pairs (e,ϕ)(e,\phi) where eEe\in E is an object and ϕ:p(e)b\phi\colon p(e)\cong b is an isomorphism.
  • its morphisms (e,ϕ)(e,ϕ)(e,\phi)\to (e',\phi') are morphisms f:eef\colon e\to e' in EE such that ϕp(f)=ϕ\phi' \circ p(f) = \phi.

The essential fiber can be identified with the pseudopullback of pp along the functor b:1Bb\colon 1\to B from the terminal category which picks out the object bb. It can also be identified with a homotopy fiber in the canonical model structure on Cat. When groupoids are identified with homotopy 1-types, the essential fiber actually coincides with the classical homotopy fiber (up to equivalence).

Relationship to fibrations

If pp is an isofibration, then any of its essential fibers is equivalent to the corresponding strict fiber. This includes the case when pp is a Grothendieck fibration.

On the other hand, when pp is a Street fibration (the version of Grothendieck fibration which respects the principle of equivalence), then essential fibers do not coincide with strict fibers, and essential fibers are the more useful notion. In particular, the correspondence between fibrations and pseudofunctors only goes through for Street fibrations if one defines the pseudofunctor using essential fibers.

Last revised on October 4, 2021 at 09:25:35. See the history of this page for a list of all contributions to it.