From 97758ed1ff6295f99c35a168e17fce1ea2aa85e6 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 14:45:55 +0900 Subject: [PATCH 1/5] initial_topology --- theories/topology_theory/initial_topology.v | 138 ++++++++++++++++-- theories/topology_theory/topology_structure.v | 6 +- 2 files changed, 134 insertions(+), 10 deletions(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 943c1210cb..f7a4cc6504 100644 --- a/theories/topology_theory/initial_topology.v +++ b/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,45 @@ 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. + +(* TODO: shorten this proof*) +Lemma continuous_initial_topology (U : topologicalType) (g : U -> W): + continuous g <-> (continuous (f \o g)). +Proof. +split => cont x. + apply: continuous_comp; first by apply: cont. + by apply: initial_continuous. +move => A [B/=]; rewrite /initial_topology /= => -[[C] oC fBC] Bgx BA. +apply: filterS; first by exact: BA. +rewrite -fBC /nbhs /=. +rewrite -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 +292,95 @@ 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; first by apply: cont. + 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). + + +(* TODO : uniform and pseudometric structure for initial fam topology, tvs structure for initial and initial_fam topology *) + + diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v index a6170e44b1..3e2fa266a1 100644 --- a/theories/topology_theory/topology_structure.v +++ b/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. From c0f302d05e298c3f79e28848e2464908bc4ebf1f Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 15:01:23 +0900 Subject: [PATCH 2/5] changelog --- CHANGELOG_UNRELEASED.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2d85fdc0a5..423e045c51 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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`: From 9973a6d1fcf96e5a44b48ebe8cb33b9e0cfa2d23 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Thu, 2 Jul 2026 11:08:00 +0900 Subject: [PATCH 3/5] clean --- theories/topology_theory/initial_topology.v | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index f7a4cc6504..7be57badf5 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -113,7 +113,6 @@ rewrite nbhs_simpl; exists (f @^-1` A); first exact: filterS FB. by exact: image_preimage. Qed. -(* TODO: shorten this proof*) Lemma continuous_initial_topology (U : topologicalType) (g : U -> W): continuous g <-> (continuous (f \o g)). Proof. @@ -122,8 +121,7 @@ split => cont x. by apply: initial_continuous. move => A [B/=]; rewrite /initial_topology /= => -[[C] oC fBC] Bgx BA. apply: filterS; first by exact: BA. -rewrite -fBC /nbhs /=. -rewrite -comp_preimage. +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). @@ -382,5 +380,3 @@ HB.instance Definition _ (S : pointedType) (T : topologicalType) (I : pointedTy (* TODO : uniform and pseudometric structure for initial fam topology, tvs structure for initial and initial_fam topology *) - - From 8decc79f67d770fcc5afaa877b226190b8c65362 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 8 Jul 2026 12:40:35 +0900 Subject: [PATCH 4/5] initial sup topology wip --- theories/topology_theory/initial_topology.v | 151 +++++++++++++++++++- 1 file changed, 148 insertions(+), 3 deletions(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 7be57badf5..93a4f0e58b 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -300,7 +300,7 @@ Qed. Definition initial_fam_topology {S : Type} {T : Type} {I : pointedType} (F : I -> (S -> T)) : Type := S. -Section initial_fam_Topology. +Section initial_fam_topology. Variable (S : choiceType) (T : topologicalType) (I : pointedType) (F : I -> (S -> T)). Local Notation W := (initial_fam_topology F). @@ -372,11 +372,156 @@ rewrite -comp_preimage. by have /continuousP := cont j; apply. Qed. -End initial_fam_Topology. +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; first by apply: cont. + 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). -(* TODO : uniform and pseudometric structure for initial fam topology, tvs structure for initial and initial_fam topology *) +Fail Check (W : uniformType). +End initial_fam_sup_uniform. From 33cc95b090786709edee6d4d3def170a3a696b74 Mon Sep 17 00:00:00 2001 From: mkerjean Date: Wed, 8 Jul 2026 14:30:03 +0900 Subject: [PATCH 5/5] fix CI mc-master --- theories/topology_theory/initial_topology.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v index 93a4f0e58b..2513c8c780 100644 --- a/theories/topology_theory/initial_topology.v +++ b/theories/topology_theory/initial_topology.v @@ -117,8 +117,7 @@ Lemma continuous_initial_topology (U : topologicalType) (g : U -> W): continuous g <-> (continuous (f \o g)). Proof. split => cont x. - apply: continuous_comp; first by apply: cont. - by apply: initial_continuous. + 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. @@ -359,8 +358,8 @@ 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; first by apply: cont. - apply: initial_fam_continuous. + 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 => //. @@ -504,8 +503,8 @@ 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; first by apply: cont. - apply: initial_sup_continuous. + 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 => //.