From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
From mathcomp Require Import finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
Require Import reals signed topology.
From HB Require Import structures.
# The Cantor Space and Applications
This file develops the theory of the Cantor space, that is bool^nat with
the product topology. The two main theorems proved here are
homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff.
```
cantor_space == the Cantor space, with its canonical metric
cantor_like T == perfect + compact + hausdroff + zero dimensional
pointed_discrete T == equips T with the discrete topology
tree_of T == builds a topological tree with levels (T n)
```
The overall goal of the next few sections is to prove that
Every compact metric space `T` is the image of the Cantor space.
The overall proof will build two continuous functions
Cantor space -> a bespoke tree for `T` -> `T`
The proof is in 4 parts:
- Part 1: Some generic machinery about continuous functions from trees.
- Part 2: All cantor-like spaces are homeomorphic to the Cantor space.
(an application of part 1)
- Part 3: Finitely branching trees are Cantor-like.
- Part 4: Every compact metric space has a finitely branching tree with
a continuous surjection. (a second application of part 1)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Definition
cantor_space
:=
product_uniformType (
fun _ : nat => @discrete_uniformType _ discrete_bool).
Definition
cantor_like
(
T
: topologicalType)
:=
[/\ perfect_set [set: T],
compact [set: T],
hausdorff_space T &
zero_dimensional T].
Lemma
cantor_space_compact
: compact [set: cantor_space].
Proof.
Lemma
cantor_space_hausdorff
: hausdorff_space cantor_space.
Proof.
Lemma
cantor_zero_dimensional
: zero_dimensional cantor_space.
Proof.
Lemma
cantor_perfect
: perfect_set [set: cantor_space].
Proof.
Lemma
cantor_like_cantor_space
: cantor_like cantor_space.
Proof.
## Part 1
A tree here has countable levels, and nodes of type `K n` on the nth
level.
Each level is in the 'discrete' topology, so the nodes are independent.
The goal is to build a map from branches to X.
1. Each level of the tree corresponds to an approximation of `X`.
2. Each level refines the previous approximation.
3. Then each branch has a corresponding Cauchy filter.
4. The overall function from branches to X is a continuous surjection.
5. With an extra disjointness condition, this is also an injection
Section
topological_trees
.
Context {K : nat -> topologicalType} {X : topologicalType}
(
refine_apx
: forall
n,
set X -> K n -> set X)
(
tree_invariant
: set X -> Prop).
Hypothesis
cmptX
: compact [set: X].
Hypothesis
hsdfX
: hausdorff_space X.
Hypothesis
discreteK
: forall
n,
discrete_space (
K n).
Hypothesis
refine_cover
: forall
n
U,
U = \bigcup_e @refine_apx n U e.
Hypothesis
refine_invar
: forall
n
U
e,
tree_invariant U -> tree_invariant (
@refine_apx n U e).
Hypothesis
invar_n0
: forall
U,
tree_invariant U -> U !=set0.
Hypothesis
invarT
: tree_invariant [set: X].
Hypothesis
invar_cl
: tree_invariant `<=` closed.
Hypothesis
refine_separates:
forall
x
y
: X, x != y ->
exists
n,
forall (
U
: set X)
e,
@refine_apx n U e x -> ~@refine_apx n U e y.
Let
refine_subset
n
U
e
: @refine_apx n U e `<=` U.
Proof.
Let
T
:= product_topologicalType K.
Local Fixpoint
branch_apx
(
b
: T)
n
:=
if n is m.
+1 then refine_apx (
branch_apx b m) (
b m)
else [set: X].
Let
tree_mapF
b
:= filter_from [set: nat] (
branch_apx b).
Let
tree_map_invar
b
n
: tree_invariant (
branch_apx b n).
Proof.
Let
tree_map_sub
b
i
j
: (
i <= j)
%N -> branch_apx b j `<=` branch_apx b i.
Proof.
Instance
tree_map_filter
b
: ProperFilter (
tree_mapF b).
Proof.
Let
tree_map
b
:= lim (
tree_mapF b).
Let
cvg_tree_map
b
: cvg (
tree_mapF b).
Proof.
Local Lemma
tree_map_surj
: set_surj [set: T] [set: X] tree_map.
Proof.
move=> z _; suff : exists
g,
forall
n,
branch_apx g n z.
case=> g gnz; exists g => //; apply: close_eq => // U [oU Uz] V ngV; exists z.
by split => //; have [n _] := @cvg_tree_map g _ ngV; exact.
have zcov' : forall
n
(
U
: set X)
, exists
e,
U z -> @refine_apx n U e z.
move=> n U; have [|?] := pselect (
U z)
; last by exists point.
by rewrite [X in X z -> _](
@refine_cover n U)
; case => e _ ?; exists e.
pose zcov
n
U
:= projT1 (
cid (
zcov' n U)).
pose fix g
n
: K n * set X :=
if n is m.
+1
then (
zcov m.
+1 (
g m).
2, @refine_apx m.
+1 (
g m).
2 (
zcov m.
+1 (
g m).
2))
else (
zcov O [set: X], @refine_apx O [set: X] (
zcov O [set: X])).
pose g'
n
:= (
g n).
1; have apxg n : branch_apx g' n.
+1 = (
g n).
2.
by elim: n => //= n ->.
exists g'; elim => // n /= IH.
have /(
_ IH)
:= projT2 (
cid (
zcov' n (
branch_apx g' n))).
by case: n {IH} => // n; rewrite apxg.
Qed.
Let
tree_prefix
(
b
: T) (
n
: nat)
:
\forall
c
\near b, forall
i,
(
i < n)
%N -> b i = c i.
Proof.
Let
apx_prefix
b
c
n
:
(
forall
i,
(
i < n)
%N -> b i = c i)
-> branch_apx b n = branch_apx c n.
Proof.
elim: n => //= n IH inS; rewrite IH; first by rewrite inS.
by move=> ? ?; exact/inS/ltnW.
Qed.
Let
tree_map_apx
b
n
: branch_apx b n (
tree_map b).
Proof.
Local Lemma
tree_map_cts
: continuous tree_map.
Proof.
move=> b U /cvg_tree_map [n _] /filterS; apply.
exact/fmap_filter/nbhs_filter.
rewrite nbhs_simpl /=; near_simpl; have := tree_prefix b n; apply: filter_app.
by near=> z => /apx_prefix ->; exact: tree_map_apx.
Unshelve.
all: end_near. Qed.
Let
tree_map_setI
x
y
n
: tree_map x = tree_map y ->
refine_apx (
branch_apx x n) (
x n)
`&` refine_apx (
branch_apx y n) (
y n)
!=set0.
Proof.
Local Lemma
tree_map_inj
: (
forall
n
U,
trivIset [set: K n] (
@refine_apx n U))
->
set_inj [set: T] tree_map.
Proof.
Lemma
tree_map_props
: exists
f
: T -> X,
[/\ continuous f,
set_surj [set: T] [set: X] f &
(
forall
n
U,
trivIset [set: K n] (
@refine_apx n U))
->
set_inj [set: T] f].
Proof.
End topological_trees.
## Part 2
We can use `tree_map_props` to build a homeomorphism from the
cantor_space to a Cantor-like space T.
Section
TreeStructure
.
Context {R : realType} {T : pseudoMetricType R}.
Hypothesis
cantorT
: cantor_like T.
Let
dsctT
: zero_dimensional T
Proof.
Let
pftT
: perfect_set [set: T]
Proof.
Let
cmptT
: compact [set: T]
Proof.
Let
hsdfT
: @hausdorff_space T
Proof.
Let
c_invar
(
U
: set T)
:= clopen U /\ U !=set0.
Let
U_
:= unsquash (
clopen_surj cmptT).
Let
split_clopen'
(
U
: set T)
: exists
V,
open U -> U !=set0 -> [/\ clopen V, V `&` U !=set0 & ~`V `&` U !=set0].
Proof.
have [oU|?] := pselect (
open U)
; last by exists point.
have [Un0|?] := pselect (
U !=set0)
; last by exists point.
have [x [y] [Ux] Uy xny] := (
iffLR perfect_set2)
pftT U oU Un0.
have [V [clV Vx Vy]] := dsctT xny; exists V => _ _.
by split => //; [exists x | exists y].
Qed.
Let
split_clopen
(
U
: set T)
:= projT1 (
cid (
split_clopen' U)).
Let
c_ind
n
(
V
: set T) (
b
: bool)
:=
let
Wn
:=
if pselect ((
U_ n)
`&` V !=set0 /\ ~` (
U_ n)
`&` V !=set0)
then U_ n else split_clopen V in
(
if b then Wn else ~` Wn)
`&` V.
Local Lemma
cantor_map
: exists
f
: cantor_space -> T,
[/\ continuous f,
set_surj [set: cantor_space] [set: T] f &
set_inj [set: cantor_space] f ].
Proof.
have [] := @tree_map_props
(
fun=> [topologicalType of bool])
T c_ind c_invar cmptT hsdfT.
- by [].
- move=> n V; rewrite eqEsubset; split => [t Vt|t [? ? []]//].
have [?|?] := pselect (
U_ n `&` V !=set0 /\ ~` U_ n `&` V !=set0).
+ have [Unt|Unt] := pselect (
U_ n t).
* by exists true => //; rewrite /c_ind; case: pselect.
* by exists false => //; rewrite /c_ind; case: pselect.
+ have [scVt|scVt] := pselect (
split_clopen V t).
* by exists true => //; rewrite /c_ind; case: pselect.
* by exists false => //; rewrite /c_ind; case: pselect.
- move=> n U e [] clU Un0; rewrite /c_ind; case: pselect => /=.
+ move=> [UU CUU]; case: e => //; split => //; apply: clopenI => //.
exact: funS.
by apply: clopenC => //; exact: funS.
+ move=> _; have [|//|clscU scUU CscUU] := projT2 (
cid (
split_clopen' U)).
by case: clU.
case: e; split => //; first exact: clopenI.
by apply: clopenI => //; exact: clopenC.
- by move=> ? [].
- by split; [exact: clopenT | exists point].
- by move=> ? [[]].
- move=> x y /dsctT [A [clA Ax Any]].
have [n _ UnA] := @surj _ _ _ _ U_ _ clA; exists n => V e.
have [|+ _] := pselect (
V y)
; last by apply: subsetC => ? [].
have [Vx Vy|? _ []//] := pselect (
V x).
rewrite {1 2}/c_ind; case: pselect => /=; rewrite ?UnA.
by move=> _; case: e; case => // ? ?; apply/not_andP; left.
by apply: absurd; split; [exists x | exists y].
- move=> f [ctsf surjf injf]; exists f; split => //; apply: injf.
by move=> n U i j _ _ [z] [] [] + Uz [+ _]; move: i j => [] [].
Qed.
Let
tree_map
:= projT1 (
cid cantor_map).
Let
tree_map_bij
: bijective tree_map.
Proof.
#[local] HB.instance Definition _ := @BijTT.
Build _ _ _ tree_map_bij.
Lemma
homeomorphism_cantor_like
:
exists
f
: {splitbij [set: cantor_space] >-> [set: T]},
continuous f /\ (
forall
A,
closed A -> closed (
f @` A)).
Proof.
End TreeStructure.
## Part 3: Finitely branching trees are Cantor-like
Section
FinitelyBranchingTrees
.
Context {R : realType}.
Definition
pointed_discrete
(
P
: pointedType)
: pseudoMetricType R :=
@discrete_pseudoMetricType R
(
@discrete_uniformType (
TopologicalType
(
FilteredType P P principal_filter)
discrete_topological_mixin)
erefl)
erefl.
Definition
tree_of
(
T
: nat -> pointedType)
: pseudoMetricType R :=
@product_pseudoMetricType R _
(
fun
n
=> pointed_discrete (
T n))
(
countableP _).
Lemma
cantor_like_finite_prod
(
T
: nat -> topologicalType)
:
(
forall
n,
finite_set [set: pointed_discrete (
T n)
])
->
(
forall
n,
(
exists
xy
: T n * T n, xy.
1 != xy.
2))
->
cantor_like (
tree_of T).
Proof.
End FinitelyBranchingTrees.
Local Notation
"A ^-1"
:= (
[set
xy
| A (
xy.
2, xy.
1)
])
: classical_set_scope.
## Part 4: Building a finitely branching tree to cover `T`
Section
alexandroff_hausdorff
.
Context {R : realType} {T : pseudoMetricType R}.
Hypothesis
cptT
: compact [set: T].
Hypothesis
hsdfT
: hausdorff_space T.
Section
two_pointed
.
Context (
t0
t1
: T).
Hypothesis
T2e
: t0 != t1.
Let
ent_balls'
(
E
: set (
T * T))
:
exists
M
: set (
set T)
, entourage E -> [/\
finite_set M,
forall
A,
M A -> exists
a,
A a /\
A `<=` closure [set
y
| split_ent E (
a, y)
],
exists
A
B
: set T, M A /\ M B /\ A != B,
\bigcup_(
A
in M)
A = [set: T] &
M `<=` closed].
Proof.
Let
ent_balls
E
:= projT1 (
cid (
ent_balls' E)).
Let
count_unif'
:= cid2
((
iffLR countable_uniformityP) (
@countable_uniformity_metric _ T)).
Let
count_unif
:= projT1 count_unif'.
Let
ent_count_unif
n
: entourage (
count_unif n).
Proof.
Let
count_unif_sub
E
: entourage E -> exists
N,
count_unif N `<=` E.
Proof.
by move=> entE; rewrite /count_unif; case: count_unif' => f + ? /=; exact.
Qed.
Let
K'
n
: Type := @sigT (
set T) (
ent_balls (
count_unif n)).
Let
K'p
n
: K' n.
Proof.
Let
K
n
:= PointedType (
classicType_choiceType (
K' n)) (
K'p n).
Let
Tree
:= @tree_of R K.
Let
embed_refine
n
(
U
: set T) (
k
: K n)
:=
(
if pselect (
projT1 k `&` U !=set0)
then projT1 k
else if pselect (
exists
e
: K n , projT1 e `&` U !=set0)
is left e
then projT1 (
projT1 (
cid e))
else set0)
`&` U.
Let
embed_invar
(
U
: set T)
:= closed U /\ U !=set0.
Let
Kn_closed
n
(
e
: K n)
: closed (
projT1 e).
Proof.
Local Lemma
cantor_surj_pt1
: exists2
f
: Tree -> T,
continuous f & set_surj [set: Tree] [set: T] f.
Proof.
pose entn
n
:= projT2 (
cid (
ent_balls' (
count_unif n))).
have [//| | |? []//| |? []// | |] := @tree_map_props (
@pointed_discrete R \o K)
T (
embed_refine) (
embed_invar)
cptT hsdfT.
- move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
have [//|_ _ _ + _] := entn n; rewrite -subTset.
move=> /(
_ t I)
[W cbW Wt]; exists (
existT _ W cbW)
=> //.
by rewrite /embed_refine; case: pselect => //=; apply: absurd; exists t.
- move=> n U e [clU Un0]; split.
apply: closedI => //; case: pselect => //= ?.
by case: pselect => ?; [exact: Kn_closed|exact: closed0].
rewrite /embed_refine; case: pselect => //= ?; case: pselect.
by case=> i [z [pz bz]]; set P := cid _; have := projT2 P; apply.
case: Un0 => z Uz; apply: absurd.
have [//|_ _ _ + _] := entn n; rewrite -subTset; move=> /(
_ z I)
[i bi iz].
by exists (
existT _ _ bi)
, z.
- by split; [exact: closedT | exists point].
- move=> x y xny; move: hsdfT; rewrite open_hausdorff.
move=> /(
_ _ _ xny)
[[U V]] /= [/set_mem Ux /set_mem Vy] [+ oV UVI0].
rewrite openE => /(
_ _ Ux)
; rewrite /interior -nbhs_entourageE => -[E entE ExU].
have [//| n ctE] :=
@count_unif_sub (
split_ent E `&` (
split_ent E)
^-1%classic).
exact: filterI.
exists n => B [C ebC]; have [//|_ Csub _ _ _ embx emby] := entn n.
have [[D cbD] /= Dx Dy] : exists2
e
: K n, projT1 e x & projT1 e y.
move: embx emby; rewrite /embed_refine; case: pselect => /=.
by move=> ? [? ?] [? ?]; exists (
existT _ _ ebC).
case: pselect; last by move => ? ? [].
by move=> e _ [? ?] [? ?]; exists (
projT1 (
cid e)).
suff : E (
x, y)
by move/ExU; move/eqP/disjoints_subset: UVI0 => /[apply].
have [z [Dz DzE]] := Csub _ cbD.
have /ent_closure:= DzE _ Dx => /(
_ (
ent_count_unif n))
/ctE [_ /= Exz].
have /ent_closure:= DzE _ Dy => /(
_ (
ent_count_unif n))
/ctE [Ezy _].
exact: (
@entourage_split [uniformType of T] z).
by move=> f [ctsf surjf _]; exists f.
Qed.
Local Lemma
cantor_surj_pt2
:
exists
f
: {surj [set: cantor_space] >-> [set: Tree]}, continuous f.
Proof.
Local Lemma
cantor_surj_twop
:
exists
f
: {surj [set: cantor_space] >-> [set: T]}, continuous f.
Proof.
End two_pointed.
The Alexandroff-Hausdorff theorem
Theorem
cantor_surj
:
exists
f
: {surj [set: cantor_space] >-> [set: T]}, continuous f.
Proof.
End alexandroff_hausdorff.