TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A functor is an equivalence exactly when it is fully faithful and split essentially surjective, without Choice

Statement

A functor $F : C \to D$ is an equivalence exactly when it is fully faithful and split essentially surjective. No choice principle is needed because the splitting is part of the data.

Facts & Assumptions

Given: A functor $F : C \to D$ .

[L1]

Equivalence and quasi-inverse data are defined in Equivalence, quasi-inverse, and adjoint equivalence of categories.

[L2]

Fully faithful and split essentially surjective have the precise hom-bijection and specified-witness meanings in Faithful, full, fully faithful, essentially surjective, and split essentially surjective functors.

[L3]

A fully faithful functor reflects isomorphisms (Every fully faithful functor reflects isomorphisms).

Proof

technique · direct

1.1

Suppose first that $F$ has quasi-inverse $G$ , unit $η : 1_{C} \Rightarrow G F$ , and counit $ε : F G \Rightarrow 1_{D}$ . Then $D \mapsto (G D, ε_{D})$ explicitly splits essential surjectivity.

givenL1L2

1.2

Conversely, assume $F$ is fully faithful and comes with objects $C_{D}$ and isomorphisms $ε_{D} : F C_{D} \to D$ . Define $G D = C_{D}$ , and for $u : D \to E$ define $G (u)$ as the unique morphism whose image under $F$ is $ε_{E}^{- 1} u ε_{D}$ ; fullness gives existence and faithfulness gives uniqueness.

givenL2

2.1

Naturality and invertibility of $η$ show faithfulness: if $F f = F g$ , then $G F f = G F g$ , so $η_{B} f = G F f η_{A} = G F g η_{A} = η_{B} g$ and $f = g$ .

step 1.1L1

2.2

The defining equation makes $G (1_{D}) = 1_{G D}$ and $G (v u) = G (v) G (u)$ after applying faithful $F$ , so $G$ is a functor, and the same equation is precisely naturality of $ε : F G \Rightarrow 1_{D}$ .

step 1.2L2

3.1

Put $δ_{A} = ε_{F A} \circ F (η_{A})$ , an automorphism of $F A$ . For $u : F A \to F B$ , set $v = δ_{B} u δ_{A}^{- 1}$ and $h = η_{B}^{- 1} G (v) η_{A}$ ; naturality of $ε$ gives $F h = δ_{B}^{- 1} v δ_{A} = u$ , so $F$ is full.

step 1.1step 2.1L1L2

3.2

For each $A$ , fullness gives a unique $η_{A} : A \to G F A$ with $F (η_{A}) = ε_{F A}^{- 1}$ ; faithfulness and naturality of $ε$ make $η$ natural, and [L3] makes each $η_{A}$ an isomorphism because its image is.

step 2.2L2L3

4.1

Thus $(F, G, η, ε)$ is equivalence data. The two constructions prove both directions without making any unrecorded selection.

step 1.1step 2.1step 3.1step 3.2L1∎

Depends on

Used by

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, Chapter 1 (standard reference, not scraped)
Ahrens, Kapulkin and Shulman, Univalent categories and the Rezk completion, section 6 (standard reference, not scraped)