fixing build

CHANGELOG_UNRELEASED.md

@@ -177,9 +177,10 @@
     `completely_regular_regular`.
 - in file `topology.v`,
   + new definitions `one_point_compactification`, and `one_point_nbhs`.
-  + new lemmas `compact_normal_local`, `compact_normal`, `opc_compact`,
-    `opc_some_nbhs`, `opc_some_continuous`, `opc_open_some`,
-    `opc_weak_topology`, and `opc_hausdorff`.
+  + new lemmas `opc_compact`, `opc_some_nbhs`, `opc_some_continuous`, 
+    `opc_open_some`, `opc_weak_topology`, and `opc_hausdorff`.
+- in file `separation_axioms.v`
+  + new lemmas `compact_normal_local` and `compact_normal`.
 
 ### Changed
 

theories/separation_axioms.v

@@ -177,14 +177,14 @@ Qed.
 Lemma accessible_closed_set1 : accessible_space -> forall x : T, closed [set x].
 Proof.
 move=> T1 x; rewrite -[X in closed X]setCK; apply: open_closedC.
-rewrite openE => y /eqP /T1 [U [oU [yU xU]]].
+rewrite openE => y /eqP /T1 [U [oU yU xU]].
 rewrite /interior nbhsE /=; exists U; last by rewrite subsetC1.
 by split=> //; exact: set_mem.
 Qed.
 
 Lemma accessible_kolmogorov : accessible_space -> kolmogorov_space.
 Proof.
-move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //.
+move=> T1 x y /T1 [A [oA xA yA]]; exists A; left; split=> //.
 by rewrite nbhsE inE; exists A => //; rewrite inE in xA.
 Qed.
 
@@ -258,6 +258,28 @@ Import numFieldTopology.Exports.
 Lemma Rhausdorff (R : realFieldType) : hausdorff_space R.
 Proof. exact: order_hausdorff. Qed.
 
+Lemma opc_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(_ _); apply: hsdfX=> U V Ux Vy.
+  have [] := clxy (Some @` U) (Some @` V).
+    by move/filterS: Ux; apply; apply: preimage_image.
+    by move/filterS: Vy; apply; apply: preimage_image.
+  case=> [?|] [] /= [// p /[swap] /Some_inj <- ?] [q /[swap] /Some_inj -> ?].
+  by exists p.
+- have [U] := lcpt x I; rewrite withinET => Ux [] cU clU.
+  case/(_ (Some @` U) ((Some @` (~` U)) `|` [set None])); first exact: opc_some_nbhs.
+    by exists U.
+  by case => [?|] [][]// z /[swap] /Some_inj <- ? [] //= [? /[swap] /Some_inj ->].
+- have [U] := lcpt y I; rewrite withinET => Uy [] cU clU.
+  case/(_ ((Some @` (~` U)) `|` [set None]) (Some @` U) ); first by exists U.
+    exact: opc_some_nbhs.
+  case => [?|] [][]//= + [] ? // /[swap] /Some_inj ->.
+  by case => ? /[swap] /Some_inj <-.
+Qed.
+
+
 Section separated_topologicalType.
 Variable T : topologicalType.
 Implicit Types x y : T.
@@ -464,6 +486,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 `<=` interior 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; apply: 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 => //; apply: 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 : interior 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; apply: 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 => <-; apply: 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.

theories/topology.v

@@ -106,6 +106,8 @@ Require Import reals signed.
 (*                                     is both open and closed in A is A      *)
 (*                    separated A B == the two sets A and B are separated     *)
 (*            connected_component x == the connected component of point x     *)
+(*     one_point_compactification X == the one point compactification of X    *)
+(*                                     built on the type (option X).          *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* ### Uniform spaces                                                         *)
@@ -4488,7 +4490,6 @@ have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0.
 by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply: fcAfEb; split; exists t.
 Qed.
 
-
 Lemma continuous_localP {X Y : topologicalType} (f : X -> Y) :
   continuous f <->
   forall (x : X), \forall U \near powerset_filter_from (nbhs x),
@@ -4503,3 +4504,99 @@ move=> U nbhsU wctsf; wlog oU : U wctsf nbhsU / open U.
 move/nbhs_singleton: nbhsU; move: x; apply/in_setP.
 by rewrite -continuous_open_subspace.
 Unshelve. end_near. Qed.
+
+Definition one_point_compactification (X : Type) : Type := option X.
+
+Section one_point_compactification.
+Context {X : topologicalType}.
+
+Local Notation opc := (one_point_compactification X).
+
+HB.instance Definition _ := Choice.on opc.
+HB.instance Definition _ := Pointed.on opc.
+
+Definition one_point_nbhs (x : opc) : set_system opc := 
+  if x is Some x' then Some @ nbhs x' else
+     filter_from (compact `&` closed) (fun U => (Some @` ~`U) `|` [set None]).
+
+Let one_point_filter (x : opc) : ProperFilter (one_point_nbhs x).
+Proof.
+case: x; first by move=>?; exact: fmap_proper_filter. 
+apply: filter_from_proper; last by move=> ? _; exists None; right.
+apply: filter_from_filter.
+  by exists set0; split; [exact: compact0 | exact: closed0].
+move=> P Q [? ?] [? ?]; exists (P `|` Q); last case.
+- by split; [exact: compactU | exact: closedU].
+- by move=> ? []// [a /not_orP [? ?]] /Some_inj <-; split=>//; left; exists a.
+- by case => //= _; split; right.
+Qed.
+
+Let one_point_singleton (x : opc) U : one_point_nbhs x U -> U x.
+Proof.
+case: x; first by move=> x' /= /nbhs_singleton.
+by case=> W _; apply; right.
+Qed.
+
+Let one_point_nbhs_nbhs (p : opc) (A : set opc) : 
+  one_point_nbhs p A -> one_point_nbhs p (one_point_nbhs^~ A).
+Proof.
+case: p.
+  move=> r /=; rewrite nbhs_simpl nbhsE; case => U [oU Ur] UsA /=.
+  by exists U => //= z /=; rewrite nbhs_simpl => Uz; rewrite nbhsE; exists U.
+case => C [? ?] nCA /=; exists C => //; case; last by move=> _; exists C.
+move=> x [] // [] y /[swap] /Some_inj -> /= nCx; rewrite nbhs_simpl.
+rewrite nbhsE; exists (~` C); first by split => //; apply/closed_openC.
+by move=> z /= nCz; apply nCA; left.
+Qed.
+
+HB.instance Definition _ := hasNbhs.Build opc one_point_nbhs.
+
+HB.instance Definition _ := @Nbhs_isNbhsTopological.Build opc 
+  one_point_filter one_point_singleton one_point_nbhs_nbhs.
+
+Lemma opc_compact : compact [set: opc].
+Proof.
+apply/compact_near_coveringP => ? F /= P FF FT.
+have [//| [U i [[W /= [cptW cW WU nfI UIP]]]]] := FT None.
+have P'F : forall x, W x -> \near x & F, P F (Some x).
+  move=> x Wx; suff : \forall y \near Some @ x & f \near id @ F, P f y.
+    by rewrite near_map2.
+  exact: FT (Some x) I.
+move/compact_near_coveringP/(_ _ F _ FF P'F):cptW => cWP.
+near=> j => z _; case: z; first last.
+  apply: (UIP (None,j)); split => //=; first by apply: WU; right.
+  exact: (near nfI _).
+move=> z; case: (pselect (W z)); first by move=> ?; exact: (near cWP).
+move=> ?; apply: (UIP (Some z,j)); split => //=. 
+  by apply: WU; left; exists z.
+exact: (near nfI _).
+Unshelve. all: by end_near. Qed.
+
+Lemma opc_some_nbhs (x : X) (U : set X) : 
+  nbhs x U -> @nbhs _ opc (Some x) (Some @` U).
+Proof.
+rewrite {2}/nbhs /= nbhs_simpl /= => /filterS; apply; exact: preimage_image.
+Qed.
+
+Lemma opc_some_continuous : continuous (Some : X -> opc).
+Proof. by move=> x U. Qed.
+
+Lemma opc_open_some (U : set X) : open U -> @open opc (Some @` U).
+Proof.
+rewrite ?openE /= => Uo ? /= [x /[swap] <- Ux] /=. 
+by apply: opc_some_nbhs; apply: Uo.
+Qed.
+
+Lemma opc_weak_topology : 
+  @nbhs _ (@weak_topology X opc Some) = @nbhs _ X.
+Proof. 
+rewrite funeq2E=> x U; apply/propeqP; split; rewrite /(@nbhs _ (weak_topology _)) /=.
+  case => V [[/= W] oW <- /= Ws] /filterS; apply; apply: opc_some_continuous.
+  exact: oW.
+rewrite nbhsE; case => V [? ? ?]; exists V; split => //.
+exists (Some @` V); first exact: opc_open_some.
+rewrite eqEsubset; split => z /=; first by case=> ? /[swap] /Some_inj ->.
+by move=> ?; exists z.
+Qed.
+
+End one_point_compactification.