10.2 Cardinal numbers
As usual for truncations, if is a set, then denotes its image under the canonical projection ; we call the cardinality of . By definition, is a set. It also inherits the structure of a semiring from \set.
Since is a set, to define for all , by induction it suffices to assume that is for some . Now we want to define , i.e. we want to define for all . However, since is a set, by induction it suffices to assume that is for some . But now we can define to be . ∎
Similarly, the operation of cardinal multiplication
is defined by induction on truncation:
is a commutative semiring, i.e. for we have the following.
where and .
We prove the commutativity of multiplication, ; the others are exactly analogous. Since is a set, the type is a mere proposition, and in particular a set. Thus, by induction it suffices to assume and are of the form and respectively, for some . Now and , so it suffices to show . Finally, by univalence, it suffices to give an equivalence . But this is easy: take and its obvious inverse. ∎
The operation of cardinal exponentiation is also defined by induction on truncation:
For we have
Exactly like \autorefcard:semiring. ∎
Cardinal inequality is a preorder, i.e. for we have
As before, by induction on truncation. For instance, since is a mere proposition, by induction on 0-truncation we may assume , , and are , , and respectively. Now since is a mere proposition, by induction on -truncation we may assume given injections and . But then is an injection from to , so holds. Reflexivity is even easier. ∎
We may likewise show that cardinal inequality is compatible with the semiring operations.
If is an injection, define at as follows. Since is injective, the fiber of at is a mere proposition. Therefore, by excluded middle, either there is an with , or not. In the first case, define ; otherwise set . Then for any , we have , so is surjective.
The second statement follows from this by induction on truncation. For the third, if is surjective, then by the axiom of choice, there merely exists a function with for all . But then must be injective. ∎
Theorem 10.2.10 (Schroeder–Bernstein).
Assuming excluded middle, for sets and we have
Assuming excluded middle, cardinal inequality is a partial order, i.e. for we have
Since is a mere proposition, by induction on truncation we may assume and are and , respectively, and that we have injections and . But then the Schroeder–Bernstein theorem gives an isomorphism , hence an equality . ∎
Finally, we can reproduce Cantor’s theorem, showing that for every cardinal there is a greater one.
Theorem 10.2.12 (Cantor).
For , there is no surjection .
Suppose is any function, and define by . If , then but , a contradiction. Thus, is not surjective. ∎
Assuming excluded middle, for any , there is a cardinal such that and .
Let . Now we want to show a mere proposition, so by induction we may assume is , so that . Using excluded middle, we have a function defined by
And if , then , so ; hence is injective. Thus, .
On the other hand, if , then we would have an injection . By \autorefthm:injsurj, since we have and excluded middle, there would then be a surjection , contradicting Cantor’s theorem. ∎
|Title||10.2 Cardinal numbers|