diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b..893b80843 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/_CoqProject b/_CoqProject index b670dbef3..4b266b226 100644 --- a/_CoqProject +++ b/_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 diff --git a/classical/filter.v b/classical/filter.v index 96385a0e2..48417ea37 100644 --- a/classical/filter.v +++ b/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. diff --git a/theories/Make b/theories/Make index d43131777..06da64bde 100644 --- a/theories/Make +++ b/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 diff --git a/theories/normedtype.v b/theories/normedtype.v index bf6d1713a..6068c1001 100644 --- a/theories/normedtype.v +++ b/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,16 +3718,15 @@ 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]. @@ -3728,6 +3734,113 @@ 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]. @@ -3735,12 +3848,12 @@ 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. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index e1ea94f40..4f54e83e1 100644 --- a/theories/separation_axioms.v +++ b/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. diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v new file mode 100644 index 000000000..7c970d03f --- /dev/null +++ b/theories/topology_theory/one_point_compactification.v @@ -0,0 +1,107 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import signed topology_structure uniform_structure. +From mathcomp Require Import pseudometric_structure compact weak_topology. + +(**md**************************************************************************) +(* # One-Point Compactifications *) +(* *) +(* Builds the one-point compactification of a topological space `X`. The main *) +(* results are that the compactification is indeed compact, and that `X` *) +(* embeds into its one-point compactification. *) +(* *) +(* one_point_compactification X == the one-point compactification of `X` *) +(* as an alias of `option X` *) +(******************************************************************************) + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +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 => [x|]; first 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 [cptP cloP] [cptQ cloQ]; exists (P `|` Q). +- by split; [exact: compactU | exact: closedU]. +- case=> [x [|//]|[] //= _]; [|by split; right..]. + by move=> [a /not_orP[Pa Qa]] [<-{x}]; split => //; left; exists a. +Qed. + +Let one_point_singleton (x : opc) U : one_point_nbhs x U -> U x. +Proof. by case: x => [x' /= /nbhs_singleton//|[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 => [r /=|]. + rewrite nbhs_simpl nbhsE => -[U [oU Ur] USA/=]. + by exists U => //= z /=; rewrite nbhs_simpl nbhsE => Uz; exists U. +case=> C [cptC cloC] nCA /=; exists C => // -[|_]; last by exists C. +move=> x [|//] [y] /[swap] -[-> /=] nCx; rewrite nbhs_simpl nbhsE/=. +exists (~` C); first by split => //; exact: 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 one_point_compactification_compact : compact [set: opc]. +Proof. +apply/compact_near_coveringP => ? F /= P FF FT. +have [[U i] [[W [cptW cW] /= WU nFi UiP]]] := FT None I. +have P'F x : W x -> \near x & F, P F (Some x). + move=> 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 => [z|]. +- have [?|Wz] := pselect (W z); first exact: (near cWP). + by apply: (UiP (_, _)); split => /=; + [apply: WU; left; exists z|exact: (near nFi)]. +- by apply: (UiP (_, _)); split => /=; [apply: WU; right|exact: (near nFi)]. +Unshelve. all: by end_near. Qed. + +Lemma one_point_compactification_some_nbhs (x : X) (U : set X) : + nbhs x U -> @nbhs _ opc (Some x) (Some @` U). +Proof. exact/filterS/preimage_image. Qed. + +Lemma one_point_compactification_some_continuous : continuous (Some : X -> opc). +Proof. by move=> x U. Qed. + +Lemma one_point_compactification_open_some (U : set X) : + open U -> @open opc (Some @` U). +Proof. +rewrite !openE/= => UU' opcX [x /UU' Ux <-]. +exact/one_point_compactification_some_nbhs. +Qed. + +Lemma one_point_compactification_weak_topology : + @nbhs _ (@weak_topology X opc Some) = @nbhs _ X. +Proof. +rewrite predeq2E => x U; split; rewrite /(@nbhs _ (weak_topology _))/=. + case=> _ [[/= W] oW <- /= WSs] /filterS; apply. + exact/one_point_compactification_some_continuous/oW. +rewrite nbhsE => -[V [oV Vx VU]]; exists V; split => //. +exists (Some @` V); first exact: one_point_compactification_open_some. +by rewrite eqEsubset; split=> [y [z Vz [<-//]]|]; exact: preimage_image. +Qed. + +End one_point_compactification. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 6b5552b87..357618420 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -14,3 +14,4 @@ From mathcomp Require Export supremum_topology. From mathcomp Require Export topology_structure. From mathcomp Require Export uniform_structure. From mathcomp Require Export weak_topology. +From mathcomp Require Export one_point_compactification.