11.5 Compactness of the interval
We already pointed out that our constructions of reals are entirely compatible with classical logic. Thus, by assuming the law of excluded middle (LABEL:eq:lem) and the axiom of choice (LABEL:eq:ac) we could develop classical analysis, which would essentially amount to copying any standard book on analysis.
Nevertheless, anyone interested in computation, for example a numerical analyst, ought to be curious about developing analysis in a computationally meaningful setting. That analysis in a constructive setting is even possible was demonstrated by [Bishop1967]. As a sample of the differences and similarities between classical and constructive analysis we shall briefly discuss just one topic—compactness of the closed interval and a couple of theorems surrounding the concept.
Compactness is no exception to the common phenomenon in constructive mathematics that classically equivalent notions bifurcate. The three most frequently used notions of compactness are:
Heine-Borel compact: “every open cover has a finite subcover”.
These are all equivalent in classical mathematics. Let us see how they fare in homotopy type theory. We can use either the Dedekind or the Cauchy reals, so we shall denote the reals just as . We first recall several basic definitions.
A metric space is a set with a map satisfying, for all ,
A Cauchy approximation in is a sequence satisfying
The limit of a Cauchy approximation is a point satisfying
A complete metric space is one in which every Cauchy approximation has a limit.
In words, this is a finite sequence of points such that every point in merely is within of some .
A metric space is totally bounded when it has -nets of all sizes:
In the definition of total boundedness we used sloppy notation . Formally, we should have written instead, where is the inductive type of finite lists from \autorefsec:bool-nat. However, that would make the rest of the statement a bit more cumbersome to express.
Note that in the definition of total boundedness we require pure existence of an -net, not mere existence. This way we obtain a function which assigns to each a specific -net. Such a function might be called a “modulus of total boundedness”. In general, when porting classical metric notions to homotopy type theory, we should use propositional truncation sparingly, typically so that we avoid asking for a non-constant map from to or . For instance, here is the “correct” definition of uniform continuity.
A map on a metric space is uniformly continuous when
In particular, a uniformly continuous map has a modulus of uniform continuity, which is a function that assigns to each a corresponding .
Let us show that is compact in the first sense.
The closed interval is complete and totally bounded.
Given , there is such that , so we may take the -net for . This is an -net because, for every there merely exists such that and , and so .
For completeness of , consider a Cauchy approximation and let be its limit in . Since and are Lipschitz maps, the retraction defined by commutes with limits of Cauchy approximations, therefore
which means that , as required. ∎
We thus have at least one good notion of compactness in homotopy type theory. Unfortunately, it is limited to metric spaces because total boundedness is a metric notion. We shall consider the other two notions shortly, but first we prove that a uniformly continuous map on a totally bounded space has a supremum, i.e. an upper bound which is less than or equal to all other upper bounds.
A uniformly continuous map on a totally bounded metric space has a supremum . For every there exists such that .
Let be the modulus of uniform continuity of . We define an approximation as follows: for any total boundedness of gives a -net . Define
We claim that is a Cauchy approximation. Consider any , so that
for some -net and -net . Every is merely -close to some , therefore , from which we may conclude that
therefore . Symmetrically we obtain , therefore .
We claim that is the supremum of . To prove that for all it suffices to show . So suppose to the contrary that . There is such that . But now merely for some participating in the definition of we get , therefore , a contradiction.
Now, if in \autorefctb-uniformly-continuous-sup we also knew that were complete, we could hope to weaken the assumption of uniform continuity to continuity, and strengthen the conclusion to existence of a point at which the supremum is attained. The usual proofs of these improvements rely on the facts that in a complete totally bounded space
continuity implies uniform continuity, and
every sequence has a convergent subsequence.
The first statement follows easily from Heine-Borel compactness, and the second is just Bolzano–Weierstraß compactness. Unfortunately, these are both somewhat problematic. Let us first show that Bolzano–Weierstraß compactness implies an instance of excluded middle known as the limited principle of omniscience: for every ,
Computationally speaking, we would not expect this principle to hold, because it asks us to decide whether infinitely many values of a function are .
Bolzano–Weierstraß compactness of implies the limited principle of omniscience.
While we might not mourn Bolzano–Weierstraß compactness too much, it seems harder to live without Heine–Borel compactness, as attested by the fact that both classical mathematics and Brouwer’s Intuitionism accepted it. As we do not want to wade too deeply into general topology, we shall work with basic open sets. In the case of these are the open intervals with rational endpoints. A family of such intervals, indexed by a type , would be a map
with the idea that a pair of rationals with determines the type . It is slightly more convenient to allow degenerate intervals as well, so we take a family of basic intervals to be a map
To be quite precise, a family is a dependent pair , not just . A finite family of basic intervals is one indexed by for some . We usually present it by a finite list . Finally, a finite subfamily of is given by a list of indices which then determine the finite family .
As long as we are aware of the distinction between a pair and the corresponding interval , we may safely use the same notation for both. Intersections and inclusions of intervals are expressible in terms of their endpoints:
We say that (pointwise) covers when
The Heine-Borel compactness for states that every covering family of merely has a finite subfamily which still covers .
If excluded middle holds then is Heine-Borel compact.
Assume for the purpose of reaching a contradiction that a family covers but no finite subfamily does. We construct a sequence of closed intervals which are nested, their sizes shrink to , and none of them is covered by a finite subfamily of .
We set . Assuming has been constructed, let and . Both and are covered by , but they cannot both have a finite subcover, or else so would . Either has a finite subcover or it does not. If it does we set , otherwise we set .
The sequences and are both Cauchy and they converge to a point which is contained in every . There merely exists such that . Because the sizes of the intervals shrink to zero, there is such that , but this means that is covered by a single interval , while at the same time it has no finite subcover. A contradiction. ∎
Without excluded middle, or a pinch of Brouwerian Intuitionism, we seem to be stuck. Nevertheless, Heine-Borel compactness of can be recovered in a constructive setting, in a fashion that is still compatible with classical mathematics! For this to be done, we need to revisit the notion of cover. The trouble with (11.5.10) is that the truncated existential allows a space to be covered in any haphazard way, and so computationally speaking, we stand no chance of merely extracting a finite subcover. By removing the truncation we get
which might help, were it not too demanding of covers. With this definition we could not even show that and cover because that would amount to exhibiting a non-constant map , see \autorefex:reals-non-constant-into-Z. Here we can take a lesson from “pointfree topology” (i.e. locale theory): the notion of cover ought to be expressed in terms of open sets, without reference to points. Such a “holistic” view of space will then allow us to analyze the notion of cover, and we shall be able to recover Heine-Borel compactness. Locale theory uses power sets, which we could obtain by assuming propositional resizing; but instead we can steal ideas from the predicative cousin of locale theory, which is called “formal topology”.
Suppose that we have a family and an interval . How might we express the fact that is covered by the family, without referring to points? Here is one: if equals some then it is covered by the family. And another one: if is covered by some other family , and in turn each is covered by , then is covered . Notice that we are listing rules which can be used to deduce that covers . We should find sufficiently good rules and turn them into an inductive definition.
The definition should be read as a higher-inductive type in which the listed rules are point constructors, and the type is -truncated. The first four clauses are of a general nature and should be intuitively clear. The last two clauses are specific to the real line: one says that an interval may be covered by two intervals if they overlap, while the other one says that an interval may be covered from within. Incidentally, if then is covered by the empty family by the last clause.
Inductive covers enjoy the Heine-Borel property, the proof of which requires a lemma.
Suppose and . Then there merely exists a finite subfamily of which inductively covers .
We prove the statement by induction on . There are six cases:
Reflexivity: if then by monotonicity is covered by the finite subfamily .
Transitivity: suppose and . By the inductive hypothesis there merely exists which covers . Again by the inductive hypothesis, each of is covered by a finite subfamily of , and we can collect these into a finite subfamily which covers .
Monotonicity: if and then we may apply the inductive hypothesis to because .
Localization: suppose and . Because , by the inductive hypothesis there is a finite subcover of . We also know that , therefore is covered by , which is a finite subfamily of .
If for some then by monotonicity .
Finally, by reflexivity. ∎
Say that inductively covers when there merely exists such that .
A closed interval is Heine-Borel compact for inductive covers.
Suppose is inductively covered by , so there merely is such that . By \autorefreals-formal-topology-locally-compact there is a finite subcover of , which is therefore a finite subcover of . ∎
Experience from formal topology shows that the rules for inductive covers are sufficient for a constructive development of pointfree topology. But we can also provide our own evidence that they are a reasonable notion.
An inductive cover is also a pointwise cover.
Assuming excluded middle, a pointwise cover is also an inductive cover.
Consider a family of basic intervals , where we write , an interval inductively covered by , and such that . We prove by induction on that there merely exists such that . Most cases are pretty obvious, so we show just two. If by reflexivity, then there merely is some such that and so . If by transitivity via then by the inductive hypothesis there merely is such that , and then since again by the inductive hypothesis there merely exists such that . Other cases are just as exciting.
Suppose pointwise covers . By \autorefdefn:inductive-cover-interval-2 of \autorefdefn:inductive-cover it suffices to show that inductively covers whenever , so consider such and . By \autorefclassical-Heine-Borel there is a finite subfamily which already pointwise covers , and hence . Let be a Lebesgue number for as in \autorefex:finite-cover-lebesgue-number. There is a positive such that . For let
The intervals , , …, inductively cover by repeated use of transitivity and \autorefdefn:inductive-cover-interval-1 in \autorefdefn:inductive-cover. Because their widths are below each of them is contained in some , and we may use transitivity and monotonicity to conclude that inductively cover . ∎
The upshot of the previous theorem is that, as far as classical mathematics is concerned, there is no difference between a pointwise and an inductive cover. In particular, since it is consistent to assume excluded middle in homotopy type theory, we cannot exhibit an inductive cover which fails to be a pointwise cover. Or to put it in a different way, the difference between pointwise and inductive covers is not what they cover but in the proofs that they cover.
We could write another book by going on like this, but let us stop here and hope that we have provided ample justification for the claim that analysis can be developed in homotopy type theory. The curious reader should consult \autorefex:mean-value-theorem for constructive versions of the mean value theorem.
|Title||11.5 Compactness of the interval|