diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 03c90f7b0..31ab6ca7b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`, diff --git a/_CoqProject b/_CoqProject index 0c3ff3b81..4a9bd2415 100644 --- a/_CoqProject +++ b/_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 diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 2bb8f9f86..4e1150553 100644 --- a/classical/mathcomp_extra.v +++ b/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)). diff --git a/theories/Make b/theories/Make index 95312be86..cf786d30d 100644 --- a/theories/Make +++ b/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 diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index 4f54e83e1..ff6f7702c 100644 --- a/theories/separation_axioms.v +++ b/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. diff --git a/theories/topology_theory/sigT_topology.v b/theories/topology_theory/sigT_topology.v new file mode 100644 index 000000000..c0b779117 --- /dev/null +++ b/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. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 357618420..25460c770 100644 --- a/theories/topology_theory/topology.v +++ b/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.