From 94bf9e1b128c6f8692f96854ed8a70cdbfebc255 Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 5 Oct 2024 19:39:46 -0400 Subject: [PATCH] continuous functions and subtype --- theories/function_spaces.v | 27 ++++- theories/topology.v | 221 ++++++++++++++++++++++++++++++++++++- 2 files changed, 243 insertions(+), 5 deletions(-) diff --git a/theories/function_spaces.v b/theories/function_spaces.v index fcc1a68e85..10a8288e2e 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -136,8 +136,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. @@ -528,6 +536,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 *) @@ -1028,6 +1047,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.v b/theories/topology.v index 7600e7f760..543ddc3c66 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -256,6 +256,31 @@ HB.structure Definition Topological := HB.structure Definition PointedTopological := {T of PointedNbhs T & Nbhs_isTopological T}. +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_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 Topological1. Context {T : topologicalType}. @@ -504,6 +529,34 @@ Lemma cst_continuous {T U : topologicalType} (x : U) : continuous (fun _ : T => x). Proof. by move=> t; apply: cvg_cst. Qed. +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. + Section within_topologicalType. Context {T : topologicalType} (A : set T). Implicit Types B : set T. @@ -905,7 +958,7 @@ apply: (filter_from_proper (filter_from_filter _ _)) => [|P Q M_P M_Q|P M_P]. - by exists (fun i j => setT) => ??; apply: filterT. - exists (fun i j => P i j `&` Q i j) => [??|mx PQmx]; first exact: filterI. by split=> i j; have [] := PQmx i j. -- exists (\matrix_(i, j) xget (M i j) (P i j)) => i j; rewrite mxE. +- exists (\matrix_(i, j) xget (M i j) (P i j)) => i j; rewrite mxE. by apply: xgetPex; exact: filter_ex (M_P i j). Qed. @@ -992,6 +1045,9 @@ End Weak_Topology. HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) := Pointed.on (weak_topology f). +HB.instance Definition _ {X : topologicalType} (A : set X) := + Topological.copy (set_type A) (weak_topology set_val). + (** Supremum of a family of topologies *) Definition sup_topology {T : Type} {I : Type} @@ -2744,6 +2800,8 @@ End weak_uniform. HB.instance Definition _ (pS : pointedType) (U : uniformType) (f : pS -> U) := Pointed.on (weak_topology f). +HB.instance Definition _ {X : uniformType} (A : set X) := + Uniform.copy (A : Type) (@weak_topology (A:Type) X set_val ). Definition entourage_set (U : uniformType) (A : set ((set U) * (set U))) := exists2 B, entourage B & forall PQ, A PQ -> forall p q, @@ -2775,9 +2833,9 @@ Proof. case: (pselect (exists t:T, True)). case => p _; apply: finI_filter; move=> J JsubEnt /=; exists (p, p). by IEntP => i b /= /entourage_refl ? ? _. -move=> empT. +move=> empT. have TT0 (E : set (T*T)) : E = set0. - rewrite eqEsubset; split => //=; case=> t ? _; move: empT. + rewrite eqEsubset; split => //=; case=> t ? _; move: empT. by apply: absurd; exists t. have ent0 : sup_ent set0. rewrite -(TT0 setT); exists set0 => //=; exists fset0 => //=. @@ -3843,6 +3901,10 @@ Proof. by []. Qed. End weak_pseudoMetric. +HB.instance Definition _ + {R : realType} {X : pseudoMetricType R} (A : set X) := + PseudoMetric.copy (A : Type) (@weak_topology (A:Type) X set_val). + Lemma compact_second_countable {R : realType} {T : pseudoPMetricType R} : compact [set: T] -> @second_countable T. Proof. @@ -4261,8 +4323,41 @@ case: (nbhs_subspaceP [set a] x); last by move=> _ /nbhs_singleton /= ? ? ->. by move=> -> /nbhs_singleton ?; apply: nearW => ? ->. Qed. +Lemma continuous_subspace_setT {U} (f : T -> U) : + continuous f <-> {within setT, continuous f}. +Proof. split; by move=> + x K nfK=> /(_ x K nfK); rewrite nbhs_subspaceT. Qed. + End SubspaceRelative. +Section subspace_product. +Context {X Y Z : topologicalType} (A : set X) (B : set Y) . + +Lemma nbhs_prodX_subspace_inE x : (A `*` B) x -> + @nbhs _ (subspace (A `*` B)) x = @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 /=. + case;case=> 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]]]; apply: PQABU. +case; case=> P Q /= [/(nbhs_subspace_ex _ Aa) [P' P'a PPA]]. +case/(nbhs_subspace_ex _ Bb) => Q' Q'a QQB PQU. +exists (P' , Q'); first by split. +case=> p q/= [P'p Q'q] [Ap Bq]; apply: PQU; split => /=. + by (suff : (P `&` A) p by case); rewrite PPA. +by (suff : (Q `&` B) q by case); 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. + Section SubspaceUniform. Local Open Scope relation_scope. Context {X : uniformType} (A : set X). @@ -4488,3 +4583,123 @@ 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. + +#[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. + +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; case=> V + UAVA; rewrite nbhsE; case => 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 /=; case; case=> 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 by 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 by 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 /=; apply. +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. + by move/subspace_sigL_continuousP. +by move=> ?; apply/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 [] ? ?; apply/mem_set. Qed. +Next Obligation. by case; case => a b /= /set_mem [] ? ?; apply/mem_set. Qed. + +Program Definition sigT_of_setX (ab : (A * B)%type) : (A `*` B) := + (@exist _ _ (\val ab.1, \val ab.2) _). +Next Obligation. +by case; case=> x /= /set_mem ? [y /= /set_mem ?]; apply/mem_set. +Qed. + +Lemma sigT_of_setXK : cancel sigT_of_setX setX_of_sigT. +Proof. +by case; case=> x ? [y ?]; congr (( _, _)); apply: eq_sig_hprop. +Qed. + +Lemma setX_of_sigTK : cancel setX_of_sigT sigT_of_setX. +Proof. by case; case => a b ?; apply: eq_sig_hprop. Qed. + +Lemma setX_of_sigT_continuous : continuous setX_of_sigT. +Proof. +case;case => /= 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;case => a b /= [] ? ?; exists (P', Q') => //; split. + by move: oP'; rewrite openE; exact. + by move: oQ'; rewrite openE; exact. +case; case => a b /= abAB [/= P'a Q'b]; apply: pqU. +by split => //=; [ exact: P'P | exact: Q'Q]. +Qed. + +Lemma sigT_of_setX_continuous : continuous sigT_of_setX. +Proof. +case; case => x /= Ax [y By] U [? [] [W + <-] /=]; rewrite set_valE /=. +rewrite openE /= => /[apply] [][][] P Q /=; rewrite {1}nbhsE. +rewrite {1}nbhsE /= => [][][P' [oP' P'x P'P]] [Q' [oQ' Q'y Q'Q]] PQW WU. +exists (val@^-1` P', \val@^-1` Q') => //=. + split => //=; first by (exists (\val@^-1` P'); first by split => //=; exists P'). + by exists (\val@^-1` Q'); first by split => //=; exists Q'. +case; case=> p Ap [q Bq] /= [P'p Q'q]; apply: WU; apply: PQW; split. + exact: P'P. +exact: Q'Q. +Qed. + +End subtype_setX. \ No newline at end of file