nLab fibred functor

Redirected from "morphism of fibrations".
Contents

Contents

Idea

Fibred functors are morphisms between fibred categories. They are 1-cells in the 2-category Fib\mathbf{Fib}.

Definition

A fibred functor between fibred categories p:p:\mathcal{E} \to \mathcal{B} and p:p':\mathcal{E}' \to \mathcal{B}' is a pair of functors F 0:F_0:\mathcal{B} \to \mathcal{B}' and F 1:F_1:\mathcal{E} \to \mathcal{E}' such that the following commutes: and such that F 1F_1 preserve cartesian morphisms.

Symbolically, preserving cartesian morphisms means that for each E:E:\mathcal{E} and f:Bp(E)f:B \to p(E) morphism in the base, we have F 0(f) *EF 1(f *E)F_0(f)^*E \cong F_1(f^*E), where () *(-)^* denotes reindexing.

Remark

When F 0F_0 is the identity we recover the notion of morphism between fibrations over the same base (which are the 1-cells in Fib()\mathbf{Fib}(\mathcal{B})). In that case, F 1F_1 induces a family of functors between fibers over the same object in the base.

For cloven fibrations

If pp and pp' are assumed to be cloven fibrations, then a (cloven) fibred functor between them is assumed to preserve the cleavage, i.e. the choice of cartesian lifts.

Properties

The total category of a fibration supports a factorization system whose left class is comprised of vertical maps (those projecting to an isomorphism) and whose right class are cartesian maps. Fibred functors, by definition, only support the latter, because vertical maps are supported by square of functors in general:

Proposition

Consider a commutative square of functors: Then F 1F_1 sends pp-vertical maps to pp'-vertical maps.

Proof

Let φ:DE\varphi:D \to E be a vertical map in \mathcal{E}, meaning p(φ)=1 Bp(\varphi) = 1_{B}, where B=p(D)=p(E)B=p(D)=p(E). Then F 1(φ):F 1(D)F 1(E)F_1(\varphi) : F_1(D) \to F_1(E) is a 1-cell over p(F 1φ)=F 0(p(φ))=1 F 0Bp'(F_1\varphi) = F_0(p(\varphi)) = 1_{F_0B}.

Thus fibred functors preserve the vertical-cartesian factorization of maps.

See also

Last revised on October 18, 2023 at 19:04:52. See the history of this page for a list of all contributions to it.