4.6 Surjections and embeddings
When and are sets and 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.
We say is surjective (or a surjection) if for every we have .
We say is a embedding if for every the function is an equivalence.
In other words, is surjective if every fiber of is merely inhabited, or equivalently if for all there merely exists an such that . In traditional logical notation, is surjective if . This must be distinguished from the stronger assertion that ; if this holds we say that is a split surjection.
If and are sets, then by Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2), is an embedding just when
In this case we say that 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.
A function is an equivalence if and only if it is both surjective and an embedding.
If is an equivalence, then each is contractible, hence so is , so is surjective. And we showed in Theorem 2.11.1 (http://planetmath.org/211identitytype#Thmprethm1) that any equivalence is an embedding.
Conversely, suppose is a surjective embedding. Let ; we show that is contractible. Since is surjective, there merely exists an such that . Thus, the fiber of over is inhabited; it remains to show it is a mere proposition. For this, suppose given with and . Then since is an equivalence, there exists with . However, using the characterization of paths in -types, the latter equality rearranges to . Thus, together with it exhibits in the fiber of over . ∎
For any we have
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|