10.2 Cardinal numbers
Definition 10.2.1.
The type of cardinal numbers
is the 0-truncation of the type \setof sets:
Thus, a cardinal number, or cardinal, is an inhabitant of .
Technically, of course, there is a separate type associated to each universe .
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.
Definition 10.2.2.
Proof.
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 . β
Definition 10.2.3.
Lemma 10.2.4.
Proof.
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.
β
Definition 10.2.5.
The operation of cardinal exponentiation is also defined by induction on truncation:
Lemma 10.2.6.
For we have
Proof.
Exactly like \autorefcard:semiring. β
Definition 10.2.7.
The relation of cardinal inequality
is defined by induction on truncation:
where is the type of injections from to . In other words, means that there merely exists an injection from to .
Lemma 10.2.8.
Cardinal inequality is a preorder, i.e.Β for we have
Proof.
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.
Lemma 10.2.9.
Consider the following statements:
-
1.
There is an injection .
-
2.
There is a surjection .
Then, assuming excluded middle:
- β’
- β’
-
β’
Assuming the axiom of choice
, we haveΒ 2 merely 1.
Proof.
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
Proof.
The usual βback-and-forthβ argument applies without significant changes.
Note that it actually constructs an isomorphism (assuming excluded middle so that we can decide whether a given element belongs to a cycle, an infinite chain, a chain beginning in , or a chain beginning in ).
β
Corollary 10.2.11.
Assuming excluded middle, cardinal inequality is a partial order, i.e.Β for we have
Proof.
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 .
Proof.
Suppose is any function, and define by .
If , then but , a contradiction.
Thus, is not surjective.
β
Corollary 10.2.13.
Assuming excluded middle, for any , there is a cardinal such that and .
Proof.
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 |
---|---|
\metatable |