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.
```
pointed_principal_filter == alias for pointed types with principal
filters
cantor_space == the Cantor space, with its canonical metric
cantor_like T == perfect + compact + hausdroff + zero dimensional
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 pointed_principal_filter (
P : pointedType)
: Type := P.
HB.instance Definition _ (
P : pointedType)
:=
Pointed.on (
pointed_principal_filter P).
HB.instance Definition _ (
P : pointedType)
:=
hasNbhs.Build (
pointed_principal_filter P)
principal_filter.
Section discrete_topology_for_pointed_types.
Let discrete_pointed_subproof (
P : pointedType)
:
discrete_space (
pointed_principal_filter P).
Proof.
by []. Qed.
Definition pointed_discrete_topology (
P : pointedType)
: Type :=
discrete_topology (
discrete_pointed_subproof P).
End discrete_topology_for_pointed_types.
Lemma discrete_pointed (
T : pointedType)
:
discrete_space (
pointed_discrete_topology T).
Proof.
apply/funext => /= x; apply/funext => A; apply/propext; split.
- by move=> [E hE EA] x0 ->{x0}; apply: EA => /=; apply: hE => /=; exists x.
- move=> h; exists [set x | x.
1 = x.
2]; first by move=> -[a b] [t _] [<- <-].
by move=> y /= xy; exact: h.
Qed.
Definition cantor_space :=
prod_topology (
fun _ : nat => discrete_topology discrete_bool).
HB.instance Definition _ := Pointed.on cantor_space.
HB.instance Definition _ := Nbhs.on cantor_space.
HB.instance Definition _ := Topological.on cantor_space.
Definition cantor_like (
T : topologicalType)
:=
[/\ perfect_set [set: T],
compact [set: T],
hausdorff_space T &
zero_dimensional T].
Lemma discrete_bool_compact : compact [set: discrete_topology discrete_bool].
Proof.
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 := prod_topology 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=> discrete_topology discrete_bool)
T c_ind c_invar cmptT hsdfT.
- by move=> ?; exact: discrete_pointed.
- 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 tree_of (
T : nat -> pointedType)
: pseudoMetricType R :=
[the pseudoMetricType R of prod_topology
(
fun n => pointed_discrete_topology (
T n))
].
Lemma cantor_like_finite_prod (
T : nat -> topologicalType)
:
(
forall n, finite_set [set: pointed_discrete_topology (
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.
HB.instance Definition _ n := gen_eqMixin (
K' n).
HB.instance Definition _ n := gen_choiceMixin (
K' n).
HB.instance Definition _ n := isPointed.Build (
K' n) (
K'p n).
Let K n := [the pointedType of K' 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_topology \o K)
T (
embed_refine) (
embed_invar)
cptT hsdfT.
- by move=> n; exact: discrete_pointed.
- 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 _ 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.