From e1606d629b37e4e06f44b574173a1f54dcdb456b Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 14:45:55 +0900 Subject: [PATCH 1/2] 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 6661159148..b35c82075f 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 c1fab2fcde9a54e06ecf67c02a2c3c683101772f Mon Sep 17 00:00:00 2001 From: mkerjean Date: Sun, 21 Jun 2026 15:01:23 +0900 Subject: [PATCH 2/2] changelog --- CHANGELOG_UNRELEASED.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0023dbb5e0..e267aa7ff0 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -131,6 +131,13 @@ - in `lebesgue_stieltjes_measure.v`: + definition `lebesgue_display` +- 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 - moved from `measurable_structure.v` to `classical_sets.v`: @@ -162,6 +169,8 @@ - new files `signed_measure.v` and `radon_nikodym.v` + with the contents of `charge.v` (deprecated) +- in `initial_topology.v`: + + lemma `cvg_image` renamed `cvg_initial` ### Changed - moved from `measurable_structure.v` to `classical_sets.v`: