4.6 Surjections and embeddings

When $A$ and $B$ are sets and $f:A\to B$ is an equivalence, we also call it as isomorphism or a bijection. (We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of “sameness” than homotopy equivalence.) In set theory, a function is a bijection just when it is both injective and surjective. The same is true in type theory, if we formulate these conditions appropriately. For clarity, when dealing with types that are not sets, we will speak of embeddings instead of injections.

Definition 4.6.1.

Let $f\mathrm{:}A\mathrm{\to }B$.

1. We say $f$ is surjective (or a surjection) if for every $b:B$ we have $\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel$.

2. We say $f$ is a embedding if for every $x,y:A$ the function ${\mathrm{𝖺𝗉}}_f:(x{=}_{A}y)\to (f(x){=}_{B}f(y))$ is an equivalence.

In other words, $f$ is surjective if every fiber of $f$ is merely inhabited, or equivalently if for all $b:B$ there merely exists an $a:A$ such that $f(a)=b$. In traditional logical notation, $f$ is surjective if $\forall (b:B).\exists (a:A).(f(a)=b)$. This must be distinguished from the stronger assertion that ${\prod }_{(b:B)}{\sum }_{(a:A)}(f(a)=b)$; if this holds we say that $f$ is a split surjection.

If $A$ and $B$ are sets, then by Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2), $f$ is an embedding just when

$$\prod _{x,y:A}(f(x){=}_{B}f(y))\to (x{=}_{A}y).$$ (4.6.2)

In this case we say that $f$ is injective, or an injection. We avoid these word for types that are not sets, because they might be interpreted as (4.6.2), which is an ill-behaved notion for non-sets. It is also true that any function between sets is surjective if and only if it is an epimorphism in a suitable sense, but this also fails for more general types, and surjectivity is generally the more important notion.

Theorem 4.6.3.

A function $f\mathrm{:}A\mathrm{\to }B$ is an equivalence if and only if it is both surjective and an embedding.

Proof.

If $f$ is an equivalence, then each ${\mathrm{𝖿𝗂𝖻}}_f(b)$ is contractible, hence so is $\parallel {\mathrm{𝖿𝗂𝖻}}_f(b)\parallel$, so $f$ is surjective. And we showed in Theorem 2.11.1 (http://planetmath.org/211identitytype#Thmprethm1) that any equivalence is an embedding.

Conversely, suppose $f$ is a surjective embedding. Let $b:B$; we show that ${\sum }_{(x:A)}(f(x)=b)$ is contractible. Since $f$ is surjective, there merely exists an $a:A$ such that $f(a)=b$. Thus, the fiber of $f$ over $b$ is inhabited; it remains to show it is a mere proposition. For this, suppose given $x,y:A$ with $p:f(x)=b$ and $q:f(y)=b$. Then since ${\mathrm{𝖺𝗉}}_f$ is an equivalence, there exists $r:x=y$ with ${\mathrm{𝖺𝗉}}_f(r)=p{q}^{-1}$. However, using the characterization of paths in $\mathrm{\Sigma }$-types, the latter equality rearranges to $r_{*}\left(p\right)=q$. Thus, together with $r$ it exhibits $(x,p)=(y,q)$ in the fiber of $f$ over $b$. ∎

Corollary 4.6.4.

For any $f\mathrm{:}A\mathrm{\to }B$ we have

$$\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)\simeq (\mathrm{𝗂𝗌𝖤𝗆𝖻𝖾𝖽𝖽𝗂𝗇𝗀}(f)\times \mathrm{𝗂𝗌𝖲𝗎𝗋𝗃𝖾𝖼𝗍𝗂𝗏𝖾}(f)).$$

Proof.

Being a surjection and an embedding are both mere propositions; now apply Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2). ∎

Of course, this cannot be used as a definition of “equivalence”, since the definition of embeddings refers to equivalences. However, this characterization can still be useful; see §8.8 (http://planetmath.org/88whiteheadstheoremandwhiteheadsprinciple). We will generalize it in http://planetmath.org/node/87580Chapter 7.

Title	4.6 Surjections and embeddings