Skip to content

rename weak_topology -> initial_topology #1834

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
affeldt-aist wants to merge 1 commit into
base: master
Choose a base branch
from
Open

rename weak_topology -> initial_topology #1834

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 29 additions & 1 deletion CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
1 change: 1 addition & 0 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions theories/Make
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
66 changes: 33 additions & 33 deletions theories/function_spaces.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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.

Expand Down Expand Up @@ -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))).
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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} .
Expand Down Expand Up @@ -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) :=
Expand Down Expand Up @@ -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.

Expand All @@ -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 *.
Expand Down
4 changes: 2 additions & 2 deletions theories/homotopy_theory/continuous_path.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
Expand Down Expand Up @@ -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).
Expand Down
12 changes: 7 additions & 5 deletions theories/normedtype_theory/urysohn.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 => //=.
Expand Down Expand Up @@ -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.
Expand All @@ -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 => /=.
Expand Down Expand Up @@ -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
Expand Down
Loading