nLab split essentially surjective functor

Split essentially surjective functors

Split essentially surjective functors


In foundations without the axiom of choice, it is not true that every fully faithful and essentially surjective functor is an equivalence of categories, since the mere property of being isomorphic to some object in the image is not enough to get a specific such object and isomorphism without the axiom of choice. However, it is true if instead one uses split essentially surjective functors, where the isomorphisms are structure rather than mere property.



A functor F:CDF : C \to D is split essentially surjective if there is a specified family

{(xC,p y:F(x)y)} yD \Big\{ (x\in C, p_y : F(x) \cong y) \Big\}_{y\in D}

indexed by objects yDy \in D.



In homotopy type theory

In homotopy type theory (or, indeed, any dependent type theory), the definition above can be phrased for general precategories in type theoretic language:


A functor F:CDF : C \to D is split essentially surjective if there is a specified dependent function

p: y:D x:C(F(x)y).p: \prod_{y:D} \sum_{x:C} (F(x) \cong y).

This differs from the definition of an essentially surjective functor by the lack of propositional truncations in the definition:


A functor F:CDF : C \to D is essentially surjective if the there is a dependent term

p(y): x:C(F(x)y)p(y) \colon \left\Vert \sum_{x:C} (F(x) \cong y)\right\Vert

for all objects y:Dy:D.

However, for precategories, and even for univalent categories, the axiom of choice is insufficient to ensure that every essentially surjective functor is split essentially surjective. For instance, let GG be a nontrivial group and BGBG the corresponding connected univalent groupoid, and *\ast the terminal category; then the functor *BG\ast \to BG is essentially surjective, but not split essentially surjective.

basic properties of…


Last revised on September 3, 2022 at 18:23:04. See the history of this page for a list of all contributions to it.