subtypes and continuous functions

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,17 @@
 
 ### Added
 
+- in file `topology_structure.v`,
+  + new definition `mkcts`.
+  + new lemma `continuousEP`.
+- in file `subspace_topology.v`,
+  + new lemmas `continuous_subspace_setT`, `nbhs_prodX_subspace_inE`, and 
+    `continuous_subspace_prodP`.
+- 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

_CoqProject

@@ -36,6 +36,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

theories/Make

@@ -22,6 +22,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

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.
@@ -543,6 +551,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 *)
@@ -1043,6 +1062,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_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                                          *)
@@ -635,3 +636,56 @@ 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. split; by move=> + 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 /=.
+  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.
+
+#[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.

theories/topology_theory/subtype_topology.v

@@ -0,0 +1,139 @@
+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. *)
+(* Ther 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`.        *)
+(*                                                                            *)
+(* 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; 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.

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.

theories/topology_theory/topology_structure.v

@@ -893,3 +893,57 @@ 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.
+