continuous functions and subtype

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) :=

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.