A proof about skeletons without axiom of choice

Question

I'm trying to prove this statement and I found two different proofs: the first seems to work without explicit use of AC while the second uses it precisely where I expected it.

(T) Let $i$ be a cardinality-like function on $\mathcal C$ then $\mathcal K(i;\mathcal C)$ is a skeleton of $\mathcal C$.

---

Let's begin by explaining my notation and my definitions (where terminology is bad it is because I'm not aware of the standard one). Every category in the following is assumed to be a $\mathcal U$-category where $\mathcal U$ is a Grothendieck Universe and I assume as many of them as needed.

Def 0. $\mathcal C=(\mathcal C_0,\mathcal C_1)$ is a $\mathcal U$-category iff:

1. it is locally $\mathcal U$-small;
2. $\mathcal C_0$ is a set (not necessarily an $\mathcal U$-set).

It follows that arrows form a set, not necessarily a small set.

Def 1. (cardinality-like): I'll call a function $i:\mathcal C_0\to\mathcal C_0$ cardinality-like function over $\mathcal C$ iff:

1. $X\simeq Y$ iff $iX=iY$;
2. $i^2=i$ (it is idempotent).

Note 1. that under 1) being idempotent is equivalent to $\forall X:X\simeq iX$. Also note that the image of $i$ coincides with $i$'s fixed points.

Def 2. Given a cardinality-like function over $\mathcal C$ define the full subcategory $\mathcal K(i;\mathcal C)$

1. $\mathcal K(i;\mathcal C)_0:={\rm im}(i)\subseteq \mathcal C_0$
2. Let $\kappa,\lambda \in {\rm im}(i)$ define ${\rm Hom}_{\mathcal K(i;\mathcal C)}(\kappa,\lambda):={\rm Hom}_{\mathcal C}(\kappa,\lambda)$.

Def 3. $\mathcal C$ is skeletal iff: for objects $X\simeq Y\Leftrightarrow X=Y$.

Note 2. that by definition $\mathcal K(i;\mathcal C)$ is skeletal.

Def 4. A full subcategory $\mathcal S\hookrightarrow \mathcal C$ is a skeleton for $\mathcal C$ iff:

1. $\mathcal S$ is skeletal;
2. the canonical inclusion functor ${\rm In}:\mathcal S\hookrightarrow \mathcal C$ is essentially surjective.

---

Now the proof-verification part. Reading The Joy of Cats I understand that under the assumption that an inclusion $F$ is full: "essential surjectivity of $F$" is equivalent to "$F$ being an equivalence. That means that to show that ${\rm In}:\mathcal K(i;\mathcal C)\hookrightarrow \mathcal C$ is a skeleton it should be enough to show the essential surjectivity.

(T) Let $i$ be a cardinality-like function on $\mathcal C$ then $\mathcal K:=\mathcal K(i;\mathcal C)$ is a skeleton of $\mathcal C$.

proof 1. $\mathcal K$ is full by definition. $\mathcal K$ is skeletal: given objects $\kappa,\lambda\in \mathcal K_0$ if $\kappa\simeq \lambda$ then by def. 2 $i\kappa= i\lambda$. Objects of $\mathcal K$ are $i$-fixed points thus $\kappa=\lambda$. Given a $X\in\mathcal C_0$ just set $\kappa:=iX\in\mathcal K_0$: we have ${\rm In}(\kappa)={\rm In}(iX)=iX$ so by note 1 ${\rm In}(\kappa)\simeq X$, i.e.${\rm In}$ is essentially surjective. $\square$

On the other hand, if I try to prove this by building an inverse functor of ${\rm In}$ that makes it an equivalence I have to use axiom of choice, using the $\mathcal U$-category condition, to define a family of bijections $\beta_X:X\to iX$, use that family to define an inverse functor $F$ and then I have to use $\beta$ to define the unit and co-unit of the equivalence.

prof 2. (sketch) Consider the $\mathcal C_0$-family of $\mathcal U$-sets ${\rm Hom}_{\mathcal C}(X,iX)$. They are all non-empty by note 1. Since $\mathcal C$ is $\mathcal U$-category the union of the family is a set. Assuming choice, exists at least a choice function $\beta:\mathcal C_0\to \bigcup_{X\in\mathcal C_0}{\rm Hom}_{\mathcal C}(X,iX)$ takin values on the isos (by note 1). Define the functor $F:\mathcal C\to \mathcal K$ to be $F(X)=iX$ on objects and to be $$F(f):=\beta_Yf\beta_X^{-1}$$ on arrows. I can prove it is functorial. Set $\eta_X:=\beta_{{\rm In}(X)}$, i.e. the restriction on the subcategory. The proof is concluded by showing that $\beta^{-1}:{\rm In}\circ F\Rightarrow {\bf 1}_{\mathcal C}$ and $\eta:{\bf 1}_{\mathcal K}\Rightarrow F\circ {\rm In}$ are natural.

$\mathcal Q$ In prof 1 am I really avoiding the axiom of choice?

On request I can post the full prof 2.

Answer 1

As hinted by @AsafKaragila the assumption of choices lies in the assumption of existence of a cardinal-like function. It is in fact equivalent to it, I claim.

---

More generally, let $X$ be a set and $E\subseteq X\times X$ an equivalence relation.

Definition. A function $f:X\to X$ is called $E$-like function ove $X$ iff

1. $\forall x,y\in X.\,xEy\Leftrightarrow f(x)=f(y)$
2. $f^2=f$

Define the following statements

(E-Axiom) For every equivalence relation $E$ over $X$ exists an $E$-like function over $X$.

(AC${^\sigma}$) Every surjection has a section.

---

Lemma 1. Every equivalence relation $E$ over $X$ defines a surjection $\pi:X\to X/E$ where $X/E:=\{C\in\mathcal P(X)\,|\,\exists x\in X.C=\pi(x)\}$ with the property that $$\forall x,y\in X.\,xEy\Leftrightarrow \pi(x)=\pi(y)$$

Proof. Define $\pi(x):=\{y\in X\,|\,yEx\}$. $\pi$ is surjective by definition. ($\Leftarrow$) By reflexivity $x\in\pi(x)=\pi(y)$ thus $xEy$. ($\Rightarrow$) if $xEy$ then for every $z$ s.t. $zEx$ by transitivity $zEy$ and vice-versa. $\square$

Lemma 2. if $f$ is $E$-like over $X$ then ${\rm ker }f=E$.

Proof. By $E$-likeness $xEy\Leftrightarrow f(x)=f(y)$. By definition of kernel $(x,y)\in {\rm ker }f :\Leftrightarrow f(x)=f(y)$. $\square$

Theorem. The E-axiom is equivalent to AC${^\sigma}$.

Proof. ($\Leftarrow$) Let $E$ be an equivalence rel. over $X$ consider the surjection $\pi:X\to X/E$ of lemma 1. By AC${^\sigma}$ exists a $\sigma:X/E \to X$ such that $\pi\sigma={\rm id}_{X/E}$. Define $f:=\sigma\pi:X\to X$. $f$ is $E$-like over $X$:

• By lemma 1 and injectivity of the section $\sigma\pi(x)=\sigma\pi(y)\Leftrightarrow \pi(x)=\pi(y) \Leftrightarrow xEy$;
• $\sigma\pi\sigma\pi=\sigma\pi$.

($\Rightarrow$) Take a surjective function $\phi:X\to Y$. Every function $\phi:X\to Y$ defines a equivalence relation ${\rm ker}\phi$ over $X$. By E-axiom exists $f:X\to X$ that is ${\rm ker}\phi$-like over $X$. By lemma 2 ${\rm ker}\phi={\rm ker}f$ so set $K:=X/{\rm ker}\phi=X/{\rm ker}f$. We get the following injective-surjective factorizations:

1. $X\overset{f}{\to}X=X\overset{\pi}{\to}K\overset{\overline{f}}{\to} X$, i.e. $f=\overline{f}\pi$;
2. $X\overset{\phi}{\to}Y=X\overset{\pi}{\to}K\overset{\overline{\phi}}{\to} Y$, i.e. $\phi=\overline{\phi}\pi$ where $\overline{\phi}$ is bijective.

Define $\sigma:=\overline{f}(\overline{\phi}^{-1}):Y\to X$. $\sigma$ is a section of $\phi$: we have $\sigma\phi=\overline{f}(\overline{\phi}^{-1})\overline{\phi}\pi=\overline{f}\pi=f$. The function $f$ is idempotent ($*$), $\phi$ is surjective ($**$) and $\sigma$ is injective ($***$) because is a composition of two injectives

$(\sigma\phi)(\sigma\phi) =\sigma\phi \quad (*)\\ \sigma(\phi\sigma)\phi =\sigma\phi \\ \sigma\phi\sigma =\sigma \quad (**)\\ \phi\sigma = {\rm id}_Y \quad (***)\\$

$\square$

---

I hope this is what @AsafKaragila was trying to say with his, way too cryptic, hints.