subtypes and continuous functions (#1340)

* continuous functions and subtype

---------

Co-authored-by: Reynald Affeldt <[email protected]>

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

_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

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

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

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.

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.

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

@@ -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.