Module mathcomp.analysis.topology_theory.initial_topology

From HB Require Import structures.
From mathcomp Require Import boot order algebra all_classical finmap.
#[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 product_topology order_topology.
From mathcomp Require Import pseudometric_structure.

# 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 (e.g., Wilansky) 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. sub_initial_topology V S U == sub-initial topology generated by the \val : U -> V U has type subChoiceType S with S : pred V. This is a subTopologicalType when V is endowed with a topology. This is a subConvexTvsType when V is endowed with a convexTvsType (and when U is subLmodType). ``` `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.

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition { : Type} { : Type}
( : S -> T) : Type := S.

Section Initial_Topology.
Variable ( : choiceType) ( : topologicalType) ( : S -> T).
Local Notation := (initial_topology f).

Definition := [set f @^-1` A | in open].

Let : initial_open [set: W].

Proof.

by exists setT => //; exact: openT. Qed.

Let : setI_closed initial_open.

Proof.

by move=> ? ? [C Cop <-] [D Dop <-]; exists (C `&` D) => //; exact: openI.
Qed.

Let ( : Type) ( : I -> set W) :
(forall , initial_open (g i)) -> initial_open (\bigcup_ g i).

Proof.

move=> gop.
set opi := fun => [set | open Ui /\ g i = f @^-1` Ui].
exists (\bigcup_ get (opi i)).
  apply: bigcup_open => i.
  by have /getPex [] : exists , 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 , 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.

..on W.
.
isOpenTopological.Build W initial_opT initial_opI initial_op_bigU.

Lemma : continuous (f : W -> T).

Proof.

by apply/continuousP => A ?; exists A. Qed.

Lemma ( : set_system S) ( : S) :
Filter F -> f @` setT = setT ->
F --> (s : W) <-> ([set f @` 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.

Lemma ( : W) : nbhs (f w) A -> nbhs w (f @^-1` A).

Proof.

rewrite nbhsE /= => -[B [oB Bfx]] BA.
by exists (f @^-1` B); split => //= ; [exists B|move=> z /= /BA].
Qed.

End Initial_Topology.

. () (T : topologicalType) (f : S -> T) :=
Pointed.on (initial_topology f).

Definition ( : Type) ( : pred V) ( : subChoiceType S)
: Type := initial_topology (\val : U -> V).

Section SubType_isSubTopological.
Context ( : topologicalType) ( : pred V) ( : subChoiceType S).

Local Notation := (sub_initial_topology U).
..on T.
..on T.
..on T.

Let : continuous (val : T -> V).

Proof.

exact: initial_continuous. Qed.

..Build V S T top_continuous_valE.

End SubType_isSubTopological.

Section initial_uniform.
Local Open Scope relation_scope.
Variable ( : choiceType) ( : uniformType) ( : pS -> U).

Let := initial_topology f.

Definition : set_system (S * S) :=
filter_from (@entourage U) (fun => (map_pair f)@^-1` V).

Let : 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 A -> diagonal `<=` A.

Proof.

by move=> [B ? sBA] [x y]/diagonalP ->; apply/sBA; exact: entourage_refl.
Qed.

Let : 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 A -> exists2 , initial_ent B & B \; B `<=` A.

Proof.

move=> [B entB sBA]; have : exists , 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 : 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.

..Build (initial_topology f)
initial_ent initial_ent_filter initial_ent_refl initial_ent_inv
initial_ent_split initial_ent_nbhs.

End initial_uniform.

Section initial_unif_continuous.
Context { : choiceType} { : uniformType} ( : T -> U).

Lemma : unif_continuous (f : initial_topology f -> U).

Proof.

by move=> A entA; by exists A. Qed.

Lemma
( : uniformType) ( : V -> initial_topology f) :
unif_continuous (f \o g : V -> U) -> unif_continuous g.

Proof.

by move=> fg /= A [B entB BA]; apply: filterS _ _ BA _; exact: fg. Qed.

Lemma ( : uniformType) :
unif_continuous (fun : initial_topology f * V => f x.1).

Proof.

by apply: unif_continuous_comp;
[exact: fst_unif_continuous|exact: initial_unif_continuous].
Qed.

Lemma ( : uniformType) :
unif_continuous (fun : V * initial_topology f => f x.2).

Proof.

by apply: unif_continuous_comp;
[exact: snd_unif_continuous|exact: initial_unif_continuous].
Qed.

End initial_unif_continuous.

. () (U : uniformType) (f : pS -> U) :=
Pointed.on (initial_topology f).

Section initial_pseudoMetric.
Context { : realType} ( : choiceType) ( : pseudoMetricType R) .
Variable ( : pS -> U).

Notation := (initial_topology f).

Definition ( : S) ( : R) ( : S) := ball (f x) r (f y).

Let ( : S) ( : R) : 0 < e ->
initial_ball x e x.

Proof.

by move=> /posnumP[{}e]; exact: ball_center. Qed.

Let : entourage = entourage_ initial_ball.

Proof.

rewrite /entourage /= /initial_ent -entourage_ballE /entourage_.
have -> : (fun => [set | ball (f xy.1) e (f xy.2)]) =
   (preimage (map_pair f) \o fun => [set | 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 | 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 | ball xy.1 e xy.2] => //; exists e => /=.
Qed.

..Build R S
  initial_pseudo_metric_ball_center (fun _ _ _ => @ball_sym _ _ _ _ _)
  (fun _ _ _ _ _ => @ball_triangle _ _ _ _ _ _ _)
  initial_pseudo_metric_entourageE.

Lemma ( : R) ( : 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 {} { : orderTopologicalType d} { : subType X}.

Let : orderTopologicalType d := order_topology (sub_type Y).
Let : topologicalType := @initial_topology (sub_type Y) X val.

Lemma ( : 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 { : choiceType} { : topologicalType}
( : Y -> Z) ( : 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.

Files

Module mathcomp.analysis.topology_theory.initial_topology