(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
For any category, there is a functor
from the arrow category that sends each morphism to its codomain .
This functor is always an opfibration. It corresponds under the Grothendieck construction to the pseudofunctor
that sends each object to the overcategory .
If has all pullbacks, then the functor is in addition a fibration, hence a bifibration. Traditionally, though, its fibered aspect is emphasised (and it even motivates the notion of cartesianess for categories over categories). A right adjoint of exists for every morphism in iff C is a locally cartesian closed category.
This functor is called the codomain fibration of .
Some say basic fibration or self-indexing or the fundamental fibration — anything with so many names must be important!
If instead of the codomain the domain is used, one obtains the dual notion: domain opfibration.
We spell out the details of the functor, of its cartesian and opcartesian morphisms and their properties.
Recall from the discussion at arrow category that the objects in are morphisms in and the morphisms in are the commutative squares in of the form
with the obvious composition.
The functor is given on objects by the codomain (= target) map, and on morphisms it gives the lower arrow of the commutative square.
If we write for the arrow category, where is the interval category , then this functor is the hom-functor applied to the inclusion
That the functor is an opfibration means that for each object of , each morphism in has a lift to a morphism
in that is a opcartesian morphism.
Such a lift is given by
For given any commuting triangle
in , and any lift
of , there is the unique lift
such that
If has pullbacks, then is in addition a fibered category in the sense of Grothendieck:
for every object in , the cartesian lift of a morphism in is given by the morphism
Because for
any commuting triangle in , and for
any lift of in , which by the commutativity of the triangle we may write as
there is, precisely by the universal property of the pullback, a unique morphism, in such that this factors as
Recall that in an opfibration , the direct image of an object along a morphism is the codomain of the opcartesian lift of .
By the above discussion this means that in the codomain opfibration the direct image of an object in along some morphism is the composite morphism in , regarded as an object in : this yields the functor
of overcategories obained by postcomposition with .
Recall that in an fibration , the inverse image of an object along a morphism is the domain of the cartesian lift of .
By the above discussion this means that in the codomain fibration the inverse image of an object in along some morphism is the morphism out of the pullback in , regarded as an object in : this yields the functor
of overcategories obained by pullback.
For every morphism in , the direct and inverse image functors are a pair of adjoint functors
with left adjoint and right adjoint, .
By the above discussion, the adjunction isomorphism
is given by the universal property of the pullback operation, which says that morphisms
factor uniquely through the pullback
and hence uniquely correspond to morphisms
If is a model category, and a morphism in , we can consider the induced model structure on the overcategories , and . The adjoint pair
is then a Quillen pair.
Since the codomain fibration is a bifibration when has all pullbacks, there is a notion of monadic descent in this case. Details on this are at monadic descent for codomain fibrations.
We discuss the codomain fibration in higher category theory.
A categorification in dimension 2 (see 2-category theory) is a codomain 2-fibration, whose main example is over .
Mike Shulman: I still don’t believe that that is a 2-fibration. How do you lift the 2-cells?
David Roberts: How does one lift the 2-cells in a 2-fibration anyway? The case of (using weak 2-functors in ) should in my opinion be an guiding example for this. Although, perhaps it would be better to consider (at least at first) the underlying (2,1)-category or even the (2,1)-category .
Mike Shulman: I think the guiding example of a 2-fibration should actually be , as in Hermida’s paper. There, you can lift the 2-cells, because in each fibration you can lift the 1-cells.
Let be an (∞,1)-category.
The codomain fibration
is an coCartesian fibration.
It is classified under the (∞,1)-Grothendieck construction by
where on the right we have the over-(∞,1)-category.
This is a special case of (Lurie, corollary 2.4.7.12).
For an (∞,1)-topos, this is the canonical (infinity,2)-sheaf.
(…)
an (∞,1)-topos the codomain fibration is the dependent sum
where is the object classifier, of some size. This is the internal universe. Since the slice (∞,1)-topos is the context given by , in a precise sense is the “context of the universe”. And so this says that the codomain fibration is the “context of the universe” regarded over the base -topos which is the “outermost universe”.
(…)
Secton 2.4.7 of
Last revised on April 14, 2014 at 23:47:59. See the history of this page for a list of all contributions to it.