Initial topology induced by a family of functions

CHANGELOG_UNRELEASED.md

@@ -192,6 +192,14 @@
 
 - in `functions.v`:
   + lemmas `zerofctE`, `onefctE`
+- in `initial_topology.v`:
+  + lemmas `cvg_image` `continuous_initial_topology` `bigsetI_open`
+    `initial_fam_continuous` `cvg_init_fam` `cvg_image_init_fam`
+    `continuous_init_fam`
+  + definition `initial_fam_topology`
+  + instance of `Topological` on `initial_fam_topology`
+
+### Changed
 
 - in `functions.v`:
   + lemmas `linfunP`, `linfun_eqP`
@@ -234,6 +242,8 @@
 - in `measurable_structure.v`:
   + lemmas `countable_bigcap_measurable`, `countable_bigcup_measurable`
 
+- in `initial_topology.v`:
+  + lemma `cvg_image` renamed `cvg_initial`
 ### Changed
 
 - in `realsum.v`:

theories/topology_theory/initial_topology.v

@@ -1,6 +1,6 @@
 (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect_compat algebra all_classical.
+From mathcomp Require Import all_ssreflect_compat algebra all_classical finmap.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
 From mathcomp Require Import interval_inference reals topology_structure.
@@ -32,6 +32,10 @@ From mathcomp Require Import pseudometric_structure.
 (*                                This is a subConvexTvsType when V is        *)
 (*                                endowed with a convexTvsType (and when U is *)
 (*                                subLmodType).                               *)
+(*      initial_fam_topology f == initial topology by a family of functions   *)
+(*                              F : (I -> (S -> T).                           *)
+(*                                I must be a pointedType, S a choiceType     *)
+(*                                and T a topologicalType.                    *)
 (* ```                                                                        *)
 (* `initial_topology` is equipped with the structures of:                     *)
 (* - uniform space                                                            *)
@@ -86,21 +90,42 @@ HB.instance Definition _ :=
 Lemma initial_continuous : continuous (f : W -> T).
 Proof. by apply/continuousP => A ?; exists A. Qed.
 
-Lemma cvg_image (F : set_system S) (s : S) :
-  Filter F -> f @` setT = setT ->
-  F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s.
+(* TODO : use image_set_system to be imported from measure theory *)
+Lemma cvg_initial (F : set_system S) (s : S) :
+  Filter F ->
+ ([set f @` A | A in F] : set_system _) --> f s ->  F --> (s : W).
 Proof.
-move=> FF fsurj; split=> [cvFs|cvfFfs].
-  move=> A /initial_continuous [B [Bop Bs sBAf]].
-  have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs.
-  rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB.
-  exact: image_preimage.
+move=> FF cvfFfs.
 move=> A /= [_ [[B Bop <-] Bfs sBfA]].
 have /cvfFfs [C FC fCeB] : nbhs (f s) B by rewrite nbhsE; exists B.
 rewrite nbhs_filterE; apply: filterS FC.
 by apply: subset_trans sBfA; rewrite -fCeB; apply: preimage_image.
 Qed.
 
+Lemma cvg_image (F : set_system S) (s : S) :
+  Filter F -> f @` setT = setT ->
+  F --> (s : W) <-> ([set f @` A | A in F] : set_system _) --> f s.
+Proof.
+move=> FF fsurj; split=> [cvFs|/cvg_initial //].
+move=> A /initial_continuous [B [Bop Bs sBAf]].
+have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs.
+rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB.
+by exact: image_preimage.
+Qed.
+
+Lemma continuous_initial_topology (U : topologicalType) (g : U -> W):
+  continuous g <-> (continuous (f \o g)).
+Proof.
+split => cont x.
+  by apply: (continuous_comp (cont x)); apply: initial_continuous.
+move => A [B/=]; rewrite /initial_topology /= => -[[C] oC fBC] Bgx BA.
+apply: filterS; first by exact: BA.
+rewrite -fBC /nbhs -comp_preimage.
+apply: cont; apply: open_nbhs_nbhs; split => //.
+have : f @` B `<=` C by move => z /= [t]; rewrite -fBC //= => ? <-.
+by apply => /=; exists (g x).
+Qed.
+
 End Initial_Topology.
 (*#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed `initial_open`")]
 Notation wopen := initial_open (only parsing).*)
@@ -264,3 +289,238 @@ Proof.
 move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf.
 exact: open_nbhs_nbhs.
 Qed.
+
+Lemma bigsetI_open (U : topologicalType) (I: Type) (s : seq I) (P : pred I) (f : I -> set U) :
+ (forall i, P i ->  open (f i)) ->  open (\big[setI/setT]_(i<- s | P i) f i).
+Proof.
+move=> Pf. apply: big_ind => //. by apply: openT. exact: openI.
+Qed.
+
+Definition initial_fam_topology {S : Type} {T : Type} {I : pointedType}
+  (F : I -> (S -> T)) : Type := S.
+
+Section initial_fam_topology.
+Variable (S : choiceType) (T : topologicalType) (I : pointedType)  (F : I -> (S -> T)).
+Local Notation W := (initial_fam_topology F).
+
+Definition init_fam_subbase := [set O | exists i, exists2 A, (O = (F i) @^-1` A) & open A  ].
+
+HB.instance Definition _ := Choice.on W.
+HB.instance Definition _ := isSubBaseTopological.Build W init_fam_subbase id.
+
+Lemma initial_fam_continuous : forall i, continuous ((F i) : W -> T).
+Proof. move=> i; apply/continuousP => A oA.
+exists [set  (F i @^-1` A)]; last by rewrite bigcup_set1.
+move=> /= O /= -> /= . rewrite /finI_from /=.
+exists [fset  (F i @^-1` A)]%fset; last by rewrite set_fset1 bigcap_set1.
+by move => ? /=; rewrite inE; move/eqP ->; rewrite /init_fam_subbase in_setE /=; exists i; exists A.
+Qed.
+
+Lemma cvg_init_fam (G : set_system W) (s : W) :
+  Filter G ->
+  (forall i, ([set (F i)  @` A | A in G] : set_system _) --> F i s) ->  G --> (s : W) .
+Proof.
+move=> FG cvfFfs.
+move => A -[] /=.
+move => _  [[]] H Hop <- [B HB Bs] sBfA/=; rewrite nbhs_filterE.
+have BA : B `<=` A.
+  apply: subset_trans; last by exact: sBfA.
+  by move => y /= By; exists B =>//.
+apply: (@filterS _ G _  B) => //; move /(_ B HB): Hop  => /= [] /= C CO Bcap.
+(* can´t  apply fsubsetP or subsetP on CO  to obtain the following *)
+have Ci : forall (O : set S) , O \in C ->
+  exists i : I, exists2 A : set T, O = F i @^-1` A & open A.
+  by move => O /CO /set_mem //=.
+move => {CO} {sBfA} {BA} {A}.
+have GC: forall (O : set S), O \in C -> G O.
+  move => O OC; move: (OC) => /Ci [i [D OD openD]].
+  have : nbhs (F i s) D.
+    rewrite nbhsE; exists D => //; split => //.
+    by move: Bs; rewrite -Bcap /bigcap /= => /(_ O OC); rewrite OD.
+  move/(cvfFfs i D); rewrite nbhs_filterE => //= [[O']] GO' /= O'D.
+  apply: filterS; last by exact: GO'.
+  by rewrite OD -O'D; apply: preimage_image.
+by rewrite -Bcap; apply: filter_bigI => /= O OC; apply: GC.
+Qed.
+
+Lemma cvg_image_init_fam (G : set_system W) (s : W) :
+  Filter G -> (forall i, (F i) @` setT = setT) ->
+  G --> (s : W) <-> (forall i, ([set (F i)  @` A | A in G] : set_system _) --> F i s).
+Proof.
+move=> FG fsurj; split=> [cvFs|/cvg_init_fam] //.
+move=> i A /initial_fam_continuous [B [//= Bop Bs sBAf]].
+have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs.
+rewrite nbhs_simpl; exists ((F i) @^-1` A); first exact: filterS FB.
+by exact: image_preimage.
+Qed.
+
+Lemma continuous_init_fam (V : topologicalType) (f : V -> W) :
+ (forall i, continuous ((F i) \o (f : V -> S))) <-> continuous f.
+Proof.
+split=> cont; last first.
+  move=> i x; apply: (continuous_comp (cont x)).
+  by apply: initial_fam_continuous.
+move => x A; rewrite /nbhs /= => -[/= B] [Bfrom Bfx BA] /=.
+apply: filterS; first by apply: preimage_subset BA.
+apply: open_nbhs_nbhs; split => //.
+have:= Bfrom => -[] C CO <-; rewrite preimage_bigcup.
+apply: bigcup_open => i /CO [] /= D Dsub <-; rewrite preimage_bigcap /=.
+rewrite bigcap_fset /= big_seq; apply: bigsetI_open => /= E /Dsub.
+move/set_mem; rewrite /init_fam_subbase /= => -[j [A0 -> oA]].
+rewrite -comp_preimage.
+by have /continuousP := cont j; apply.
+Qed.
+
+End initial_fam_topology.
+
+
+HB.instance Definition _ (S : pointedType) (T : topologicalType)  (I : pointedType)  (F : I -> (S -> T)) :=
+  Pointed.on (initial_fam_topology F).
+HB.instance Definition _ (S : pointedType) (T : topologicalType)  (I : pointedType)  (F : I -> (S -> T)) :=
+  Filtered.on (initial_fam_topology F).
+
+
+Section initial_fam_topology_uniform.
+
+Local Open Scope relation_scope.
+Variable (S : choiceType) (T : uniformType) (I : pointedType) (F : I -> (S -> T)).
+
+Let W := initial_fam_topology F.
+
+Definition initial_fam_ent : set_system (W * W) :=
+  filter_from (@entourage T) (fun V => \bigcap_i (map_pair (F i))@^-1` V).
+
+Let initial_fam_ent_filter : Filter initial_fam_ent.
+Proof.
+apply: filter_from_filter; first by exists setT; exact: entourageT.
+move=> P Q eP eQ; exists (P `&` Q); first by exact: filterI.
+by move=> [a b]; rewrite /bigcap /= => H; split => i _; have [] := H i.
+Qed.
+
+Let initial_fam_ent_refl A : initial_fam_ent A -> diagonal `<=` A.
+Proof.
+move=> [B ? sBA] [x y]/diagonalP ->; apply/sBA; rewrite /bigcap /= => i _.
+exact: entourage_refl.
+Qed.
+
+Let initial_fam_ent_inv A : initial_fam_ent A -> initial_fam_ent A^-1.
+Proof.
+move=> [B ? sBA]; exists B^-1; first exact: entourage_inv.
+by move=> ??; exact/sBA.
+Qed.
+
+Let initial_fam_ent_split A : initial_fam_ent A -> exists2 B, initial_fam_ent B & B \; B `<=` A.
+Proof.
+move=> [B entB sBA]; have : exists C, entourage C /\ C \; C `<=` B.
+  exact/exists2P/entourage_split_ex.
+case=> C [entC CsubB].
+exists (\bigcap_i map_pair (F i) @^-1` C); first by exists C.
+case=> x y [a /= P Q]. apply/sBA => i /= _.
+apply: CsubB. exists ((F i) a) => /=; first by apply: P.
+by apply: Q.
+Qed.
+
+Let initial_fam_ent_nbhs : nbhs = nbhs_ initial_fam_ent.
+Proof.
+rewrite predeq2E => x V; split.
+  case=> [P [[/= B Q <-] Bx BsubV]].
+  have: nbhs ( x)  (\bigcup_(i in B) i).
+    by apply: open_nbhs_nbhs; split => //; exists B.
+(*  move/nbhsP. [W ? WsubB]; exists ((map_pair f) @^-1` W); first by exists W.
+  by move=> ? ?; exact/BsubV/WsubB.
+case=> W [V' entV' V'subW] /filterS; apply.
+have : nbhs (f x) (xsection V' (f x)) by apply/nbhsP; exists V'.
+rewrite (@nbhsE U) => [[O [openU Ofx Osub]]].
+(exists (f @^-1` O); repeat split => //); first by exists O => //.
+by move=> w ?; apply/mem_set; apply: V'subW; apply/set_mem; exact: Osub.
+Qed.*)
+Admitted.
+
+HB.instance Definition _ := @Nbhs_isUniform.Build (initial_fam_topology F)
+  initial_fam_ent initial_fam_ent_filter initial_fam_ent_refl initial_fam_ent_inv
+  initial_fam_ent_split initial_fam_ent_nbhs.
+End initial_fam_topology_uniform.
+
+
+From mathcomp Require Import supremum_topology.
+
+Section initial_fam_Topology_with_sup.
+Variable (S : choiceType)  (I : pointedType) (T : I -> topologicalType)  (F : forall i :I, (S -> T i)).
+
+Definition Fc := fun i => Topological.class (initial_topology (F i)).
+
+Definition initial_sup_topology := (sup_topology Fc).
+
+Local Notation W := (initial_sup_topology).
+
+Lemma initial_sup_continuous : forall i, continuous ((F i) : W -> T i).
+Proof. move=> i; apply/continuousP => A oA.
+exists [set  (F i @^-1` A)]; last by rewrite bigcup_set1.
+move=> /= O /= -> /= . rewrite /finI_from /=.
+exists [fset  (F i @^-1` A)]%fset; last by rewrite set_fset1 bigcap_set1.
+by move => ? /=; rewrite inE; move/eqP ->; apply/mem_set; exists i => //; exists A.
+Qed.
+
+Lemma cvg_init_sup (G : set_system W) (s : W) :
+  Filter G ->
+  (forall i, ([set (F i)  @` A | A in G] : set_system _) --> F i s) ->  G --> (s : W) .
+Proof.
+move=> FG cvfFfs.
+move => A -[] /=.
+move => _  [[]] H Hop <- [B HB Bs] sBfA/=; rewrite nbhs_filterE.
+have BA : B `<=` A.
+  apply: subset_trans; last by exact: sBfA.
+  by move => y /= By; exists B =>//.
+apply: (@filterS _ G _  B) => //; move /(_ B HB): Hop  => /= [] /= C CO Bcap.
+(* can´t  apply fsubsetP or subsetP on CO  to obtain the following *)
+have Ci : forall (O : set S) , O \in C ->
+  exists i : I, exists2 A : set (T i), O = F i @^-1` A & open A.
+  by move => O /CO /set_mem //= [i] _ -[O' oO' <-]; exists i; exists O'.
+move => {CO} {sBfA} {BA} {A}.
+have GC: forall (O : set S), O \in C -> G O.
+  move => O OC; move: (OC) => /Ci [i [D OD openD]].
+  have : nbhs (F i s) D.
+    rewrite nbhsE; exists D => //; split => //.
+    by move: Bs; rewrite -Bcap /bigcap /= => /(_ O OC); rewrite OD.
+  move/(cvfFfs i D); rewrite nbhs_filterE => //= [[O']] GO' /= O'D.
+  apply: filterS; last by exact: GO'.
+  by rewrite OD -O'D; apply: preimage_image.
+by rewrite -Bcap; apply: filter_bigI => /= O OC; apply: GC.
+Qed.
+
+Lemma cvg_image_init_sup (G : set_system W) (s : W) :
+  Filter G -> (forall i, (F i) @` setT = setT) ->
+  G --> (s : W) <-> (forall i, ([set (F i)  @` A | A in G] : set_system _) --> F i s).
+Proof.
+move=> FG fsurj; split=> [cvFs|/cvg_init_sup] //.
+move=> i A /initial_sup_continuous [B [//= Bop Bs sBAf]].
+have /cvFs FB : nbhs (s : W) B by apply: open_nbhs_nbhs.
+rewrite nbhs_simpl; exists ((F i) @^-1` A); first exact: filterS FB.
+by exact: image_preimage.
+Qed.
+
+Lemma continuous_init_sup (V : topologicalType) (f : V -> W) :
+ (forall i, continuous ((F i) \o (f : V -> S))) <-> continuous f.
+Proof.
+split=> cont; last first.
+  move=> i x; apply: (continuous_comp (cont x)).
+  by apply: initial_sup_continuous.
+move => x A; rewrite /nbhs /= => -[/= B] [Bfrom Bfx BA] /=.
+apply: filterS; first by apply: preimage_subset BA.
+apply: open_nbhs_nbhs; split => //.
+have:= Bfrom => -[] C CO <-; rewrite preimage_bigcup.
+apply: bigcup_open => i /CO [] /= D Dsub <-; rewrite preimage_bigcap /=.
+rewrite bigcap_fset /= big_seq; apply: bigsetI_open => /= E /Dsub.
+move/set_mem => -[j _ [E' oE' <-]]; rewrite -comp_preimage.
+by have /continuousP := cont j; apply.
+Qed.
+
+End initial_fam_Topology_with_sup.
+
+Section initial_fam_sup_uniform.
+Variable (S : choiceType)  (I : pointedType) (T : I -> uniformType)  (F : forall i :I, (S -> T i)).
+
+Local Notation W := (@initial_sup_topology S I T F).
+
+Fail Check (W : uniformType).
+End initial_fam_sup_uniform.

theories/topology_theory/topology_structure.v

@@ -496,6 +496,10 @@ HB.instance Definition _ := Nbhs_isTopological.Build T
 
 HB.end.
 
+Definition open_from (T : Type) (I : Type) (D : set I) (b : I -> set T)
+:= [set \bigcup_(i in D') b i | D' in subset^~ D].
+
+
 (** Topology defined by a base of open sets *)
 
 HB.factory Record isBaseTopological T & Choice T := {
@@ -509,7 +513,7 @@ HB.factory Record isBaseTopological T & Choice T := {
 
 HB.builders Context T & isBaseTopological T.
 
-Definition open_from := [set \bigcup_(i in D') b i | D' in subset^~ D].
+Local Notation open_from := (open_from D b).
 
 Let open_fromT : open_from setT.
 Proof. exists D => //; exact: b_cover. Qed.