adding the sigT topology (#1368)

* adding the sigT topology

Co-authored-by: affeldt-aist <[email protected]>

---------

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

CHANGELOG_UNRELEASED.md

@@ -57,6 +57,17 @@
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
 
+- in file `mathcomp_extra.v`,
+  + new definition `sigT_fun`.
+- in file `sigT_topology.v`,
+  + new definition `sigT_nbhs`.
+  + new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`,
+    `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and 
+    `sigT_compact`.
+- in file `separation_axioms.v`,
+  + new lemma `sigT_hausdorff`.
+
+
 ### Changed
 
 - in file `normedtype.v`,

_CoqProject

@@ -58,6 +58,7 @@ theories/topology_theory/weak_topology.v
 theories/topology_theory/num_topology.v
 theories/topology_theory/quotient_topology.v
 theories/topology_theory/one_point_compactification.v
+theories/topology_theory/sigT_topology.v
 
 theories/separation_axioms.v
 theories/function_spaces.v

classical/mathcomp_extra.v

@@ -13,9 +13,11 @@ From mathcomp Require Import finset interval.
 (*             dfwith f x == fun j => x if j = i, and f j otherwise           *)
 (*                           given x : T i                                    *)
 (*                 swap x := (x.2, x.1)                                       *)
-(*           map_pair f x := (f x.1, f x.2)                                       *)
+(*           map_pair f x := (f x.1, f x.2)                                   *)
 (*         monotonous A f := {in A &, {mono f : x y / x <= y}} \/             *)
 (*                           {in A &, {mono f : x y /~ x <= y}}               *)
+(*             sigT_fun f := lifts a family of functions f into a function on *)
+(*                           the dependent sum                                *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -509,3 +511,7 @@ Proof.
 move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab).
 by rewrite in_itv/= !fge ?(itvP xab).
 Qed.
+
+Definition sigT_fun {I : Type} {X : I -> Type} {T : Type}
+  (f : forall i, X i -> T) (x : {i & X i}) : T :=
+  (f (projT1 x) (projT2 x)).

theories/Make

@@ -26,6 +26,8 @@ topology_theory/weak_topology.v
 topology_theory/num_topology.v
 topology_theory/quotient_topology.v
 topology_theory/one_point_compactification.v
+topology_theory/sigT_topology.v
+
 separation_axioms.v
 function_spaces.v
 cantor.v

theories/separation_axioms.v

@@ -1125,3 +1125,23 @@ by move=> y [] ? [->] -> /eqP.
 Qed.
 
 End perfect_sets.
+
+Section sigT_separations.
+Context {I : choiceType} {X : I -> topologicalType}.
+
+Lemma sigT_hausdorff :
+  (forall i, hausdorff_space (X i)) -> hausdorff_space {i & X i}.
+Proof.
+move=> hX [i x] [j y]; rewrite/cluster /= /nbhs /= 2!sigT_nbhsE /= => cl.
+have [] := cl (existT X i @` [set: X i]) (existT X j @` [set: X j]);
+  [by apply: existT_nbhs; exact: filterT..|].
+move=> p [/= [_ _ <-] [_ _ [ji]]] _.
+rewrite {}ji {j} in x y cl *.
+congr existT; apply: hX => U V Ux Vy.
+have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|].
+move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //.
+rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr.
+by move=> a b; exact: pselect.
+Qed.
+
+End sigT_separations.

theories/topology_theory/sigT_topology.v

@@ -0,0 +1,87 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra all_classical.
+From mathcomp Require Import topology_structure compact subspace_topology.
+
+(**md**************************************************************************)
+(* # sigT topology                                                            *)
+(*  This file equips the type {i & X i} with its standard topology            *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*         sigT_nbhs x == the neighborhoods of the standard topology on the   *)
+(*                        type {i & X i}                                      *)
+(* ```                                                                        *)
+(******************************************************************************)
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Section sigT_topology.
+Context {I : choiceType} {X : I -> topologicalType}.
+
+Definition sigT_nbhs (x : {i & X i}) : set_system {i & X i} :=
+  existT _ _ @ nbhs (projT2 x).
+
+Lemma sigT_nbhsE (i : I) (x : X i) :
+  sigT_nbhs (existT _ i x) = (existT _ _) @ (nbhs x).
+Proof. by done. Qed.
+
+HB.instance Definition _ := hasNbhs.Build {i & X i} sigT_nbhs.
+
+Local Lemma sigT_nbhs_proper x : ProperFilter (sigT_nbhs x).
+Proof. by case: x => i xi; exact: fmap_proper_filter. Qed.
+
+Local Lemma sigT_nbhs_singleton x A : sigT_nbhs x A -> A x.
+Proof. by case: x => ? ? /=; exact: nbhs_singleton. Qed.
+
+Local Lemma sigT_nbhs_nbhs x A: sigT_nbhs x A -> sigT_nbhs x (sigT_nbhs^~ A).
+Proof.
+case: x => i Xi /=.
+rewrite sigT_nbhsE /= nbhsE /= => -[W [oW Wz WlA]].
+by exists W => // x /= Wx; exact/(filterS WlA)/open_nbhs_nbhs.
+Qed.
+
+HB.instance Definition _ := Nbhs_isNbhsTopological.Build {i & X i}
+  sigT_nbhs_proper sigT_nbhs_singleton sigT_nbhs_nbhs.
+
+Lemma existT_continuous (i : I) : continuous (existT X i).
+Proof. by move=> ? ?. Qed.
+
+Lemma existT_open_map (i : I) (A : set (X i)) : open A -> open (existT X i @` A).
+Proof.
+move=> oA; rewrite openE /interior /= => iXi [x Ax <-].
+rewrite /nbhs /= sigT_nbhsE /= nbhs_simpl /=.
+move: oA; rewrite openE => /(_ _ Ax); apply: filterS.
+by move=> z Az; exists z.
+Qed.
+
+Lemma existT_nbhs (i : I) (x : X i) (U : set (X i)) :
+  nbhs x U -> nbhs (existT _ i x) (existT _ i @` U).
+Proof. exact/filterS/preimage_image. Qed.
+
+Lemma sigT_openP (U : set {i & X i}) :
+  open U <-> forall i, open (existT _ i @^-1` U).
+Proof.
+split=> [oU i|?]; first by apply: open_comp=> // y _; exact: existT_continuous.
+rewrite openE => -[i x Uxi].
+by rewrite /interior /nbhs/= sigT_nbhsE; exact: open_nbhs_nbhs.
+Qed.
+
+Lemma sigT_continuous {Z : topologicalType} (f : forall i, X i -> Z) :
+  (forall i, continuous (f i)) -> continuous (sigT_fun f).
+Proof. by move=> ctsf [] i x U nU; apply: existT_continuous; exact: ctsf. Qed.
+
+Lemma sigT_setUE : [set: {i & X i}] = \bigcup_i (existT _ i @` [set: X i]).
+Proof. by rewrite eqEsubset; split => [[i x] _|[]//]; exists i. Qed.
+
+Lemma sigT_compact : finite_set [set: I] -> (forall i, compact [set: X i]) ->
+  compact [set: {i & X i}].
+Proof.
+move=> fsetI cptX; rewrite sigT_setUE -fsbig_setU//.
+apply: big_rec; first exact: compact0.
+move=> i ? _ cptx; apply: compactU => //.
+apply: continuous_compact; last exact: cptX.
+exact/continuous_subspaceT/existT_continuous.
+Qed.
+
+End sigT_topology.

theories/topology_theory/topology.v

@@ -15,3 +15,4 @@ From mathcomp Require Export topology_structure.
 From mathcomp Require Export uniform_structure.
 From mathcomp Require Export weak_topology.
 From mathcomp Require Export one_point_compactification.
+From mathcomp Require Export sigT_topology.