Skip to content
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

draft: separating pointed out of topological #1191

Closed
wants to merge 3 commits into from
Closed

draft: separating pointed out of topological #1191

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e2f1ac9
separating pointed out of topological
zstone1 Mar 25, 2024
d2ca418
fixing the rest of the pointedness issues
zstone1 Mar 25, 2024
4537b50
trying to make backwards compatability work
zstone1 Apr 11, 2024
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
42 changes: 30 additions & 12 deletions theories/cantor.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,8 @@ Proof. by []. Qed.
Definition pointed_discrete_topology (P : pointedType) : Type :=
discrete_topology (discrete_pointed_subproof P).

HB.instance Definition _ P := Pointed.on (pointed_discrete_topology P).

End discrete_topology_for_pointed_types.
(* note that in topology.v, we already have:
HB.instance Definition _ := discrete_uniform_mixin.
Expand Down Expand Up @@ -128,6 +130,15 @@ split.
- exact: cantor_zero_dimensional.
Qed.

HB.instance Definition _ (U : Type) (T : U -> ptopologicalType) :=
Pointed.copy (forall x : U, T x) (prod_topology T).

Global Instance prod_topology_filter (U : Type) (T : U -> ptopologicalType) (f : prod_topology T) :
ProperFilter (nbhs f).
Proof.
exact: nbhs_pfilter.
Qed.

(**md**************************************************************************)
(* ## Part 1 *)
(* *)
Expand All @@ -143,7 +154,7 @@ Qed.
(* *)
(******************************************************************************)
Section topological_trees.
Context {K : nat -> topologicalType} {X : topologicalType}
Context {K : nat -> ptopologicalType} {X : ptopologicalType}
(refine_apx : forall n, set X -> K n -> set X)
(tree_invariant : set X -> Prop).

Expand Down Expand Up @@ -233,7 +244,8 @@ elim: n => [|n IH]; first by near=> z => ?; rewrite ltn0.
near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z).
move=> [->]; near: z; exists (proj n @^-1` [set b n]).
split => //; suff : @open T (proj n @^-1` [set b n]) by [].
by apply: open_comp; [move=> + _; exact: proj_continuous| exact: discrete_open].
apply: open_comp; [move=> + _; exact: proj_continuous| apply: discrete_open].
exact: discreteK.
Unshelve. all: end_near. Qed.

Let apx_prefix b c n :
Expand All @@ -253,7 +265,6 @@ Qed.
Local Lemma tree_map_cts : continuous tree_map.
Proof.
move=> b U /cvg_tree_map [n _] /filterS; apply.
exact/fmap_filter/nbhs_filter.
rewrite nbhs_simpl /=; near_simpl; have := tree_prefix b n; apply: filter_app.
by near=> z => /apx_prefix ->; exact: tree_map_apx.
Unshelve. all: end_near. Qed.
Expand Down Expand Up @@ -299,7 +310,7 @@ End topological_trees.
(******************************************************************************)

Section TreeStructure.
Context {R : realType} {T : pseudoMetricType R}.
Context {R : realType} {T : pseudoPMetricType R}.
Hypothesis cantorT : cantor_like T.

Let dsctT : zero_dimensional T. Proof. by case: cantorT. Qed.
Expand Down Expand Up @@ -395,13 +406,20 @@ End TreeStructure.
(* ## Part 3: Finitely branching trees are Cantor-like *)
(******************************************************************************)
Section FinitelyBranchingTrees.
Context {R : realType}.

Definition tree_of (T : nat -> pointedType) : pseudoMetricType R :=
[the pseudoMetricType R of prod_topology
(fun n => pointed_discrete_topology (T n))].
Definition tree_of (T : nat -> pointedType) : Type :=
prod_topology (fun n => pointed_discrete_topology (T n)).

HB.instance Definition _ (T : nat -> pointedType) : Pointed (tree_of T):=
Pointed.on (tree_of T).

HB.instance Definition _ (T : nat -> pointedType) := Uniform.on (tree_of T).

HB.instance Definition _ {R : realType} (T : nat -> pointedType) :
@PseudoMetric R _ :=
@PseudoMetric.on (tree_of T).

Lemma cantor_like_finite_prod (T : nat -> topologicalType) :
Lemma cantor_like_finite_prod (T : nat -> ptopologicalType) :
(forall n, finite_set [set: pointed_discrete_topology (T n)]) ->
(forall n, (exists xy : T n * T n, xy.1 != xy.2)) ->
cantor_like (tree_of T).
Expand All @@ -426,7 +444,7 @@ Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
(* ## Part 4: Building a finitely branching tree to cover `T` *)
(******************************************************************************)
Section alexandroff_hausdorff.
Context {R : realType} {T : pseudoMetricType R}.
Context {R : realType} {T : pseudoPMetricType R}.

Hypothesis cptT : compact [set: T].
Hypothesis hsdfT : hausdorff_space T.
Expand Down Expand Up @@ -506,7 +524,7 @@ HB.instance Definition _ n := gen_choiceMixin (K' n).
HB.instance Definition _ n := isPointed.Build (K' n) (K'p n).

Let K n := [the pointedType of K' n].
Let Tree := @tree_of R K.
Let Tree := @tree_of K.

Let embed_refine n (U : set T) (k : K n) :=
(if pselect (projT1 k `&` U !=set0)
Expand Down Expand Up @@ -566,7 +584,7 @@ Local Lemma cantor_surj_pt2 :
exists f : {surj [set: cantor_space] >-> [set: Tree]}, continuous f.
Proof.
have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f.
apply: (@cantor_like_finite_prod _ (pointed_discrete_topology \o K)) => [n /=|n].
apply: (@cantor_like_finite_prod (pointed_discrete_topology \o K)) => [n /=|n].
have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
suff -> : [set: {classic K' n}] =
(@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))).
Expand Down
87 changes: 52 additions & 35 deletions theories/function_spaces.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,7 +112,7 @@ Variable I : Type.

Definition product_topology_def (T : I -> topologicalType) :=
sup_topology (fun i => Topological.class
(weak_topology (fun f : [the pointedType of forall i, T i] => f i))).
(weak_topology (fun f : [the choiceType of forall i, T i] => f i))).

HB.instance Definition _ (T : I -> topologicalType) :=
Topological.copy (prod_topology T) (product_topology_def T).
Expand Down Expand Up @@ -155,7 +155,7 @@ Proof.
move=> f; have /cvg_sup/(_ i)/cvg_image : f --> f by apply: cvg_id.
move=> h; apply: cvg_trans (h _) => {h}.
by move=> Q /= [W nbdW <-]; apply: filterS nbdW; exact: preimage_image.
rewrite eqEsubset; split => y //; exists (dfwith (fun=> point) i y) => //.
rewrite eqEsubset; split => y //; exists (dfwith f i y) => //.
by rewrite dfwithin.
Qed.

Expand Down Expand Up @@ -204,7 +204,9 @@ Lemma tychonoff (I : eqType) (T : I -> topologicalType)
(forall i, compact (A i)) ->
compact [set f : forall i, T i | forall i, A i (f i)].
Proof.
move=> Aco; rewrite compact_ultra => F FU FA.
case: (pselect ([set f : forall i, T i | forall i, A i (f i)] == set0)).
move/eqP => -> _; exact: compact0.
case/negP/set0P=> a0 Aa0 Aco; rewrite compact_ultra => F FU FA.
set subst_coord := fun (i : I) (pi : T i) (f : forall x : I, T x) (j : I) =>
if eqP is ReflectT e then ecast i (T i) (esym e) pi else f j.
have subst_coordT i pi f : subst_coord i pi f i = pi.
Expand All @@ -215,7 +217,7 @@ have subst_coordN i pi f j : i != j -> subst_coord i pi f j = f j.
by move: inej; rewrite {1}e => /negP.
have pr_surj i : @^~ i @` [set: forall i, T i] = setT.
rewrite predeqE => pi; split=> // _.
by exists (subst_coord i pi (fun=> point)) => //; rewrite subst_coordT.
by exists (subst_coord i pi a0) => //; rewrite subst_coordT.
pose pF i : set_system _ := [set @^~ i @` B | B in F].
have pFultra i : UltraFilter (pF i) by exact: ultra_image (pr_surj i).
have pFA i : pF i (A i).
Expand All @@ -227,9 +229,10 @@ have pFA i : pF i (A i).
by move=> /subst_coordN ->; apply: Af.
have cvpFA i : A i `&` [set p | pF i --> p] !=set0.
by rewrite -ultra_cvg_clusterE; apply: Aco.
exists (fun i => get (A i `&` [set p | pF i --> p])).
split=> [i|]; first by have /getPex [] := cvpFA i.
by apply/cvg_sup => i; apply/cvg_image=> //; have /getPex [] := cvpFA i.
exists (fun i => xget (a0 i) (A i `&` [set p | pF i --> p])).
split=> [i|]; first by have /(xgetPex (a0 i)) [] := cvpFA i.
apply/cvg_sup => i; apply/cvg_image=> //.
by have /(xgetPex (a0 i)) [] := cvpFA i.
Qed.

Lemma perfect_prod {I : Type} (i : I) (K : I -> topologicalType) :
Expand Down Expand Up @@ -440,13 +443,16 @@ Qed.

Definition arrow_uniform_type : Type := T -> U.

#[export] HB.instance Definition _ := Pointed.on arrow_uniform_type.
#[export] HB.instance Definition _ := Choice.on arrow_uniform_type.
#[export] HB.instance Definition _ := isUniform.Build arrow_uniform_type
fct_ent_filter fct_ent_refl fct_ent_inv fct_ent_split.

#[export] HB.instance Definition _ := Uniform.on arrow_uniform_type.
End fct_Uniform.

#[export] HB.instance Definition _ {T : choiceType} {U : puniformType} :=
Pointed.on (arrow_uniform_type T U).

Lemma cvg_fct_entourageP (T : choiceType) (U : uniformType)
(F : set_system (arrow_uniform_type T U)) (FF : Filter F)
(f : arrow_uniform_type T U) :
Expand Down Expand Up @@ -597,10 +603,14 @@ split=> [[Q [[/= W oW <- /=] Wf subP]]|[E [entE subP]]].
case: (oW _ Wf) => ? [ /= E entE] Esub subW.
exists E; split=> // h Eh; apply/subP/subW/Esub => /= [[u Au]].
by apply: Eh => /=; rewrite -inE.
near=> g; apply: subP => y /mem_set Ay; rewrite -!(sigLE A).
case : (pselect (exists (u : U), True)); first last.
move=> nU; apply: (filterS subP); apply: (@filterS _ _ _ setT).
by move=> t _ /= y; move: nU; apply: absurd; exists y.
exact: filterT.
case=> u0 _; near=> g; apply: subP => y /mem_set Ay; rewrite -!(sigLE A).
move: (SigSub _); near: g.
have := (@cvg_image _ _ (@sigL_arrow _ A V) _ f (nbhs_filter f)
(image_sigL point)).1 cvg_id [set h | forall y, E (sigL A f y, h y)].
(image_sigL (f u0))).1 cvg_id [set h | forall y, E (sigL A f y, h y)].
case; first by exists [set fg | forall y, E (fg.1 y, fg.2 y)]; [exists E|].
move=> B nbhsB rBrE; apply: (filterS _ nbhsB) => g Bg [y yA].
by move: rBrE; rewrite eqEsubset; case => [+ _]; apply; exists g.
Expand Down Expand Up @@ -725,25 +735,6 @@ exists (g u); split; [apply: X'X| apply: Y'Y]; last exact: entourage_refl.
apply: (C [set fg | forall y, A y -> X' (fg.1 y, fg.2 y)]) => //=.
by rewrite uniform_entourage; exists X'.
Qed.
Lemma uniform_restrict_cvg
(F : set_system (U -> V)) (f : U -> V) A : Filter F ->
{uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
Proof.
move=> FF; rewrite cvg_sigL; split.
- rewrite -sigLK; move/(cvg_app valL) => D.
apply: cvg_trans; first exact: D.
move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
apply/uniform_nbhs; exists E; split=> //= h /=.
rewrite /sigL => R u _; rewrite oinv_set_val.
by case: insubP=> /= *; [apply: R|apply: entourage_refl].
- move/(@cvg_app _ _ _ _ (sigL A)).
rewrite -fmap_comp sigL_restrict => D.
apply: cvg_trans; first exact: D.
move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
apply/uniform_nbhs; exists E; split=> //= h /=.
rewrite /sigL => R [u Au] _ /=.
by have := R u I; rewrite /patch Au.
Qed.

Lemma uniform_nbhsT (f : U -> V) :
(nbhs (f : {uniform U -> V})) = nbhs (f : arrow_uniform_type U V).
Expand Down Expand Up @@ -817,6 +808,27 @@ Qed.

End UniformCvgLemmas.

Lemma uniform_restrict_cvg {U : choiceType} {V : puniformType}
(F : set_system (U -> V)) (f : U -> V) A : Filter F ->
{uniform A, F --> f} <-> {uniform, restrict A @ F --> restrict A f}.
Proof.
move=> FF; rewrite cvg_sigL; split.
- rewrite -sigLK; move/(cvg_app valL) => D.
apply: cvg_trans; first exact: D.
move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
apply/uniform_nbhs; exists E; split=> //= h /=.
rewrite /sigL => R u _; rewrite oinv_set_val.
by case: insubP=> /= *; [apply: R|apply: entourage_refl].
- move/(@cvg_app _ _ _ _ (sigL A)).
rewrite -fmap_comp sigL_restrict => D.
apply: cvg_trans; first exact: D.
move=> P /uniform_nbhs [E [/=entE EsubP]]; apply: (filterS EsubP).
apply/uniform_nbhs; exists E; split=> //= h /=.
rewrite /sigL => R [u Au] _ /=.
by have := R u I; rewrite /patch Au.
Qed.


Section FamilyConvergence.

Lemma fam_cvgE {U : choiceType} {V : uniformType} (F : set_system (U -> V))
Expand Down Expand Up @@ -881,7 +893,7 @@ move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split.
by move=> g /= gPQ; split; exact: (subset_trans gPQ).
Qed.

HB.instance Definition _ := Pointed.on compact_openK.
HB.instance Definition _ := Choice.on compact_openK.

HB.instance Definition _ := hasNbhs.Build compact_openK compact_openK_nbhs.

Expand All @@ -908,8 +920,6 @@ HB.instance Definition _ :=

End compact_open_setwise.

HB.instance Definition _ := Pointed.on compact_open.

Definition compact_open_def :=
sup_topology (fun i : sigT (@compact T) =>
Topological.class (@compact_openK (projT1 i))).
Expand Down Expand Up @@ -942,12 +952,19 @@ Qed.

End compact_open.

HB.instance Definition _ {U : topologicalType} {V : ptopologicalType} K :=
Pointed.on (@compact_openK U V K).

HB.instance Definition _ {U : topologicalType} {V : ptopologicalType} :=
Pointed.on (@compact_open U V).


Notation "{ 'compact-open' , U -> V }" := (@compact_open U V).
Notation "{ 'compact-open' , F --> f }" :=
(F --> (f : @compact_open _ _)).

Section compact_open_uniform.
Context {U : topologicalType} {V : uniformType}.
Context {U : topologicalType} {V : puniformType}.

Let small_ent_sub := @small_set_sub _ (@entourage V).

Expand Down Expand Up @@ -1029,7 +1046,7 @@ apply/Ff/uniform_nbhs; exists (split_ent (split_ent A))^-1%classic.
by split; [exact: entourage_inv | move=> g fg; near_simpl; near=> z; exact: fg].
Unshelve. all: end_near. Qed.

Lemma uniform_limit_continuous_subspace {U : topologicalType} {V : uniformType}
Lemma uniform_limit_continuous_subspace {U : topologicalType} {V : puniformType}
(K : set U) (F : set_system (U -> V)) (f : subspace K -> V) :
ProperFilter F -> (\forall g \near F, continuous (g : subspace K -> V)) ->
{uniform K, F --> f} -> {within K, continuous f}.
Expand Down Expand Up @@ -1085,7 +1102,7 @@ Qed.
End UniformPointwise.

Section ArzelaAscoli.
Context {X : topologicalType} {Y : uniformType} {hsdf : hausdorff_space Y}.
Context {X : topologicalType} {Y : puniformType} {hsdf : hausdorff_space Y}.
Implicit Types (I : Type).

(** The key condition in Arzela-Ascoli that, like uniform continuity, moves a
Expand Down
30 changes: 19 additions & 11 deletions theories/normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -229,13 +229,13 @@ by rewrite opprK.
Qed.

HB.mixin Record NormedZmod_PseudoMetric_eq (R : numDomainType) T
of Num.NormedZmodule R T & PseudoMetric R T := {
of Num.NormedZmodule R T & PseudoPointedMetric R T := {
pseudo_metric_ball_norm : ball = ball_ (fun x : T => `| x |)
}.

#[short(type="pseudoMetricNormedZmodType")]
HB.structure Definition PseudoMetricNormedZmod (R : numDomainType) :=
{T of Num.NormedZmodule R T & PseudoMetric R T
{T of Num.NormedZmodule R T & PseudoPointedMetric R T
& NormedZmod_PseudoMetric_eq R T}.

Section pseudoMetricnormedzmodule_lemmas.
Expand Down Expand Up @@ -2743,17 +2743,25 @@ Lemma continuousZl s a x :
{for x, continuous s} -> {for x, continuous (fun z => s z *: a)}.
Proof. by move=> ?; apply: cvgZl. Qed.

Lemma continuousM s t x :
{for x, continuous s} -> {for x, continuous t} ->
{for x, continuous (s * t)}.
Proof. by move=> f_cont g_cont; apply: cvgM. Qed.

Lemma continuousV s x : s x != 0 ->
{for x, continuous s} -> {for x, continuous (fun x => (s x)^-1%R)}.
Proof. by move=> ?; apply: cvgV. Qed.

End local_continuity.

(* TODO: we need `ptopological` only because need to inherit the semiring structure.
if that is ever fixed upstream, we can eliminate this section *)
Section local_continuity_ring.
Context {K : numFieldType} {V : normedModType K} {T : ptopologicalType}.
Implicit Types (f g : T -> V) (s t : T -> K) (x : T) (k : K) (a : V).

Lemma continuousM s t x :
{for x, continuous s} -> {for x, continuous t} ->
{for x, continuous (s * t)}.
Proof. by move=> f_cont g_cont; apply: cvgM. Qed.
End local_continuity_ring.


Section nbhs_ereal.
Context {R : numFieldType} (P : \bar R -> Prop).

Expand Down Expand Up @@ -3609,11 +3617,11 @@ Qed.

Definition urysohnType : Type := T.

HB.instance Definition _ := Pointed.on urysohnType.

HB.instance Definition _ := Choice.on urysohnType.
HB.instance Definition _ :=
isUniform.Build urysohnType ury_unif_filter ury_unif_refl ury_unif_inv
ury_unif_split.
HB.instance Definition _ {p : Pointed T} := Pointed.copy urysohnType (Pointed.Pack p).

Lemma normal_uniform_separator (B : set T) :
closed A -> closed B -> A `&` B = set0 -> uniform_separator A B.
Expand Down Expand Up @@ -4923,7 +4931,7 @@ have : n \in enum_fset D by [].
by rewrite enum_fsetE => /mapP[/= i iD ->]; exact/le_bigmax.
Qed.

Lemma rV_compact (T : topologicalType) n (A : 'I_n.+1 -> set T) :
Lemma rV_compact (T : ptopologicalType) n (A : 'I_n.+1 -> set T) :
(forall i, compact (A i)) ->
compact [ set v : 'rV[T]_n.+1 | forall i, A i (v ord0 i)].
Proof.
Expand Down Expand Up @@ -5447,7 +5455,7 @@ Notation linear_continuous0 := __deprecated__linear_continuous0 (only parsing).
Notation linear_bounded0 := __deprecated__linear_bounded0 (only parsing).

Section center_radius.
Context {R : numDomainType} {M : pseudoMetricType R}.
Context {R : numDomainType} {M : pseudoPMetricType R}.
Implicit Types A : set M.

(* NB: the identifier "center" is already taken! *)
Expand Down
Loading
Loading