From f75d6499eee06e6fd5912217746576e836980a84 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 4 Feb 2026 11:44:22 +0900 Subject: [PATCH] rename `weak_topology` -> `initial_topology` Co-authored-by: Marie Kerjean --- CHANGELOG_UNRELEASED.md | 30 ++- _CoqProject | 1 + theories/Make | 1 + theories/function_spaces.v | 66 ++--- theories/homotopy_theory/continuous_path.v | 4 +- theories/normedtype_theory/urysohn.v | 12 +- theories/topology_theory/initial_topology.v | 235 ++++++++++++++++++ .../one_point_compactification.v | 9 +- theories/topology_theory/subspace_topology.v | 10 +- theories/topology_theory/subtype_topology.v | 12 +- theories/topology_theory/topology.v | 2 +- theories/topology_theory/weak_topology.v | 220 +--------------- 12 files changed, 327 insertions(+), 275 deletions(-) create mode 100644 theories/topology_theory/initial_topology.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0d911f46cb..c575dcdc03 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -17,16 +17,44 @@ + lemma `Rintegral_cst` (does not use `cst` anymore) ### Renamed -- in set_interval.v +- in `set_interval.v`: + `itv_is_ray` -> `itv_is_open_unbounded` + `itv_is_bd_open` -> `itv_is_oo` +- `weak_topology.v` -> `initial_topology.v` + + `weak_topology` -> `initial_topology` + + `weak_continuous` -> `initial_continuous` + + `weak_ent` -> `initial_ent` + + `weak_ball` -> `initial_ball` + + `weak_ballE` -> `initial_ballE` + + `open_order_weak` -> `open_order_initial` + + `continuous_comp_weak` -> `continuous_comp_initial` + +- in `one_point_compactification.v`: + + `one_point_compactification_weak_topology` -> + `one_point_compactification_initial_topology` + +- in `subspace_topology.v`: + + `weak_subspace_open` -> `initial_subspace_open` + +- in `functions_spaces.v`: + + `weak_sep_cvg` -> `initial_sep_cvg` + + `weak_sep_nbhsE` -> `initial_sep_nbhsE` + + `weak_sep_openE` -> `initial_sep_openE` + + `join_product_weak` -> `join_product_initial` + ### Generalized ### Deprecated ### Removed +- in `weak_topology.v`: + + lemmas `weak_ent_filter`, `weak_ent_refl`, `weak_ent_inv`, + `weak_ent_split`, `weak_ent_nbhs`, `weak_pseudo_metric_ball_center`, + `weak_pseudo_metric_entourageE` + (now `Let`'s in `initial_topology.v`) + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index 3fbb3d0b8c..f5551604f7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -58,6 +58,7 @@ theories/topology_theory/supremum_topology.v theories/topology_theory/topology_structure.v theories/topology_theory/uniform_structure.v theories/topology_theory/weak_topology.v +theories/topology_theory/initial_topology.v theories/topology_theory/num_topology.v theories/topology_theory/quotient_topology.v theories/topology_theory/one_point_compactification.v diff --git a/theories/Make b/theories/Make index 960f2f546d..2d727dad6d 100644 --- a/theories/Make +++ b/theories/Make @@ -25,6 +25,7 @@ topology_theory/supremum_topology.v topology_theory/topology_structure.v topology_theory/uniform_structure.v topology_theory/weak_topology.v +topology_theory/initial_topology.v topology_theory/num_topology.v topology_theory/quotient_topology.v topology_theory/one_point_compactification.v diff --git a/theories/function_spaces.v b/theories/function_spaces.v index a20bb345d3..08db6e606c 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -126,18 +126,18 @@ Variable I : Type. Definition product_topology_def (T : I -> topologicalType) := sup_topology (fun i => Topological.class - (weak_topology (fun f : (forall i, T i) => f i))). + (initial_topology (fun f : (forall i, T i) => f i))). HB.instance Definition _ (T : I -> topologicalType) := Topological.copy (prod_topology T) (product_topology_def T). HB.instance Definition _ (T : I -> uniformType) := Uniform.copy (prod_topology T) - (sup_topology (fun i => Uniform.class (weak_topology (@proj _ T i)))). + (sup_topology (fun i => Uniform.class (initial_topology (@proj _ T i)))). HB.instance Definition _ (R : realType) (Ii : countType) (Tc : Ii -> pseudoMetricType R) := PseudoMetric.copy (prod_topology Tc) - (sup_pseudometric (fun i => PseudoMetric.class (weak_topology (@proj _ Tc i))) + (sup_pseudometric (fun i => PseudoMetric.class (initial_topology (@proj _ Tc i))) (countableP _)). End Product_Topology. @@ -156,12 +156,12 @@ HB.instance Definition _ (U : Type) (T : U -> uniformType) := HB.instance Definition _ (U T : topologicalType) := Topological.copy (continuousType U T) - (weak_topology (id : continuousType U T -> (U -> T))). + (initial_topology (id : continuousType U T -> (U -> T))). HB.instance Definition _ (U : topologicalType) (T : uniformType) := Uniform.copy (continuousType U T) - (weak_topology (id : continuousType U T -> (U -> T))). + (initial_topology (id : continuousType U T -> (U -> T))). End ArrowAsProduct. @@ -328,58 +328,58 @@ Definition separate_points_from_closed := forall (U : set T) x, Hypothesis sepf : separate_points_from_closed. Hypothesis ctsf : forall i, continuous (f_ i). -Let weakT : topologicalType := - sup_topology (fun i => Topological.on (weak_topology (f_ i))). +Let initialT : topologicalType := + sup_topology (fun i => Topological.on (initial_topology (f_ i))). Let PU : topologicalType := prod_topology U_. -Local Notation sup_open := (@open weakT). -Local Notation "'weak_open' i" := (@open weakT) (at level 0). +Local Notation sup_open := (@open initialT). +Local Notation "'weak_open' i" := (@open initialT) (at level 0). Local Notation natural_open := (@open T). -Lemma weak_sep_cvg (F : set_system T) (x : T) : - Filter F -> (F --> (x : T)) <-> (F --> (x : weakT)). +Lemma initial_sep_cvg (F : set_system T) (x : T) : + Filter F -> (F --> (x : T)) <-> (F --> (x : initialT)). Proof. move=> FF; split. move=> FTx; apply/cvg_sup => i U. - have /= -> := @nbhsE (weak_topology (f_ i)) x. + have /= -> := @nbhsE (initial_topology (f_ i)) x. case=> B [[C oC <- ?]] /filterS; apply; apply: FTx; rewrite /= nbhsE. by exists (f_ i @^-1` C) => //; split => //; exact: open_comp. move/cvg_sup => wiFx U; rewrite /= nbhs_simpl nbhsE => [[B [oB ?]]]. move/filterS; apply; have [//|i nclfix] := @sepf _ x (open_closedC oB). -apply: (wiFx i); have /= -> := @nbhsE (weak_topology (f_ i)) x. +apply: (wiFx i); have /= -> := @nbhsE (initial_topology (f_ i)) x. exists (f_ i @^-1` (~` closure [set f_ i x | x in ~` B])); [split=>//|]. apply: open_comp; last by rewrite ?openC//; exact: closed_closure. - by move=> + _; exact: (@weak_continuous _ _ (f_ i)). + by move=> + _; exact: (@initial_continuous _ _ (f_ i)). rewrite -interiorC interiorEbigcup preimage_bigcup => z [V [oV]] VnB => /VnB. by move/forall2NP => /(_ z) [] // /contrapT. Qed. -Lemma weak_sep_nbhsE x : @nbhs T T x = @nbhs T weakT x. +Lemma initial_sep_nbhsE x : @nbhs T T x = @nbhs T initialT x. Proof. rewrite predeqE => U; split; move: U. - by have P := weak_sep_cvg x (nbhs_filter (x : weakT)); exact/P. -by have P := weak_sep_cvg x (nbhs_filter (x : T)); exact/P. + by have P := initial_sep_cvg x (nbhs_filter (x : initialT)); exact/P. +by have P := initial_sep_cvg x (nbhs_filter (x : T)); exact/P. Qed. -Lemma weak_sep_openE : @open T = @open weakT. +Lemma initial_sep_openE : @open T = @open initialT. Proof. rewrite predeqE => A; rewrite ?openE /interior. -by split => + z => /(_ z); rewrite weak_sep_nbhsE. +by split => + z => /(_ z); rewrite initial_sep_nbhsE. Qed. Definition join_product (x : T) : PU := f_ ^~ x. Lemma join_product_continuous : continuous join_product. Proof. -suff : continuous (join_product : weakT -> PU). - by move=> cts x U => /cts; rewrite nbhs_simpl /= -weak_sep_nbhsE. -move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : weakT)). -move=> i; move: x; apply/(@continuousP _ (weak_topology (@^~ i))) => A [B ? E]. +suff : continuous (join_product : initialT -> PU). + by move=> cts x U => /cts; rewrite nbhs_simpl /= -initial_sep_nbhsE. +move=> x; apply/cvg_sup; first exact/fmap_filter/(nbhs_filter (x : initialT)). +move=> i; move: x; apply/(@continuousP _ (initial_topology (@^~ i))) => A [B ? E]. rewrite -E (_ : @^~ i = proj i) //. have -> : join_product @^-1` (proj i @^-1` B) = f_ i @^-1` B by []. apply: open_comp => // + _; rewrite /cvg_to => x U. -by rewrite nbhs_simpl /= -weak_sep_nbhsE; move: x U; exact: ctsf. +by rewrite nbhs_simpl /= -initial_sep_nbhsE; move: x U; exact: ctsf. Qed. Local Notation prod_open := (@open (subspace (range join_product))). @@ -411,8 +411,8 @@ apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->. by apply: subset_closure; exists y. Qed. -Lemma join_product_weak : set_inj [set: T] join_product -> - @open T = @open (weak_topology join_product). +Lemma join_product_initial : set_inj [set: T] join_product -> + @open T = @open (initial_topology join_product). Proof. move=> inj; rewrite predeqE => U; split; first last. by move=> [V ? <-]; apply: open_comp => // + _; exact: join_product_continuous. @@ -559,12 +559,12 @@ HB.instance Definition _ (U : choiceType) (R : numFieldType) HB.instance Definition _ (U : topologicalType) (T : uniformType) := Uniform.copy (continuousType U T) - (weak_topology (id : continuousType U T -> (U -> T))). + (initial_topology (id : continuousType U T -> (U -> T))). HB.instance Definition _ (U : topologicalType) (R : realType) (T : pseudoMetricType R) := PseudoMetric.on - (weak_topology (id : continuousType U T -> (U -> T))). + (initial_topology (id : continuousType U T -> (U -> T))). End ArrowAsUniformType. @@ -632,7 +632,7 @@ Definition sigL_arrow {U : choiceType} (A : set U) (V : uniformType) : (U -> V) -> arrow_uniform_type A V := @sigL _ V A. HB.instance Definition _ (U : choiceType) (A : set U) (V : uniformType) := - Uniform.copy {uniform` A -> V} (weak_topology (@sigL_arrow _ A V)). + Uniform.copy {uniform` A -> V} (initial_topology (@sigL_arrow _ A V)). Section RestrictedUniformTopology. Context {U : choiceType} (A : set U) {V : uniformType} . @@ -1068,8 +1068,8 @@ HB.instance Definition _ (U : topologicalType) (V : topologicalType) := Topological.copy (U -> V) {compact-open, U -> V}. HB.instance Definition _ (U : topologicalType) (V : topologicalType) := - Topological.copy (continuousType U V) - (weak_topology (id : (continuousType U V) -> (U -> V)) ). + Topological.copy (continuousType U V) + (initial_topology (id : (continuousType U V) -> (U -> V)) ). End ArrowAsCompactOpen. Definition compactly_in {U : topologicalType} (A : set U) := @@ -1606,7 +1606,7 @@ Lemma eval_continuous {X Y : topologicalType} : locally_compact [set: X] -> regular_space X -> continuous (@eval X Y). Proof. move=> lcX rsX; apply: continuous_uncurry_regular => //. - exact: weak_continuous. + exact: initial_continuous. by move=> ?; exact: cts_fun. Qed. @@ -1616,7 +1616,7 @@ Lemma compose_continuous {X Y Z : topologicalType} : continuous (uncurry (comp : continuousType Y Z -> continuousType X Y -> continuousType X Z)). Proof. -move=> lX rX lY rY; apply: continuous_comp_weak. +move=> lX rX lY rY; apply: continuous_comp_initial. set F := _ \o _. rewrite -[F]uncurryK; apply: continuous_curry_fun. pose g := uncurry F \o prodAr \o swap; rewrite /= in g *. diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index e66a3a4d93..c5df28f3e6 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/theories/homotopy_theory/continuous_path.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. @@ -60,7 +60,7 @@ HB.instance Definition _ {i : bpTopologicalType} HB.instance Definition _ {i : bpTopologicalType} {T : topologicalType} (x y : T) := Topological.copy {path i from x to y} - (@weak_topology {path i from x to y} {compact-open, i -> T} id). + (@initial_topology {path i from x to y} {compact-open, i -> T} id). Section path_eq. Context {T : topologicalType} {i : bpTopologicalType} (x y : T). diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index 116662c57b..817fee1944 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -595,7 +595,7 @@ split; first do [move=> ?; exists (Urysohn A B); split]. - exact: Urysohn_sub0. - exact: Urysohn_sub1. case=> f [ctsf f01 fA0 fB1]. -pose T' : uniformType := weak_topology f. +pose T' : uniformType := initial_topology f. exists (Uniform.class T'), ([set xy | ball (f xy.1) 1 (f xy.2)]); split. - exists [set xy | ball xy.1 1 xy.2]; last by case. by rewrite -entourage_ballE; exists 1 => //=. @@ -703,7 +703,7 @@ Context {R : realType} {X : topologicalType}. Hypothesis crs : completely_regular_space X. Let X' : uniformType := @sup_topology X {f : X -> R | continuous f} - (fun f => Uniform.class (weak_topology (projT1 f))). + (fun f => Uniform.class (initial_topology (projT1 f))). Let completely_regular_nbhsE : @nbhs X X = nbhs_ (@entourage X'). Proof. @@ -728,7 +728,7 @@ exists E; first last. by apply: fU1; exists z. move=> r /= [_]; apply => /=. pose f' : {classic {f : X -> R | continuous f}} := exist _ f ctsf. -suff /asboolP entE : @entourage (weak_topology f) (f', E).2. +suff /asboolP entE : @entourage (initial_topology f) (f', E).2. by exists (exist _ (f', E) entE). exists (fun pq => ball pq.1 1 pq.2) => //=. by rewrite /entourage /=; exists 1 => /=. @@ -774,9 +774,11 @@ HB.instance Definition _ := Uniform.copy opc (@completely_regular_uniformity.type R _ one_point_compactification_completely_reg). -Let X' := @weak_topology X opc Some. +Let X' := @initial_topology X opc Some. Lemma nbhs_one_point_compactification_weakE : @nbhs X X = nbhs_ (@entourage X'). -Proof. by rewrite nbhs_entourageE one_point_compactification_weak_topology. Qed. +Proof. +by rewrite nbhs_entourageE one_point_compactification_initial_topology. +Qed. #[local, non_forgetful_inheritance] HB.instance Definition _ := @Nbhs_isUniform.Build diff --git a/theories/topology_theory/initial_topology.v b/theories/topology_theory/initial_topology.v new file mode 100644 index 0000000000..8854b41bf4 --- /dev/null +++ b/theories/topology_theory/initial_topology.v @@ -0,0 +1,235 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. +From mathcomp Require Import all_ssreflect all_algebra all_classical. +#[warning="-warn-library-file-internal-analysis"] +From mathcomp Require Import unstable. +From mathcomp Require Import interval_inference reals topology_structure. +From mathcomp Require Import uniform_structure order_topology. +From mathcomp Require Import pseudometric_structure. + +(**md**************************************************************************) +(* # Initial topology *) +(* *) +(* This file defines the initial topology for $S$ by a function $f$ whose *) +(* domain is $S$. This topology is also known as initial topology on $S$ with *) +(* respect to $f$. *) +(* *) +(* NB: Before version 1.16.0, the initial topology was called the weak *) +(* topology. Though in some literature it can be called that way, we reserve *) +(* "weak topology" for the topology induced on a topological vector space by *) +(* its dual. *) +(* *) +(* ``` *) +(* initial_topology f == initial topology by a function f : S -> T on S *) +(* S must be a choiceType and T a topologicalType. *) +(* ``` *) +(* `initial_topology` is equipped with the structures of: *) +(* - uniform space *) +(* - pseudometric space (the metric space for initial topologies) *) +(******************************************************************************) + +Import Order.TTheory GRing.Theory Num.Theory. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +Definition initial_topology {S : Type} {T : Type} + (f : S -> T) : Type := S. + +Section Initial_Topology. +Variable (S : choiceType) (T : topologicalType) (f : S -> T). +Local Notation W := (initial_topology f). + +Definition wopen := [set f @^-1` A | A in open]. + +Local Lemma wopT : wopen [set: W]. +Proof. by exists setT => //; apply: openT. Qed. + +Local Lemma wopI (A B : set W) : wopen A -> wopen B -> wopen (A `&` B). +Proof. +by move=> [C Cop <-] [D Dop <-]; exists (C `&` D) => //; apply: openI. +Qed. + +Local Lemma wop_bigU (I : Type) (g : I -> set W) : + (forall i, wopen (g i)) -> wopen (\bigcup_i g i). +Proof. +move=> gop. +set opi := fun i => [set Ui | open Ui /\ g i = f @^-1` Ui]. +exists (\bigcup_i get (opi i)). + apply: bigcup_open => i. + by have /getPex [] : exists U, opi i U by have [U] := gop i; exists U. +have g_preim i : g i = f @^-1` (get (opi i)). + by have /getPex [] : exists U, opi i U by have [U] := gop i; exists U. +rewrite predeqE => s; split=> [[i _]|[i _]]; last by rewrite g_preim; exists i. +by rewrite -[_ _]/((f @^-1` _) _) -g_preim; exists i. +Qed. + +HB.instance Definition _ := Choice.on W. +HB.instance Definition _ := + isOpenTopological.Build W wopT wopI wop_bigU. + +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. +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=> 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. + +End Initial_Topology. + +HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) := + Pointed.on (initial_topology f). + +Section initial_uniform. +Local Open Scope relation_scope. +Variable (pS : choiceType) (U : uniformType) (f : pS -> U). + +Let S := initial_topology f. + +Definition initial_ent : set_system (S * S) := + filter_from (@entourage U) (fun V => (map_pair f)@^-1` V). + +Let initial_ent_filter : Filter initial_ent. +Proof. +apply: filter_from_filter; first by exists setT; exact: entourageT. +by move=> P Q ??; (exists (P `&` Q); first exact: filterI) => ?. +Qed. + +Let initial_ent_refl A : initial_ent A -> diagonal `<=` A. +Proof. +by move=> [B ? sBA] [x y]/diagonalP ->; apply/sBA; exact: entourage_refl. +Qed. + +Let initial_ent_inv A : initial_ent A -> initial_ent A^-1. +Proof. +move=> [B ? sBA]; exists B^-1; first exact: entourage_inv. +by move=> ??; exact/sBA. +Qed. + +Let initial_ent_split A : initial_ent A -> exists2 B, initial_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 ((map_pair f)@^-1` C); first by exists C. +by case=> x y [a ? ?]; apply/sBA/CsubB; exists (f a). +Qed. + +Let initial_ent_nbhs : nbhs = nbhs_ initial_ent. +Proof. +rewrite predeq2E => x V; split. + case=> [? [[B ? <-] ? BsubV]]; have: nbhs (f x) B by apply: open_nbhs_nbhs. + 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. + +HB.instance Definition _ := @Nbhs_isUniform.Build (initial_topology f) + initial_ent initial_ent_filter initial_ent_refl initial_ent_inv + initial_ent_split initial_ent_nbhs. + +End initial_uniform. + +HB.instance Definition _ (pS : pointedType) (U : uniformType) (f : pS -> U) := + Pointed.on (initial_topology f). + +Section initial_pseudoMetric. +Context {R : realType} (pS : choiceType) (U : pseudoMetricType R) . +Variable (f : pS -> U). + +Notation S := (initial_topology f). + +Definition initial_ball (x : S) (r : R) (y : S) := ball (f x) r (f y). + +Let initial_pseudo_metric_ball_center (x : S) (e : R) : 0 < e -> + initial_ball x e x. +Proof. by move=> /posnumP[{}e]; exact: ball_center. Qed. + +Let initial_pseudo_metric_entourageE : entourage = entourage_ initial_ball. +Proof. +rewrite /entourage /= /initial_ent -entourage_ballE /entourage_. +have -> : (fun e => [set xy | ball (f xy.1) e (f xy.2)]) = + (preimage (map_pair f) \o fun e => [set xy | ball xy.1 e xy.2])%FUN. + by []. +rewrite eqEsubset; split; apply/filter_fromP. +- apply: filter_from_filter; first by exists 1 => /=. + move=> e1 e2 e1pos e2pos; wlog e1lee2 : e1 e2 e1pos e2pos / e1 <= e2. + by have [?|/ltW ?] := lerP e1 e2; [exact | rewrite setIC; exact]. + exists e1 => //; rewrite -preimage_setI; apply: preimage_subset. + by move=> ? ?; split => //; apply: le_ball; first exact: e1lee2. +- by move=> E [e ?] heE; exists e => //; apply: preimage_subset. +- apply: filter_from_filter. + by exists [set xy | ball xy.1 1 xy.2]; exists 1 => /=. + move=> E1 E2 [e1 e1pos he1E1] [e2 e2pos he2E2]. + wlog ? : E1 E2 e1 e2 e1pos e2pos he1E1 he2E2 / e1 <= e2. + have [? /(_ _ _ e1 e2)|/ltW ? ] := lerP e1 e2; first exact. + by rewrite setIC => /(_ _ _ e2 e1); exact. + exists (E1 `&` E2) => //; exists e1 => // xy /= B; split; first exact: he1E1. + by apply/he2E2/le_ball; last exact: B. +- by move=> e ?; exists [set xy | ball xy.1 e xy.2] => //; exists e => /=. +Qed. + +HB.instance Definition _ := Uniform_isPseudoMetric.Build R S + initial_pseudo_metric_ball_center (fun _ _ _ => @ball_sym _ _ _ _ _) + (fun _ _ _ _ _ => @ball_triangle _ _ _ _ _ _ _) + initial_pseudo_metric_entourageE. + +Lemma initial_ballE (e : R) (x : S) : f @^-1` (ball (f x) e) = ball x e. +Proof. by []. Qed. + +End initial_pseudoMetric. + +(** for an orderedTopologicalType T, and subtype U + (order_topology (sub_type U)) `<=` (initial_topology (sub_type U)) + but generally the topologies are not equal! + Consider `[0,1[ | {2}` as a subset of `[0,3]` for an example +*) +Section initial_order_refine. +Context {d} {X : orderTopologicalType d} {Y : subType X}. + +Let OrdU : orderTopologicalType d := order_topology (sub_type Y). +Let InitialU : topologicalType := @initial_topology (sub_type Y) X val. + +Lemma open_order_initial (U : set Y) : @open OrdU U -> @open InitialU U. +Proof. +rewrite ?openE /= /interior => + x Ux => /(_ x Ux); rewrite itv_nbhsE /=. +move=> [][][[]l|[]] [[]r|[]][]//= _ xlr /filterS; apply. +- exists `]l, r[%classic; split => //=; exists `]\val l, \val r[%classic. + exact: itv_open. + by rewrite eqEsubset; split => z; rewrite preimage_itv. +- exists `]l, +oo[%classic; split => //=; exists `]\val l, +oo[%classic. + exact: rray_open. + by rewrite eqEsubset; split => z; rewrite preimage_itv. +- exists `]-oo, r[%classic; split => //=; exists `]-oo, \val r[%classic. + exact: lray_open. + by rewrite eqEsubset; split => z; rewrite preimage_itv. +- by rewrite set_itvE; exact: filterT. +Qed. + +End initial_order_refine. + +Lemma continuous_comp_initial {Y : choiceType} {X Z : topologicalType} + (w : Y -> Z) (f : X -> initial_topology w) : + continuous (w \o f) -> continuous f. +Proof. +move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf. +exact: open_nbhs_nbhs. +Qed. diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v index 628f39684e..1e8e199b13 100644 --- a/theories/topology_theory/one_point_compactification.v +++ b/theories/topology_theory/one_point_compactification.v @@ -1,7 +1,8 @@ +(* mathcomp analysis (c) 2026 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 uniform_structure. -From mathcomp Require Import pseudometric_structure compact weak_topology. +From mathcomp Require Import pseudometric_structure compact initial_topology. (**md**************************************************************************) (* # One-Point Compactifications *) @@ -93,10 +94,10 @@ rewrite !openE/= => UU' opcX [x /UU' Ux <-]. exact/one_point_compactification_some_nbhs. Qed. -Lemma one_point_compactification_weak_topology : - @nbhs _ (@weak_topology X opc Some) = @nbhs _ X. +Lemma one_point_compactification_initial_topology : + @nbhs _ (@initial_topology X opc Some) = @nbhs _ X. Proof. -rewrite predeq2E => x U; split; rewrite /(@nbhs _ (weak_topology _))/=. +rewrite predeq2E => x U; split; rewrite /(@nbhs _ (initial_topology _))/=. case=> _ [[/= W] oW <- /= WSs] /filterS; apply. exact/one_point_compactification_some_continuous/oW. rewrite nbhsE => -[V [oV Vx VU]]; exists V; split => //. diff --git a/theories/topology_theory/subspace_topology.v b/theories/topology_theory/subspace_topology.v index ad62c0f2dd..12bf5c5752 100644 --- a/theories/topology_theory/subspace_topology.v +++ b/theories/topology_theory/subspace_topology.v @@ -1,8 +1,8 @@ (* mathcomp analysis (c) 2025 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 uniform_structure compact . -From mathcomp Require Import pseudometric_structure connected weak_topology. +From mathcomp Require Import topology_structure uniform_structure compact. +From mathcomp Require Import pseudometric_structure connected initial_topology. From mathcomp Require Import product_topology. (**md**************************************************************************) @@ -564,11 +564,11 @@ Proof. by []. Qed. End SubspacePseudoMetric. -Section SubspaceWeak. +Section SubspaceInitial. Context {T : topologicalType} {U : choiceType}. Variables (f : U -> T). -Lemma weak_subspace_open (A : set (weak_topology f)) : +Lemma initial_subspace_open (A : set (initial_topology f)) : open A -> open (f @` A : set (subspace (range f))). Proof. case=> B oB <-; apply/open_subspaceP; exists B; split => //; rewrite eqEsubset. @@ -576,7 +576,7 @@ split => z [] /[swap]; first by case=> w _ <- ?; split; exists w. by case=> w _ <- [v] ? <-. Qed. -End SubspaceWeak. +End SubspaceInitial. Lemma continuous_compact {T U : topologicalType} (f : T -> U) A : {within A, continuous f} -> compact A -> compact (f @` A). diff --git a/theories/topology_theory/subtype_topology.v b/theories/topology_theory/subtype_topology.v index 14430f1372..b9cb8bc6bc 100644 --- a/theories/topology_theory/subtype_topology.v +++ b/theories/topology_theory/subtype_topology.v @@ -1,8 +1,8 @@ -(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2026 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 reals topology_structure uniform_structure compact. -From mathcomp Require Import pseudometric_structure connected weak_topology. +From mathcomp Require Import pseudometric_structure connected initial_topology. From mathcomp Require Import product_topology subspace_topology. (**md**************************************************************************) @@ -30,13 +30,13 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. HB.instance Definition _ {X : topologicalType} (A : set X) := - Topological.copy (set_type A) (weak_topology set_val). + Topological.copy (set_type A) (initial_topology set_val). HB.instance Definition _ {X : uniformType} (A : set X) := - Uniform.copy (A : Type) (@weak_topology (A : Type) X set_val). + Uniform.copy (A : Type) (@initial_topology (A : Type) X set_val). HB.instance Definition _ {R : realType} {X : pseudoMetricType R} (A : set X) := - PseudoMetric.copy (A : Type) (@weak_topology (A : Type) X set_val). + PseudoMetric.copy (A : Type) (@initial_topology (A : Type) X set_val). Section subspace_sig. Context {X : topologicalType} (A : set X). @@ -62,7 +62,7 @@ Lemma subspace_sigL_continuousP {Y : topologicalType} (f : X -> Y) : Proof. split. have /continuous_subspaceT/subspaceT_continuous := - @weak_continuous A X set_val. + @initial_continuous A X set_val. move=> svf ctsf; apply/continuous_subspace_setT => x. apply: (@continuous_comp (subspace _) (subspace A)); last exact: ctsf. by move=> U nfU; exact: svf. diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index 219af7220c..aae6eab62d 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -14,7 +14,7 @@ From mathcomp Require Export subtype_topology. From mathcomp Require Export supremum_topology. From mathcomp Require Export topology_structure. From mathcomp Require Export uniform_structure. -From mathcomp Require Export weak_topology. +From mathcomp Require Export initial_topology. From mathcomp Require Export one_point_compactification. From mathcomp Require Export sigT_topology. From mathcomp Require Export discrete_topology. diff --git a/theories/topology_theory/weak_topology.v b/theories/topology_theory/weak_topology.v index 7d8ab3139a..07f584dad0 100644 --- a/theories/topology_theory/weak_topology.v +++ b/theories/topology_theory/weak_topology.v @@ -7,221 +7,5 @@ From mathcomp Require Import interval_inference reals topology_structure. From mathcomp Require Import uniform_structure order_topology. From mathcomp Require Import pseudometric_structure. -(**md**************************************************************************) -(* # Weak/initial topology *) -(* This file defines the weak topology for $S$ by a function $f$ whose domain *) -(* is $S$. This topology is also known as initial topology on $S$ with *) -(* respect to $f$. *) -(* *) -(* ``` *) -(* weak_topology f == weak topology by a function f : S -> T on S *) -(* S must be a choiceType and T a topologicalType. *) -(* ``` *) -(* `weak_topology` is equipped with the structures of: *) -(* - uniform space *) -(* - pseudometric space (the metric space for weak topologies) *) -(******************************************************************************) - -Import Order.TTheory GRing.Theory Num.Theory. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Local Open Scope classical_set_scope. -Local Open Scope ring_scope. - -Definition weak_topology {S : Type} {T : Type} - (f : S -> T) : Type := S. - -Section Weak_Topology. -Variable (S : choiceType) (T : topologicalType) (f : S -> T). -Local Notation W := (weak_topology f). - -Definition wopen := [set f @^-1` A | A in open]. - -Local Lemma wopT : wopen [set: W]. -Proof. by exists setT => //; apply: openT. Qed. - -Local Lemma wopI (A B : set W) : wopen A -> wopen B -> wopen (A `&` B). -Proof. -by move=> [C Cop <-] [D Dop <-]; exists (C `&` D) => //; apply: openI. -Qed. - -Local Lemma wop_bigU (I : Type) (g : I -> set W) : - (forall i, wopen (g i)) -> wopen (\bigcup_i g i). -Proof. -move=> gop. -set opi := fun i => [set Ui | open Ui /\ g i = f @^-1` Ui]. -exists (\bigcup_i get (opi i)). - apply: bigcup_open => i. - by have /getPex [] : exists U, opi i U by have [U] := gop i; exists U. -have g_preim i : g i = f @^-1` (get (opi i)). - by have /getPex [] : exists U, opi i U by have [U] := gop i; exists U. -rewrite predeqE => s; split=> [[i _]|[i _]]; last by rewrite g_preim; exists i. -by rewrite -[_ _]/((f @^-1` _) _) -g_preim; exists i. -Qed. - -HB.instance Definition _ := Choice.on W. -HB.instance Definition _ := - isOpenTopological.Build W wopT wopI wop_bigU. - -Lemma weak_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. -Proof. -move=> FF fsurj; split=> [cvFs|cvfFfs]. - move=> A /weak_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=> 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. - -End Weak_Topology. - -HB.instance Definition _ (S : pointedType) (T : topologicalType) (f : S -> T) := - Pointed.on (weak_topology f). - -Section weak_uniform. -Local Open Scope relation_scope. -Variable (pS : choiceType) (U : uniformType) (f : pS -> U). - -Let S := weak_topology f. - -Definition weak_ent : set_system (S * S) := - filter_from (@entourage U) (fun V => (map_pair f)@^-1` V). - -Lemma weak_ent_filter : Filter weak_ent. -Proof. -apply: filter_from_filter; first by exists setT; exact: entourageT. -by move=> P Q ??; (exists (P `&` Q); first exact: filterI) => ?. -Qed. - -Lemma weak_ent_refl A : weak_ent A -> diagonal `<=` A. -Proof. -by move=> [B ? sBA] [x y]/diagonalP ->; apply/sBA; exact: entourage_refl. -Qed. - -Lemma weak_ent_inv A : weak_ent A -> weak_ent A^-1. -Proof. -move=> [B ? sBA]; exists B^-1; first exact: entourage_inv. -by move=> ??; exact/sBA. -Qed. - -Lemma weak_ent_split A : weak_ent A -> exists2 B, weak_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 ((map_pair f)@^-1` C); first by exists C. -by case=> x y [a ? ?]; apply/sBA/CsubB; exists (f a). -Qed. - -Lemma weak_ent_nbhs : nbhs = nbhs_ weak_ent. -Proof. -rewrite predeq2E => x V; split. - case=> [? [[B ? <-] ? BsubV]]; have: nbhs (f x) B by apply: open_nbhs_nbhs. - 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. - -HB.instance Definition _ := @Nbhs_isUniform.Build (weak_topology f) weak_ent - weak_ent_filter weak_ent_refl weak_ent_inv weak_ent_split weak_ent_nbhs. - -End weak_uniform. - -HB.instance Definition _ (pS : pointedType) (U : uniformType) (f : pS -> U) := - Pointed.on (weak_topology f). - -Section weak_pseudoMetric. -Context {R : realType} (pS : choiceType) (U : pseudoMetricType R) . -Variable (f : pS -> U). - -Notation S := (weak_topology f). - -Definition weak_ball (x : S) (r : R) (y : S) := ball (f x) r (f y). - -Lemma weak_pseudo_metric_ball_center (x : S) (e : R) : 0 < e -> weak_ball x e x. -Proof. by move=> /posnumP[{}e]; exact: ball_center. Qed. - -Lemma weak_pseudo_metric_entourageE : entourage = entourage_ weak_ball. -Proof. -rewrite /entourage /= /weak_ent -entourage_ballE /entourage_. -have -> : (fun e => [set xy | ball (f xy.1) e (f xy.2)]) = - (preimage (map_pair f) \o fun e => [set xy | ball xy.1 e xy.2])%FUN. - by []. -rewrite eqEsubset; split; apply/filter_fromP. -- apply: filter_from_filter; first by exists 1 => /=. - move=> e1 e2 e1pos e2pos; wlog e1lee2 : e1 e2 e1pos e2pos / e1 <= e2. - by have [?|/ltW ?] := lerP e1 e2; [exact | rewrite setIC; exact]. - exists e1 => //; rewrite -preimage_setI; apply: preimage_subset. - by move=> ? ?; split => //; apply: le_ball; first exact: e1lee2. -- by move=> E [e ?] heE; exists e => //; apply: preimage_subset. -- apply: filter_from_filter. - by exists [set xy | ball xy.1 1 xy.2]; exists 1 => /=. - move=> E1 E2 [e1 e1pos he1E1] [e2 e2pos he2E2]. - wlog ? : E1 E2 e1 e2 e1pos e2pos he1E1 he2E2 / e1 <= e2. - have [? /(_ _ _ e1 e2)|/ltW ? ] := lerP e1 e2; first exact. - by rewrite setIC => /(_ _ _ e2 e1); exact. - exists (E1 `&` E2) => //; exists e1 => // xy /= B; split; first exact: he1E1. - by apply/he2E2/le_ball; last exact: B. -- by move=> e ?; exists [set xy | ball xy.1 e xy.2] => //; exists e => /=. -Qed. - -HB.instance Definition _ := Uniform_isPseudoMetric.Build R S - weak_pseudo_metric_ball_center (fun _ _ _ => @ball_sym _ _ _ _ _) - (fun _ _ _ _ _ => @ball_triangle _ _ _ _ _ _ _) - weak_pseudo_metric_entourageE. - -Lemma weak_ballE (e : R) (x : S) : f @^-1` (ball (f x) e) = ball x e. -Proof. by []. Qed. - -End weak_pseudoMetric. - -(** for an orderedTopologicalType T, and subtype U - (order_topology (sub_type U)) `<=` (weak_topology (sub_type U)) - but generally the topologies are not equal! - Consider `[0,1[ | {2}` as a subset of `[0,3]` for an example -*) -Section weak_order_refine. -Context {d} {X : orderTopologicalType d} {Y : subType X}. - -Let OrdU : orderTopologicalType d := order_topology (sub_type Y). -Let WeakU : topologicalType := @weak_topology (sub_type Y) X val. - -Lemma open_order_weak (U : set Y) : @open OrdU U -> @open WeakU U. -Proof. -rewrite ?openE /= /interior => + x Ux => /(_ x Ux); rewrite itv_nbhsE /=. -move=> [][][[]l|[]] [[]r|[]][]//= _ xlr /filterS; apply. -- exists `]l, r[%classic; split => //=; exists `]\val l, \val r[%classic. - exact: itv_open. - by rewrite eqEsubset; split => z; rewrite preimage_itv. -- exists `]l, +oo[%classic; split => //=; exists `]\val l, +oo[%classic. - exact: rray_open. - by rewrite eqEsubset; split => z; rewrite preimage_itv. -- exists `]-oo, r[%classic; split => //=; exists `]-oo, \val r[%classic. - exact: lray_open. - by rewrite eqEsubset; split => z; rewrite preimage_itv. -- by rewrite set_itvE; exact: filterT. -Qed. - -End weak_order_refine. - -Lemma continuous_comp_weak {Y : choiceType} {X Z : topologicalType} (w : Y -> Z) - (f : X -> weak_topology w) : - continuous (w \o f) -> continuous f. -Proof. -move=> cf z U [?/= [[W oW <-]]] /= Wsfz /filterS; apply; apply: cf. -exact: open_nbhs_nbhs. -Qed. +Attributes deprecated(since="mathcomp-analysis 1.16.0", + note="Use initial_topology.v instead").