(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 Grothendieck opfibration. Under the Grothendieck construction it corresponds to the pseudofunctor
that sends each object to the overcategory .
If has all pullbacks, then the functor is in addition a Grothendieck fibration, hence a bifibration. Traditionally it is this fibered aspect is emphasised (and it even motivates the notion of Cartesian fibrations). A right adjoint of exists for every morphism in iff C is a locally cartesian closed category.
In any case, 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.
By restricting our attention to a subset of morphisms in the codomain fibration and using the notion of the skeleton of a fibration, we may define a fibration on a category with pullbacks called the subobject fibration whose fibers are categories of subobjects for objects of .
Beginning with the codomain fibration on a category with pullbacks (now writing for the arrow category), we restrict our attention to the subcategory
the full subcategory of whose objects are monomorphisms in , called the monomorphism category of . The resulting functor
is again a fibration since monomorphisms are stable under pullback; we will call this the monomorphism fibration of . The fibers for are thin categories since parallel monos in a slice category are equal, but they aren’t subobject categories since antisymmetry is only weakly satisfied – objects with antiparallel arrows between them are necessarily isomorphic, but not necessarily equal. To remedy this, we take the fibered skeleton of the monomorphism fibration; briefly, we convert it into an indexed category using the Grothendieck construction, take the skeleton of each index category, then turn it back into a fibration using the Grothendieck construction in the other direction. The resulting fibration is denoted
and called the subobject fibration of , and the fibers are skeletal thin categories, also known as poset categories.
If we take then the fibers of the monomorphism fibration are proper classes consisting of all sets isomorphic to subsets of , which isn’t what we want. The fibers consist of one representative from each isomorphism class of sets isomorphic to subsets of , and is thusly isomorphic to the powerset of viewed as a poset. That is, as posets, with equality holding if we choose the right representatives.
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”.
(…)
Last revised on April 1, 2023 at 16:56:04. See the history of this page for a list of all contributions to it.