nLab split essentially surjective functor

Idea

When working with strict categories 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.

Definition

Definition

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

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

indexed by objects $y \in D$.

Examples

• A functor is an equivalence of categories if and only if it is fully faithful and split essentially surjective, without any use of the axiom of choice.

Properties

• Every split essentially surjective functor is essentially surjective.

• That every essentially surjective functor is split essentially surjective is equivalent to the axiom of choice.

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:

Definition

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

$$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:

Definition

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

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

for all objects $y: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 $G$ be a nontrivial group and $BG$ the corresponding connected univalent groupoid, and $\ast$ the terminal category; then the functor $\ast \to BG$ is essentially surjective, but not split essentially surjective.

Related concepts

• axiom of choice

basic properties of…

• functors

  • faithful functor

  • full functor

  • full and faithful functor

  • injective-on-objects functor

  • essentially injective functor

  • essentially surjective functor

    • surjective-on-objects functor

    • bijective-on-objects functor

    • dominant functor

  • split essentially surjective functor

  • essentially surjective and full functor

  • equivalence of categories

  • conservative functor

  • pseudomonic functor

  • (co)continuous functor

  • final functor

• 2-functors

  • full and faithful 2-functor

  • locally fully faithful 2-functor

  • equivalence of 2-categories

• (∞,1)-functors:

  • fully faithful (∞,1)-functor

  • essentially surjective (∞,1)-functor

  • equivalence of (∞,1)-categories

  • homotopy final functor, final (∞,1)-functor

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)