diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2a462bee5..98f82b072 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 453f254ed..2cdaac7e8 100644 --- a/theories/separation_axioms.v +++ b/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. diff --git a/theories/topology.v b/theories/topology.v index 274fd86df..0505c8907 100644 --- a/theories/topology.v +++ b/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. \ No newline at end of file