From 96f4793f5e0adb9f62dff744f9d4e33dca7ff999 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Wed, 6 Nov 2024 12:40:31 -0500 Subject: [PATCH] subtypes and continuous functions (#1340) * continuous functions and subtype --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 15 ++ _CoqProject | 1 + theories/Make | 1 + theories/function_spaces.v | 27 +++- theories/topology_theory/subspace_topology.v | 60 +++++++- theories/topology_theory/subtype_topology.v | 136 ++++++++++++++++++ theories/topology_theory/topology.v | 1 + theories/topology_theory/topology_structure.v | 68 ++++++++- 8 files changed, 304 insertions(+), 5 deletions(-) create mode 100644 theories/topology_theory/subtype_topology.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6e35b69d6..b5153bd4d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -106,6 +106,21 @@ `closure_open_regclosed`, `interior_closed_regopen`, `closure_interior_idem`, `interior_closure_idem` +- in file `topology_structure.v`, + + mixin `isContinuous`, type `continuousType`, structure `Continuous` + + new lemma `continuousEP`. + + new definition `mkcts`. + +- in file `subspace_topology.v`, + + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and + `continuous_subspace_prodP`. + + type `continuousFunType`, HB structure `ContinuousFun` + +- in file `subtype_topology.v`, + + new lemmas `subspace_subtypeP`, `subspace_sigL_continuousP`, + `subspace_valL_continuousP'`, `subspace_valL_continuousP`, `sigT_of_setXK`, + `setX_of_sigTK`, `setX_of_sigT_continuous`, and `sigT_of_setX_continuous`. + ### Changed ### Renamed diff --git a/_CoqProject b/_CoqProject index febad3bd7..b72bbf69d 100644 --- a/_CoqProject +++ b/_CoqProject @@ -51,6 +51,7 @@ theories/topology_theory/order_topology.v theories/topology_theory/product_topology.v theories/topology_theory/pseudometric_structure.v theories/topology_theory/subspace_topology.v +theories/topology_theory/subtype_topology.v theories/topology_theory/supremum_topology.v theories/topology_theory/topology_structure.v theories/topology_theory/uniform_structure.v diff --git a/theories/Make b/theories/Make index cf786d30d..787082052 100644 --- a/theories/Make +++ b/theories/Make @@ -19,6 +19,7 @@ topology_theory/order_topology.v topology_theory/product_topology.v topology_theory/pseudometric_structure.v topology_theory/subspace_topology.v +topology_theory/subtype_topology.v topology_theory/supremum_topology.v topology_theory/topology_structure.v topology_theory/uniform_structure.v diff --git a/theories/function_spaces.v b/theories/function_spaces.v index ec398b240..628142d6a 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -151,8 +151,16 @@ HB.instance Definition _ (U : Type) (T : U -> topologicalType) := HB.instance Definition _ (U : Type) (T : U -> uniformType) := Uniform.copy (forall x : U, T x) (prod_topology T). -HB.instance Definition _ (U : Type) R (T : U -> pseudoMetricType R) := - Uniform.copy (forall x : U, T x) (prod_topology T). +HB.instance Definition _ (U T : topologicalType) := + Topological.copy + (continuousType U T) + (weak_topology (id : continuousType U T -> (U -> T))). + +HB.instance Definition _ (U : topologicalType) (T : uniformType) := + Uniform.copy + (continuousType U T) + (weak_topology (id : continuousType U T -> (U -> T))). + End ArrowAsProduct. Section product_spaces. @@ -544,6 +552,17 @@ HB.instance Definition _ (U : choiceType) (V : uniformType) := HB.instance Definition _ (U : choiceType) (R : numFieldType) (V : pseudoMetricType R) := PseudoMetric.copy (U -> V) (arrow_uniform_type U V). + +HB.instance Definition _ (U : topologicalType) (T : uniformType) := + Uniform.copy + (continuousType U T) + (weak_topology (id : continuousType U T -> (U -> T))). + +HB.instance Definition _ (U : topologicalType) (R : realType) + (T : pseudoMetricType R) := + PseudoMetric.on + (weak_topology (id : continuousType U T -> (U -> T))). + End ArrowAsUniformType. (** Limit switching *) @@ -1044,6 +1063,10 @@ End compact_open_uniform. Module ArrowAsCompactOpen. HB.instance Definition _ (U : topologicalType) (V : topologicalType) := Topological.copy (U -> V) {compact-open, U -> V}. + +HB.instance Definition _ (U : topologicalType) (V : topologicalType) := + Topological.copy (continuousType U V) + (weak_topology (id : (continuousType U V) -> (U -> V)) ). End ArrowAsCompactOpen. Definition compactly_in {U : topologicalType} (A : set U) := diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index 7c7b02e87..0168e1809 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -3,6 +3,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. From mathcomp Require Import topology_structure uniform_structure compact . From mathcomp Require Import pseudometric_structure connected weak_topology. +From mathcomp Require Import product_topology. (**md**************************************************************************) (* # Subspaces of topological spaces *) @@ -12,6 +13,12 @@ From mathcomp Require Import pseudometric_structure connected weak_topology. (* topology that ignores points outside A *) (* incl_subspace x == with x of type subspace A with (A : set T), *) (* inclusion of subspace A into T *) +(* nbhs_subspace x == filter associated with x : subspace A *) +(* subspace_ent A == subspace entourages *) +(* subspace_ball A == balls of the pseudometric subspace structure *) +(* continuousFunType A B == type of continuous function from set A to set B *) +(* with domain subspace A *) +(* The HB structure is ContinuousFun. *) (* ``` *) (******************************************************************************) @@ -32,7 +39,6 @@ Definition incl_subspace {T A} (x : subspace A) : T := x. Section Subspace. Context {T : topologicalType} (A : set T). - Definition nbhs_subspace (x : subspace A) : set_system (subspace A) := if x \in A then within A (nbhs x) else globally [set x]. @@ -635,3 +641,55 @@ 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. + +Lemma continuous_subspace_setT {T U : topologicalType} (f : T -> U) : + continuous f <-> {within setT, continuous f}. +Proof. by split => + x K nfK=> /(_ x K nfK); rewrite nbhs_subspaceT. Qed. + +Section subspace_product. +Context {X Y Z : topologicalType} (A : set X) (B : set Y) . + +Lemma nbhs_prodX_subspace_inE x : (A `*` B) x -> + nbhs (x : subspace (A `*` B)) = @nbhs _ (subspace A * subspace B)%type x. +Proof. +case: x => a b [/= Aa Bb]; rewrite /nbhs/= -nbhs_subspace_in//. +rewrite funeqE => U /=; rewrite propeqE; split; rewrite /nbhs /=. + move=> [[P Q]] /= [nxP nyQ] PQABU; exists (P `&` A, Q `&` B). + by split; apply/nbhs_subspace_ex => //=; [exists P | exists Q]; + rewrite // -setIA setIid. + by case=> p q [[/= Pp Ap [Qq Bq]]]; exact: PQABU. +move=> [[P Q]] /= [/(nbhs_subspace_ex _ Aa) [P' P'a PPA]]. +move/(nbhs_subspace_ex _ Bb) => [Q' Q'a QQB PQU]. +exists (P', Q') => //= -[p q] [P'p Q'q] [Ap Bq]; apply: PQU; split => /=. + by have [] : (P `&` A) p by rewrite PPA. +by have [] : (Q `&` B) q by rewrite QQB. +Qed. + +Lemma continuous_subspace_prodP (f : X * Y -> Z) : + {in A `*` B, continuous (f : subspace A * subspace B -> Z)} <-> + {within A `*` B, continuous f}. +Proof. +by split; rewrite continuous_subspace_in => + x ABx U nfxU => /(_ x ABx U nfxU); + rewrite nbhs_prodX_subspace_inE//; move/set_mem: ABx. +Qed. +End subspace_product. + +#[short(type = "continuousFunType")] +HB.structure Definition ContinuousFun {X Y : topologicalType} + (A : set X) (B : set Y) := + {f of @isFun (subspace A) Y A B f & @Continuous (subspace A) Y f }. + +Section continuous_fun_comp. +Context {X Y Z : topologicalType} (A : set X) (B : set Y) (C : set Z). +Context {f : continuousFunType A B} {g : continuousFunType B C}. + +Local Lemma continuous_comp_subproof : continuous (g \o f : subspace A -> Z). +Proof. +move=> x; apply: continuous_comp; last exact: cts_fun. +exact/subspaceT_continuous/cts_fun. +Qed. + +HB.instance Definition _ := + @isContinuous.Build (subspace A) Z (g \o f) continuous_comp_subproof. + +End continuous_fun_comp. diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v new file mode 100644 index 000000000..a413d6cec --- /dev/null +++ b/theories/topology_theory/subtype_topology.v @@ -0,0 +1,136 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +From mathcomp Require Import reals topology_structure uniform_structure compact. +From mathcomp Require Import pseudometric_structure connected weak_topology. +From mathcomp Require Import product_topology subspace_topology. + +(**md**************************************************************************) +(* # Subtypes of topological spaces *) +(* We have two distinct ways of building topologies as subsets of a *) +(* topological space `X`. One is the `subspace topology`, which is defined in *) +(* `subspace_topology.v`. It builds a topology on X which 'isolates' a set A. *) +(* The other, defined in this file, defines a topology on the sigma type *) +(* `set_type` in the weak topology by the inclusion. Note `subspace A` has *) +(* the advantage that it preserves all the algebraic structure on X, but only *) +(* the local behavior A (in particular, continuity). On the other hand *) +(* `set_type A` has the right global properties you'd expect for the subset *) +(* topology. But you can't easily add two elements of `set_val [0, 1]`. *) +(* Note the implicit coercion from sets to `set_val` from `classical_sets.v`. *) +(* *) +(* This file provides `set_type` with a topology, and some theory. *) +(* ``` *) +(* sigT_of_setX == commutes `set_type` and product topologies *) +(* setX_of_sigT == commutes product and `set_type` topologies *) +(* ``` *) +(* *) +(******************************************************************************) + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +HB.instance Definition _ {X : topologicalType} (A : set X) := + Topological.copy (set_type A) (weak_topology set_val). + +HB.instance Definition _ {X : uniformType} (A : set X) := + Uniform.copy (A : Type) (@weak_topology (A : Type) X set_val). + +HB.instance Definition _ {R : realType} {X : pseudoMetricType R} (A : set X) := + PseudoMetric.copy (A : Type) (@weak_topology (A : Type) X set_val). + +Section subspace_sig. +Context {X : topologicalType} (A : set X). + +Lemma subspace_subtypeP (x : A) (U : set A) : + nbhs x U <-> nbhs (set_val x : subspace A) (set_val @` U). +Proof. +rewrite /nbhs /= -nbhs_subspace_in //; first last. + by case: x; rewrite set_valE => //= ? /set_mem. +split. + case=> _ /= [] [W oW <- /= Wx sWU]; move: oW; rewrite openE /= /interior. + move=> /(_ _ Wx); apply: filter_app; apply: nearW => w /= Ww /mem_set Aw. + by exists (@exist _ _ w Aw) => //; exact: sWU. +rewrite withinE => -[V + UAVA]; rewrite nbhsE => -[V' [oV' V'x V'V]]. +exists (sval @^-1` V'); split => //=; first by exists V'. +move=> w /= /V'V Vsw; have : (V `&` A) (\val w). + by split => //; case: w Vsw => //= ? /set_mem. +by rewrite -UAVA => -[[v ? /eq_sig_hprop] <-]. +Qed. + +Lemma subspace_sigL_continuousP {Y : topologicalType} (f : X -> Y) : + {within A, continuous f} <-> continuous (sigL A f). +Proof. +split. + have /continuous_subspaceT/subspaceT_continuous := + @weak_continuous A X set_val. + move=> svf ctsf; apply/continuous_subspace_setT => x. + apply: (@continuous_comp (subspace _) (subspace A)); last exact: ctsf. + by move=> U nfU; exact: svf. +rewrite continuous_subspace_in => + x Ax U nfxU. +move=> /(_ (@exist _ _ x Ax) U) /= []; first exact: nfxU. +move=> _ [/= [W + <- /=]] Wx svWU; rewrite nbhs_simpl/=. +rewrite /nbhs /= -nbhs_subspace_in; last exact/set_mem. +rewrite openE /= /interior=> /(_ _ Wx); rewrite {1}set_valE/=. +apply: filter_app; apply: nearW => w Ww /= /mem_set Aw. +by have /= := svWU (@exist _ _ w Aw); rewrite ?set_valE /=; exact. +Qed. + +Lemma subspace_valL_continuousP' {Y : topologicalType} (y : Y) (f : A -> Y) : + {within A, continuous (valL_ y f)} <-> continuous f. +Proof. +rewrite -{2}[f](@valLK _ _ y A); split=> [/subspace_sigL_continuousP//|cf]. +exact/subspace_sigL_continuousP. +Qed. + +Lemma subspace_valL_continuousP {Y : ptopologicalType} (f : A -> Y) : + {within A, continuous (valL f)} <-> continuous f. +Proof. exact: (@subspace_valL_continuousP' _ point). Qed. + +End subspace_sig. + +Section subtype_setX. +Context {X Y : topologicalType} (A : set X) (B : set Y). + +Program Definition setX_of_sigT (ab : A `*` B) : (A * B)%type := + (@exist _ _ ab.1 _, @exist _ _ ab.2 _). +Next Obligation. by case; case => a b /= /set_mem [] ? ?; exact/mem_set. Qed. +Next Obligation. by case; case => a b /= /set_mem [] ? ?; exact/mem_set. Qed. + +Program Definition sigT_of_setX (ab : (A * B)%type) : A `*` B := + (@exist _ _ (\val ab.1, \val ab.2) _). +Next Obligation. +by move=> [[x/= /set_mem Ax] [y/= /set_mem By]]; exact/mem_set. +Qed. + +Lemma sigT_of_setXK : cancel sigT_of_setX setX_of_sigT. +Proof. by move=> [[x ?] [y ?]]; congr (( _, _)); exact: eq_sig_hprop. Qed. + +Lemma setX_of_sigTK : cancel setX_of_sigT sigT_of_setX. +Proof. by move=> [[a b] ?]; exact: eq_sig_hprop. Qed. + +Lemma setX_of_sigT_continuous : continuous setX_of_sigT. +Proof. +move=> [[x y] p] U [/= [P Q]] /= [nxP nyQ] pqU. +case: nxP => _ [/= [] P' oP' <- /=]; rewrite set_valE /= => P'x P'P. +case: nyQ => _ [/= [] Q' oQ' <- /=]; rewrite set_valE /= => Q'x Q'Q. +pose PQ : set (A `*` B) := \val @^-1` (P' `*` Q'). +exists PQ; split => //=. + exists (P' `*` Q') => //; rewrite openE => -[a b /=] [P'a Q'b]. + exists (P', Q') => //; split. + - by move: oP'; rewrite openE; exact. + - by move: oQ'; rewrite openE; exact. +by move=> [[a b]/= abAB [P'a Q'b]]; apply/pqU; split; [exact: P'P|exact: Q'Q]. +Qed. + +Lemma sigT_of_setX_continuous : continuous sigT_of_setX. +Proof. +move=> [[x Ax] [y By]] U [? [] [W + <-] /=]; rewrite set_valE/=. +rewrite openE /= => /[apply] [][][] P Q /=; rewrite (nbhsE x) (nbhsE y) => -[]. +move=> [P' [oP' P'x P'P]] [Q' [oQ' Q'y Q'Q]] PQW WU. +exists (val @^-1` P', \val @^-1` Q') => /=; first split. +- by exists (\val@^-1` P'); split => //=; exists P'. +- by exists (\val @^-1` Q'); split => //=; exists Q'. +- by move=> [[p Ap] [q Bq]]/= [P'p Q'q]; apply/WU/PQW; + split; [exact: P'P|exact: Q'Q]. +Qed. + +End subtype_setX. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 25460c770..604b4af8a 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -10,6 +10,7 @@ From mathcomp Require Export order_topology. From mathcomp Require Export product_topology. From mathcomp Require Export pseudometric_structure. From mathcomp Require Export subspace_topology. +From mathcomp Require Export subtype_topology. From mathcomp Require Export supremum_topology. From mathcomp Require Export topology_structure. From mathcomp Require Export uniform_structure. diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index 29580b71a..5e78bde1c 100644 --- a/theories/topology_theory/topology_structure.v +++ b/theories/topology_theory/topology_structure.v @@ -40,10 +40,14 @@ From mathcomp Require Export filter. (* excluded (a "deleted neighborhood") *) (* limit_point E == the set of limit points of E *) (* discrete_space T == every nbhs is a principal filter *) -(* dense S == the set (S : set T) is dense in T, with T of *) -(* type topologicalType *) (* discrete_space dscT == the discrete topology on T, provided *) (* a (dscT : discrete_space T) *) +(* dense S == the set (S : set T) is dense in T, with T of *) +(* type topologicalType *) +(* continuousType == type of continuous functions *) +(* The HB structures is Continuous. *) +(* mkcts f_cts == object of type continuousType corresponding to *) +(* the function f (f_cts : continuous f) *) (* ``` *) (* ### Factories *) (* ``` *) @@ -973,3 +977,63 @@ Lemma clopen_comp {T U : topologicalType} (f : T -> U) (A : set U) : Proof. by case=> ? ?; split; [ exact: open_comp | exact: closed_comp]. Qed. End ClopenSets. + +HB.mixin Record isContinuous {X Y : nbhsType} (f : X -> Y):= { + cts_fun : continuous f +}. + +#[short(type = "continuousType")] +HB.structure Definition Continuous {X Y : nbhsType} := { + f of @isContinuous X Y f +}. + +HB.instance Definition _ {X Y : topologicalType} := + gen_eqMixin (continuousType X Y). +HB.instance Definition _ {X Y : topologicalType} := + gen_choiceMixin (continuousType X Y). + +Lemma continuousEP {X Y : nbhsType} (f g : continuousType X Y) : + f = g <-> f =1 g. +Proof. +case: f g => [f [[ffun]]] [g [[gfun]]]/=; split=> [[->//]|/funext eqfg]. +rewrite eqfg in ffun *; congr {| Continuous.sort := _; Continuous.class := {| + Continuous.topology_structure_isContinuous_mixin := + {|isContinuous.cts_fun := _|}|}|}. +exact: Prop_irrelevance. +Qed. + +Definition mkcts {X Y : nbhsType} (f : X -> Y) (f_cts : continuous f) := f. + +HB.instance Definition _ {X Y : nbhsType} (f: X -> Y) (f_cts : continuous f) := + @isContinuous.Build X Y (mkcts f_cts) f_cts. + +Section continuous_comp. +Context {X Y Z : topologicalType}. +Context (f : continuousType X Y) (g : continuousType Y Z). + +Local Lemma cts_fun_comp : continuous (g \o f). +Proof. move=> x; apply: continuous_comp; exact: cts_fun. Qed. + +HB.instance Definition _ := @isContinuous.Build X Z (g \o f) cts_fun_comp. + +End continuous_comp. + +Section continuous_id. +Context {X : topologicalType}. + +Local Lemma cts_id : continuous (@idfun X). +Proof. by move=> ?. Qed. + +HB.instance Definition _ := @isContinuous.Build X X (@idfun X) cts_id. + +End continuous_id. + +Section continuous_const. +Context {X Y : topologicalType} (y : Y). + +Local Lemma cts_const : continuous (@cst X Y y). +Proof. by move=> ?; exact: cvg_cst. Qed. + +HB.instance Definition _ := @isContinuous.Build X Y (cst y) cts_const. + +End continuous_const.