completely regular spaces and locally compact implies uniform

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,33 @@
 
 ### Added
 
+- in file `separation_axioms.v`,
+  + new lemmas `compact_normal_local`, and `compact_normal`.
+
+- in file `topology_theory/one_point_compactification.v`,
+  + new definitions `one_point_compactification`, and `one_point_nbhs`.
+  + new lemmas `one_point_compactification_compact`,
+    `one_point_compactification_some_nbhs`,
+    `one_point_compactification_some_continuous`,
+    `one_point_compactification_open_some`,
+    `one_point_compactification_weak_topology`, and
+    `one_point_compactification_hausdorff`.
+
+- in file `normedtype.v`,
+  + new definition `type` (in module `completely_regular_uniformity`)
+  + new lemmas `normal_completely_regular`,
+    `one_point_compactification_completely_reg`,
+    `nbhs_one_point_compactification_weakE`,
+    `locally_compact_completely_regular`, and
+    `completely_regular_regular`.
+
 ### Changed
 
+- in file `normedtype.v`,
+     changed `completely_regular_space` to depend on uniform separators
+     which removes the dependency on `R`.  The old formulation can be
+     recovered easily with `uniform_separatorP`.
+
 ### Renamed
 
 ### Generalized

_CoqProject

@@ -42,6 +42,7 @@ theories/topology_theory/uniform_structure.v
 theories/topology_theory/weak_topology.v
 theories/topology_theory/num_topology.v
 theories/topology_theory/quotient_topology.v
+theories/topology_theory/one_point_compactification.v
 
 theories/separation_axioms.v
 theories/function_spaces.v

classical/filter.v

@@ -1565,7 +1565,7 @@ move=> A [n _]; elim: n A.
 by move=> n IH A /= [B snB [C snC <-]]; apply: finI_fromI; apply: IH.
 Qed.
 
-Lemma smallest_filter_finI {T : choiceType} (D : set T) f :
+Lemma smallest_filter_finI {I T : choiceType} (D : set I) (f : I -> set T) :
   filter_from (finI_from D f) id = smallest (@Filter T) (f @` D).
 Proof. by rewrite filterI_iter_finI filterI_iterE. Qed.
 

theories/Make

@@ -28,6 +28,7 @@ topology_theory/uniform_structure.v
 topology_theory/weak_topology.v
 topology_theory/num_topology.v
 topology_theory/quotient_topology.v
+topology_theory/one_point_compactification.v
 
 ereal.v
 separation_axioms.v

theories/normedtype.v

@@ -50,6 +50,11 @@ From mathcomp Require Export separation_axioms.
 (*                                   `uniform_separator A B`                  *)
 (*       completely_regular_space == a space where points and closed sets can *)
 (*                                   be separated by a function into R        *)
+(*  completely_regular_uniformity == equips a completely_regular_space with   *)
+(*                                   the uniformity induced by continuous     *)
+(*                                   functions into the reals                 *)
+(*                                   note this uniformity is always the only  *)
+(*                                   choice, so its placed in a module        *)
 (*          uniform_separator A B == there is a suitable uniform space and    *)
 (*                                   entourage separating A and B             *)
 (*                      nbhs_norm == neighborhoods defined by the norm        *)
@@ -3687,17 +3692,19 @@ Proof. exact: (normal_spaceP 0%N 1%N). Qed.
 End normalP.
 
 Section completely_regular.
-
 Context {R : realType}.
 
-Definition completely_regular_space {T : topologicalType} :=
-  forall (a : T) (B : set T), closed B -> ~ B a -> exists f : T -> R, [/\
-    continuous f,
-    f a = 0 &
-    f @` B `<=` [set 1] ].
+(**md This is equivalent to uniformizable. Note there is a subtle
+   distinction between being uniformizable and being uniformType.
+   There is often more than one possible uniformity, and being a
+   uniformType has a specific one.
+
+   If you don't care, you can use the `completely_regular_uniformity.type`
+   which builds the uniformity.
+*)
+Definition completely_regular_space (T : topologicalType) :=
+  forall (a : T) (B : set T), closed B -> ~ B a -> uniform_separator [set a] B.
 
-(* Ideally, R should be an instance of realType here,
-   rather than a section variable. *)
 Lemma point_uniform_separator {T : uniformType} (x : T) (B : set T) :
   closed B -> ~ B x -> uniform_separator [set x] B.
 Proof.
@@ -3711,36 +3718,142 @@ Qed.
 
 Lemma uniform_completely_regular {T : uniformType} :
   @completely_regular_space T.
+Proof. by move=> x B clB Bx; exact: point_uniform_separator. Qed.
+
+Lemma normal_completely_regular {T : topologicalType} :
+  normal_space T -> accessible_space T -> completely_regular_space T.
 Proof.
-move=> x B clB Bx.
-have /(@uniform_separatorP _ R) [f] := point_uniform_separator clB Bx.
-by case=> ? _; rewrite image_set1 => fx ?; exists f; split => //; exact: fx.
+move/normal_separatorP => + /accessible_closed_set1 cl1 x A ? ?; apply => //.
+by apply/disjoints_subset => ? ->.
 Qed.
 
-End completely_regular.
-
-Section pseudometric_normal.
-
 Lemma uniform_regular {X : uniformType} : @regular_space X.
 Proof.
 move=> x A; rewrite /= -nbhs_entourageE => -[E entE].
 move/(subset_trans (ent_closure entE)) => ExA.
 by exists (xsection (split_ent E) x) => //; exists (split_ent E).
 Qed.
 
+End completely_regular.
+
+Module completely_regular_uniformity.
+Section completely_regular_uniformity.
+Context {R : realType} {X : topologicalType}.
+Hypothesis crs : completely_regular_space X.
+
+Let X' : uniformType := @sup_topology X {f : X -> R | continuous f}
+  (fun f => Uniform.class (weak_topology (projT1 f))).
+
+Let completely_regular_nbhsE : @nbhs X X = nbhs_ (@entourage X').
+Proof.
+rewrite nbhs_entourageE; apply/funext => x; apply/seteqP; split; first last.
+  apply/cvg_sup => -[f ctsf] U [/= _ [[V /= oV <- /= Vfx]]] /filterS.
+  by apply; exact/ctsf/open_nbhs_nbhs.
+move=> U; wlog oU : U / @open X U.
+  move=> WH; rewrite nbhsE => -[V [oV Vx /filterS]].
+  apply; first exact: (@nbhs_filter X').
+  by apply: WH => //; move: oV; rewrite openE; exact.
+move=> /[dup] nUx /nbhs_singleton Ux.
+have ufs : uniform_separator [set x] (~` U).
+  by apply: crs; [exact: open_closedC | exact].
+have /uniform_separatorP := ufs => /(_ R)[f [ctsf f01 fx0 fU1]].
+rewrite -nbhs_entourageE /entourage /= /sup_ent /= smallest_filter_finI.
+pose E := map_pair f @^-1` (fun pq => ball pq.1 1 pq.2).
+exists E; first last.
+  move=> z /= /set_mem; rewrite /E /=.
+  have -> : f x = 0 by apply: fx0; exists x.
+  rewrite /ball /= sub0r normrN; apply: contraPP => cUz.
+  suff -> : f z = 1 by rewrite normr1 ltxx.
+  by apply: fU1; exists z.
+move=> r /= [_]; apply => /=.
+pose f' : {classic {f : X -> R | continuous f}} := exist _ f ctsf.
+suff /asboolP entE : @entourage (weak_topology f) (f', E).2.
+  by exists (exist _ (f', E) entE).
+exists (fun pq => ball pq.1 1 pq.2) => //=.
+by rewrite /entourage /=; exists 1 => /=.
+Qed.
+
+Definition type : Type := let _ := completely_regular_nbhsE in X.
+
+#[export] HB.instance Definition _ := Topological.copy type X.
+#[export] HB.instance Definition _ := @Nbhs_isUniform.Build
+  type
+  (@entourage X')
+  (@entourage_filter X')
+  (@entourage_diagonal_subproof X')
+  (@entourage_inv X')
+  (@entourage_split_ex X')
+  completely_regular_nbhsE.
+#[export] HB.instance Definition _ := Uniform.on type.
+
+End completely_regular_uniformity.
+Module Exports. HB.reexport. End Exports.
+End completely_regular_uniformity.
+Export completely_regular_uniformity.Exports.
+
+Section locally_compact_uniform.
+Context {X : topologicalType} {R : realType}.
+Hypothesis lcpt : locally_compact [set: X].
+Hypothesis hsdf : hausdorff_space X.
+
+Let opc := @one_point_compactification X.
+
+Lemma one_point_compactification_completely_reg :
+  completely_regular_space opc.
+Proof.
+apply: (@normal_completely_regular R).
+  apply: compact_normal.
+    exact: one_point_compactification_hausdorff.
+  exact: one_point_compactification_compact.
+by apply: hausdorff_accessible; exact: one_point_compactification_hausdorff.
+Qed.
+
+#[local]
+HB.instance Definition _ := Uniform.copy opc
+  (@completely_regular_uniformity.type R _
+    one_point_compactification_completely_reg).
+
+Let X' := @weak_topology X opc Some.
+Lemma nbhs_one_point_compactification_weakE : @nbhs X X = nbhs_ (@entourage X').
+Proof. by rewrite nbhs_entourageE one_point_compactification_weak_topology. Qed.
+
+#[local, non_forgetful_inheritance]
+HB.instance Definition _ := @Nbhs_isUniform.Build
+  X
+  (@entourage X')
+  (@entourage_filter X')
+  (@entourage_diagonal_subproof X')
+  (@entourage_inv X')
+  (@entourage_split_ex X')
+  nbhs_one_point_compactification_weakE.
+
+Lemma locally_compact_completely_regular : completely_regular_space X.
+Proof. exact: uniform_completely_regular. Qed.
+
+End locally_compact_uniform.
+
+Lemma completely_regular_regular {R : realType} {X : topologicalType} :
+  completely_regular_space X -> @regular_space X.
+Proof.
+move=> crsX; pose P' := @completely_regular_uniformity.type R _ crsX.
+exact: (@uniform_regular P').
+Qed.
+
+Section pseudometric_normal.
+
 Lemma regular_openP {T : topologicalType} (x : T) :
   {for x, @regular_space T} <-> forall A, closed A -> ~ A x ->
   exists U V : set T, [/\ open U, open V, U x, A `<=` V & U `&` V = set0].
 Proof.
 split.
   move=> + A clA nAx => /(_ (~` A)) [].
     by apply: open_nbhs_nbhs; split => //; exact: closed_openC.
-  move=> U Ux /subsetC; rewrite setCK => AclU; exists (interior U).
+  move=> U Ux /subsetC; rewrite setCK => AclU; exists U^°.
   exists (~` closure U) ; split => //; first exact: open_interior.
     exact/closed_openC/closed_closure.
   apply/disjoints_subset; rewrite setCK.
   exact: (subset_trans (@interior_subset _ _) (@subset_closure _ _)).
-move=> + A Ax => /(_ (~` interior A)) []; [|exact|].
+move=> + A Ax => /(_ (~` A^°)) []; [|exact|].
   exact/open_closedC/open_interior.
 move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U.
   exact/open_nbhs_nbhs.

theories/separation_axioms.v

@@ -257,6 +257,28 @@ Import numFieldTopology.Exports.
 Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
 Proof. exact: order_hausdorff. Qed.
 
+Lemma one_point_compactification_hausdorff {X : topologicalType} :
+   locally_compact [set: X] ->
+   hausdorff_space X ->
+   hausdorff_space (one_point_compactification X).
+Proof.
+move=> lcpt hsdfX [x|] [y|] //=.
+- move=> clxy; congr Some; apply: hsdfX => U V Ux Vy.
+  have [] := clxy (Some @` U) (Some @` V).
+    by apply: filterS Ux; exact: preimage_image.
+    by apply: filterS Vy; exact: preimage_image.
+  by case=> [_|] [] /= [// p /[swap] -[] <- Up] [q /[swap] -[] -> Vp]; exists p.
+- have [U] := lcpt x I; rewrite withinET => Ux [cU clU].
+  case/(_ (Some @` U) (Some @` (~` U) `|` [set None])).
+  + exact: one_point_compactification_some_nbhs.
+  + by exists U.
+  + by move=> [?|] [][]// z /[swap] -[] <- ? []//= [? /[swap] -[] ->].
+- have [U] := lcpt y I; rewrite withinET => Uy [cU clU].
+  case/(_ (Some @` (~` U) `|` [set None]) (Some @` U)); first by exists U.
+    exact: one_point_compactification_some_nbhs.
+  by case=> [?|] [] [] //= + [] ? // /[swap] -[] -> => -[? /[swap] -[] <-].
+Qed.
+
 Section hausdorff_topologicalType.
 Variable T : topologicalType.
 Implicit Types x y : T.
@@ -465,6 +487,54 @@ have /closure_id -> : closed (~` B); first by exact: open_closedC.
 by apply/closure_subset/disjoints_subset; rewrite setIC.
 Qed.
 
+Lemma compact_normal_local (K : set T) : hausdorff_space T -> compact K ->
+  forall A : set T, A `<=` K^° -> {for A, normal_space}.
+Proof.
+move=> hT cptV A AK clA B snAB; have /compact_near_coveringP cvA : compact A.
+  apply/(subclosed_compact clA cptV)/(subset_trans AK).
+  exact: interior_subset.
+have snbC (U : set T) : Filter (filter_from (set_nbhs U) closure).
+  apply: filter_from_filter; first by exists setT; apply: filterT.
+  by move=> P Q sAP sAQ; exists (P `&` Q); [apply filterI|exact: closureI].
+have [/(congr1 setC)|/set0P[b0 B0]] := eqVneq (~` B) set0.
+  by rewrite setCK setC0 => ->; exact: filterT.
+have PsnA : ProperFilter (filter_from (set_nbhs (~` B)) closure).
+  apply: filter_from_proper => ? P.
+  by exists b0; apply/subset_closure; apply: nbhs_singleton; exact: P.
+pose F := powerset_filter_from (filter_from (set_nbhs (~` B)) closure).
+have PF : Filter F by exact: powerset_filter_from_filter.
+have cvP (x : T) : A x -> \forall x' \near x & i \near F, (~` i) x'.
+  move=> Ax; case/set_nbhsP : snAB => C [oC AC CB].
+  have [] := @compact_regular x _ hT cptV _ C; first exact: AK.
+    by rewrite nbhsE /=; exists C => //; split => //; exact: AC.
+  move=> D /nbhs_interior nD cDC.
+  have snBD : filter_from (set_nbhs (~` B)) closure (closure (~` closure D)).
+    exists (closure (~` closure D)) => [z|].
+      move=> nBZ; apply: filterS; first exact: subset_closure.
+      apply: open_nbhs_nbhs; split; first exact/closed_openC/closed_closure.
+      exact/(subsetC _ nBZ)/(subset_trans cDC).
+    by have := @closed_closure _ (~` closure D); rewrite closure_id => <-.
+  near=> y U => /=; have Dy : D^° y by exact: (near nD _).
+  have UclD : U `<=` closure (~` closure D).
+    exact: (near (small_set_sub snBD) U).
+  move=> Uy; have [z [/= + Dz]] := UclD _ Uy _ Dy.
+  by apply; exact: subset_closure.
+case/(_ _ _ _ _ cvP) : cvA => R /= [RA Rmono [U RU] RBx].
+have [V /set_nbhsP [W [oW cBW WV] clVU]] := RA _ RU; exists (~` W).
+  apply/set_nbhsP; exists (~` closure W); split.
+  - exact/closed_openC/closed_closure.
+  - by move=> y /(RBx _ RU) + Wy; apply; exact/clVU/(closure_subset WV).
+  - by apply: subsetC; exact/subset_closure.
+have : closed (~` W) by exact: open_closedC.
+by rewrite closure_id => <-; exact: subsetCl.
+Unshelve. all: by end_near. Qed.
+
+Lemma compact_normal : hausdorff_space T -> compact [set: T] -> normal_space.
+Proof.
+move=> ? /compact_normal_local + A clA; apply => //.
+by move=> z ?; exact: filterT.
+Qed.
+
 End set_separations.
 
 Arguments normal_space : clear implicits.