From 9b2e906c517557d25412a7330515319ea75cc31b Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 21 Oct 2024 16:01:56 -0400 Subject: [PATCH] wedge stuff suitably generalized --- theories/function_spaces.v | 295 ++++++++++++++++++------------------- 1 file changed, 142 insertions(+), 153 deletions(-) diff --git a/theories/function_spaces.v b/theories/function_spaces.v index 82d2c48c7..8f6a6a6ef 100644 --- a/theories/function_spaces.v +++ b/theories/function_spaces.v @@ -1700,6 +1700,7 @@ Definition wedge := {eq_quot wedge_rel}. Definition wedgei (i : I) : X i -> wedge := \pi_wedge \o (existT X i). HB.instance Definition _ := Topological.copy wedge (quotient_topology wedge). +HB.instance Definition _ := Quotient.on wedge. Global Opaque wedge. Lemma wedgei_continuous (i : I) : continuous (@wedgei i). @@ -1788,16 +1789,7 @@ move=> i x; case: (pselect (x = p0 i)). move=> ->; rewrite wedge_point_nbhs => /=; apply: WedgeIsPoint. by move/eqP => xpi; rewrite /= -wedgei_nbhs //; apply: WedgeNotPoint. Qed. -(* -Lemma wedger_reprE (b : Y) : - repr (wedger b) = inr b \/ (repr (wedger b) = inl x0 /\ b = y0). -Proof. -case: piP; case=> [l|r] /eqmodP /orP []; first by move/eqP => ->; left. -- by case/orP=> /andP []/eqP // [] -> /eqP [] ->; right. -- by move/eqP ->; left. -by case/orP => /andP [] /eqP //. -Qed. - *) + Definition wedge_fun {Z : Type} (f : forall i, X i -> Z) : wedge -> Z := sum_fun f \o repr. @@ -1811,18 +1803,6 @@ move=> a b /eqmodP /orP [ /eqP -> // | /andP [/eqP +] /eqP +]. by rewrite /sum_fun /= => -> ->; exact: fE. Qed. -(* -Lemma wedgel_reprE (a : X) : - repr (wedgel a) = inl a \/ (repr (wedgel a) = inr y0 /\ a = x0). -Proof. -case: piP; case=> [l|r] /eqmodP /orP []; first by case/eqP => ->; left. -- by case/orP=> /andP [/eqP ->] /eqP -> //. -- by move/eqP. -case/orP => /andP [/eqP]; first by case=> -> /eqP ->; right. -by move=> -> /eqP -> //. -Qed. -*) - Lemma wedge_fun_wedgei {Z : Type} (f : forall i, X i -> Z) i0 (a : X i0): (forall i j, f i (p0 i) = f j (p0 j)) -> wedge_fun f (wedgei a) = f i0 a. Proof. @@ -1837,131 +1817,134 @@ rewrite -subTset=> z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. by exists (projT2 (repr z)); rewrite // reprK /wedgei /= -sigT_eta reprK. Qed. -Definition wedge_prod : topologicalType := - \bigcup_i [set: X] `*` [set y0] `|` [set x0] `*` [set: Y]. - -Lemma wedge_prodl (x : X) : (x,y0) \in - ([set: X] `*` [set y0] `|` [set x0] `*` [set: Y]). -Proof. by apply/mem_set; left. Qed. - -Lemma wedge_prodr (y : Y) : (x0,y) \in - ([set: X] `*` [set y0] `|` [set x0] `*` [set: Y]). -Proof. by apply/mem_set; right. Qed. - -Definition wedge_prod_fun : wedge -> wedge_prod := - wedge_fun - (fun x => @exist _ _ (x,y0) (wedge_prodl x)) - (fun y => @exist _ _ (x0,y) (wedge_prodr y)). -Lemma wedge_prod_fun_bij : bijective wedge_prod_fun. -Proof. -have pE : ((fun x => @exist _ _ (x,y0) (wedge_prodl x)) x0) = - ((fun y => @exist _ _ (x0,y) (wedge_prodr y))) y0 :> wedge_prod. - exact: eq_exist. -rewrite -setTT_bijective; split => //. - move=> a b _ _; rewrite -[a](@reprK _ wedge) -[b](@reprK _ wedge). - case Ea : (repr a) => [l1|r1]; case Eb : (repr b) => [l2|r2]. - - rewrite /wedge_prod_fun /= ?wedge_funl //=. - by move=> R; have [ ->] := EqdepFacts.eq_sig_fst R. - - rewrite /wedge_prod_fun /= ?wedge_funl //= ?wedge_funr //. - by move=> R; have [-> <-] := EqdepFacts.eq_sig_fst R; rewrite wedge_pointE. - - rewrite /wedge_prod_fun /= ?wedge_funl //= ?wedge_funr //. - by move=> R; have [<- ->] := EqdepFacts.eq_sig_fst R; rewrite wedge_pointE. - - rewrite /wedge_prod_fun /= ?wedge_funr //=. - by move=> R; have [ ->] := EqdepFacts.eq_sig_fst R. -case=> /= [][x y] xyE _; have /set_mem [[_ ]|[ + _]] /= := xyE. - move=> yE; exists (wedgel x) => //; rewrite /wedge_prod_fun wedge_funl /=. - by apply: eq_exist; rewrite yE. - exact: eq_exist. -move=> xE; exists (wedger y) => //; rewrite /wedge_prod_fun wedge_funr /=. - by apply: eq_exist; rewrite xE. -exact: eq_exist. +Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> + compact [set: wedge]. +Proof. +move=> fsetI cptX. +rewrite -wedgeTE -fsbig_setU //; apply: big_ind. +- exact: compact0. +- by move=> ? ? ? ?; exact: compactU. +move=> i _; apply: continuous_compact; last exact: cptX. +by apply: continuous_subspaceT; exact: wedgei_continuous. Qed. -Lemma wedge_prod_continuous : continuous wedge_prod_fun. +(* The wedge maps into the product + \bigcup_i [x | x j = p0 j when j != i] + + For the box topology, it's an embedding. But more practically, + since the box and product agree when `I` is finite, + we get that the finite wedge embeds into the finite product. + *) +Section wedge_as_product. +Definition wedge_prod_fun : wedge -> prod_topology X := + wedge_fun (fun i x => dfwith (p0) i x). + +Lemma wedge_prod_fun_pointE (i j : I) : dfwith p0 i (p0 i) = dfwith p0 j (p0 j). Proof. -apply: wedge_continuous; last by exact: eq_exist. - apply/continuousP => ? [A oA <-]; rewrite -comp_preimage. - apply: open_comp => //; set f := (set_val \o _). - have -> : (f = fun x => (x,y0)) by exact/funext. - move=> ? ?; apply: continuous2_cvg => //; last exact: cvg_cst. - by have -> : (fun z => (z.1,z.2)) = (@id (X*Y)) by apply/funext; case. -apply/continuousP => ? [A oA <-]; rewrite -comp_preimage. -apply: open_comp => //; set f := (set_val \o _). -have -> : (f = fun y => (x0,y)) by exact/funext. -move=> ? ?; apply: continuous2_cvg => //; last exact: cvg_cst. -by have -> : (fun z => (z.1,z.2)) = (@id (X*Y)) by apply/funext; case. -Qed. - -Lemma wedge_prod_open (z : wedge) (A : set wedge) : - closed [set x0] -> closed [set y0] -> - nbhs z A -> nbhs (wedge_prod_fun z) (wedge_prod_fun @` A). -Proof. -move=> clx cly; case: wedge_nbhs_specP => //. -- move=> x ? /=; rewrite nbhsE; case => B [? ? BA]. - exists ((fun x => @exist _ _ (x,y0) (wedge_prodl x)) @` (B `&` ~`[set x0])). - split=> /=; first last. - + move=> ? /= [a] [? ?] <-; exists (wedgel a); first exact: BA. - by rewrite /wedge_prod_fun wedge_funl //; apply: eq_exist. - + exists x; first by split => //; exact/eqP. - by rewrite // /wedge_prod_fun wedge_funl; apply:eq_exist. - exists ((B `&` ~`[set x0]) `*` setT). - by apply: openX; [apply: openI => //; exact: closed_openC | exact: openT]. - rewrite eqEsubset; split; case; case=> a b /= p []. - case=> Ba ax0 _; exists a => //; apply: eq_exist; congr((_,_)). - by move:ax0; have /set_mem [[_ <- //] | [] <-] /= := p. - by move=> l [Bl lNx0] [<-]. -- move=> y ? /=; rewrite nbhsE; case => B [? ? BA]. - exists ((fun y => @exist _ _ (x0,y) (wedge_prodr y)) @` (B `&` ~`[set y0])). - split=> /=; first last. - + move=> ? /= [b] [? ?] <-; exists (wedger b); first exact: BA. - by rewrite /wedge_prod_fun wedge_funr //; apply: eq_exist. - + exists y; first by split => //; exact/eqP. - by rewrite // /wedge_prod_fun wedge_funr; apply:eq_exist. - exists (setT `*` (B `&` ~`[set y0])). - by apply: openX; [exact: openT | apply: openI => //; exact: closed_openC]. - rewrite eqEsubset; split; case; case=> a b /= p []. - move=> _ [Bb by0]; exists b => //; apply: eq_exist; congr((_,_)). - by move:by0; have /set_mem [[_ <- //] | [] <-] /= := p. - by move=> ? [? ?] [_ <-]. -case; rewrite /= ?nbhsE;case=> L [oL Lx LA] [R [oR Ry RA]]. -exists ( ((fun x => @exist _ _ (x,y0) (wedge_prodl x)) @` L) `|` - (fun y => @exist _ _ (x0,y) (wedge_prodr y)) @` R); first last. - case; case=> l r/= p [] /= []? ? [] E1 E2. - exists (wedgel l); first by apply: LA; rewrite -E1. - by rewrite /wedge_prod_fun wedge_funl; apply: eq_exist; rewrite E2. - exists (wedger r); first by apply: RA; rewrite -E2. - by rewrite /wedge_prod_fun wedge_funr; apply: eq_exist; rewrite E1. -split; first last. - by left; exists x0 => //; rewrite /wedge_prod_fun wedge_funl; apply:eq_exist. -exists (L`*` R); first exact: openX. -rewrite eqEsubset; split; case; case=> l r /= p []. -- move=> Ll Rr; have /set_mem [[_] | [+ _]] /= := p. - by move=> E; left; exists l => //; apply: eq_exist; rewrite E. - by move=> E; right; exists r => //; apply: eq_exist; rewrite E. -- by case=> ? ? [<-] <-; split => //. -- by case=> ? ? [<-] <-; split => //. +apply: functional_extensionality_dep => k /=. +case: dfwithP; first case: dfwithP => //. +by move=> i1 iNi1; case: dfwithP => //. Qed. -Lemma wedge_hausdorff : - hausdorff_space X -> - hausdorff_space Y -> - hausdorff_space wedge. +Lemma wedge_prod_fun_inj : injective wedge_prod_fun. Proof. -move=> hX hY a b clab; have [g gK prodK] := wedge_prod_fun_bij. -rewrite -[a]gK -[b]gK; congr(g _). -have := @weak_hausdorff wedge_prod; apply => //. - exact: hausdorff_prod. -move=> U V /wedge_prod_continuous Uwa /wedge_prod_continuous Vwb. -by have [z [/=] ? ?] := clab _ _ (Uwa) (Vwb); exists (wedge_prod_fun z). +have ? := wedge_prod_fun_pointE. +move=> a b; rewrite -[a](@reprK _ wedge) -[b](@reprK _ wedge). +case Ea : (repr a)=> [i x]; case Eb : (repr b) => [j y]. +rewrite /wedge_prod_fun /= ?wedge_fun_wedgei //. +move=> dfij; apply/eqmodP/orP. +case: (pselect (i = j)) => E. + destruct E; left; apply/eqP; congr(_ _). + have : dfwith p0 i x i = dfwith p0 i y i by rewrite dfij. + by rewrite ?dfwithin. +right => /=; apply/andP; split; apply/eqP. + have : dfwith p0 i x i = dfwith p0 j y i by rewrite dfij. + by rewrite dfwithin => ->; rewrite dfwithout // eq_sym; apply/eqP. +have : dfwith p0 i x j = dfwith p0 j y j by rewrite dfij. +by rewrite dfwithin => <-; rewrite dfwithout //; apply/eqP. Qed. -Lemma wedge_comp {Z1 Z2 : topologicalType} (f : Z1 -> Z2) g h : - g x0 = h y0 -> f \o wedge_fun g h = wedge_fun (f \o g) (f \o h). +Lemma wedge_prod_continuous : continuous wedge_prod_fun. Proof. -move=> ghE; apply/funext => z /=; rewrite -[z]reprK /=. -by case E: (repr z); rewrite ?wedge_funl ?wedge_funr //= ghE. -Qed. +apply: wedge_fun_continuous; last exact: wedge_prod_fun_pointE. +exact: dfwith_continuous. +Qed. + +Lemma wedge_prod_open (x : wedge) (A : set wedge) : + finite_set [set: I] -> + (forall i, closed [set p0 i]) -> + nbhs x A -> + @nbhs _ (subspace (range wedge_prod_fun)) (wedge_prod_fun x) (wedge_prod_fun @` A). +Proof. +move=> fsetI clI; case: wedge_nbhs_specP => //. + move=> i0 bcA. + pose B_ i : set ((subspace (range wedge_prod_fun))) := proj i @^-1` (@wedgei i@^-1` A). + have /finite_fsetP [fI fIE] := fsetI. + have : (\bigcap_(i in [set` fI]) B_ i) `&` range wedge_prod_fun `<=` wedge_prod_fun @` A. + move=> ? [] /[swap] [][] z _ <- /= Bwz; exists z => //. + have Iz : [set` fI] (projT1 (repr z)) by rewrite -fIE //. + have := Bwz _ Iz; congr(A _); rewrite /wedgei /= -[RHS]reprK. + apply/eqmodP/orP; left; rewrite /proj /=. + by rewrite /wedge_prod_fun /= /wedge_fun /sum_fun /= dfwithin -sigT_eta. + move/filterS; apply. + apply/nbhs_subspace_ex; first by exists (wedgei (p0 i0)). + exists (\bigcap_(i in [set` fI]) B_ i); last by rewrite -setIA setIid. + apply: filter_bigI => i _. + rewrite /B_; apply: proj_continuous. + (have Ii : [set: I] i by done); have /= := bcA _ Ii; congr(nbhs _ _). + rewrite /proj /wedge_prod_fun. + rewrite wedge_fun_wedgei; last exact: wedge_prod_fun_pointE. + by case: dfwithP. +move=> i z zNp0 /= wNz. +rewrite [x in nbhs x _]/wedge_prod_fun /= wedge_fun_wedgei; first last. + exact: wedge_prod_fun_pointE. +have : wedge_prod_fun @` (A `&` (@wedgei i @` ~`[set p0 i])) `<=` wedge_prod_fun @` A. + by move=> ? [] ? [] + /= [w] wpi => /[swap] <- Aw <-; exists (wedgei w). +move/filterS; apply; apply/nbhs_subspace_ex. + exists (wedgei z) => //. + by rewrite /wedge_prod_fun wedge_fun_wedgei //; exact: wedge_prod_fun_pointE. +exists (proj i @^-1` (@wedgei i @^-1` (A `&` (@wedgei i @` ~`[set p0 i])))). + apply/ proj_continuous; rewrite /proj dfwithin preimage_setI; apply: filterI. + exact: wNz. + have /filterS := @preimage_image _ _ (@wedgei i) (~` [set p0 i]). + apply; apply: open_nbhs_nbhs; split; first exact: closed_openC. + by apply/eqP. +rewrite eqEsubset; split => // ?; case => /[swap] [][] r _ <- /=. + case => ? /[swap] /wedge_prod_fun_inj -> [+ [e /[swap]]] => /[swap]. + move=> <- Awe eNpi; rewrite /proj /wedge_prod_fun /=. + rewrite ?wedge_fun_wedgei; last exact: wedge_prod_fun_pointE. + rewrite dfwithin; split => //; first by (split => //; exists e). + exists (wedgei e) => //. + by rewrite wedge_fun_wedgei //; exact: wedge_prod_fun_pointE. +case=> /[swap] [][y] yNpi E Ay. +case : (pselect (i = (projT1 (repr r)))); first last. + move=> R; move: yNpi; apply: absurd. + move: E; rewrite /proj/wedge_prod_fun /wedge_fun /=/sum_fun /=. + rewrite dfwithout //; last by rewrite eq_sym; apply/eqP. + case/eqmodP/orP; last by case/andP => /= /eqP E. + move=> /eqP => E. + have := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ E; apply. + by move=> a b; case: (pselect (a = b)) => ?; [left | right]. +move=> riE; split; exists (wedgei y) => //. +- by split; [rewrite E | exists y]. +- congr (wedge_prod_fun _); rewrite E. + rewrite /proj /wedge_prod_fun /wedge_fun /=/sum_fun. + by rewrite riE dfwithin /wedgei /= -sigT_eta reprK. +- congr(wedge_prod_fun _); rewrite E . + rewrite /proj /wedge_prod_fun /wedge_fun /=/sum_fun. + by rewrite riE dfwithin /wedgei /= -sigT_eta reprK. +Qed. +End wedge_as_product. +Lemma wedge_hausdorff : + (forall i, hausdorff_space (X i)) -> + hausdorff_space wedge. +Proof. +move=> /hausdorff_product hf => x y clxy. +apply: wedge_prod_fun_inj; apply: hf => U V /wedge_prod_continuous. +move=> nU /wedge_prod_continuous nV; have := clxy _ _ nU nV. +by case => z [/=] ? ?; exists (wedge_prod_fun z). +Qed. End wedge. HB.mixin Record isBiPointed (X : Type) of Equality X := { @@ -1972,36 +1955,40 @@ HB.mixin Record isBiPointed (X : Type) of Equality X := { #[short(type="biPointedType")] HB.structure Definition BiPointed := - { X of Equality X & isBiPointed X }. + { X of Choice X & isBiPointed X }. #[short(type="bpTopologicalType")] HB.structure Definition BiPointedTopological := { X of BiPointed X & Topological X }. -Notation bpwedge X Y := (@wedge X Y one zero). -Notation bpwedgel := (@wedgel _ _ one zero). -Notation bpwedger := (@wedger _ _ one zero). Section bpwedge. -Context {X Y : bpTopologicalType}. - -Local Lemma wedge_neq : bpwedgel zero != bpwedger one :> bpwedge X Y. +Context (X Y : bpTopologicalType). +Definition wedge2 b := if b then X else Y. +Definition wedge2p b := if b return wedge2 b then (@one X) else (@zero Y). +Local Notation bpwedge := (@wedge bool wedge2 wedge2p). +Local Notation bpwedgei := (@wedgei bool wedge2 wedge2p). + +Local Lemma wedge_neq : @bpwedgei true zero != @bpwedgei false one . Proof. -apply/eqP => R; have /eqmodP/orP[/eqP //|/orP [] /andP [//]] := R. -by case/eqP => /eqP + _; apply/negP; apply: zero_one_neq. +apply/eqP => R; have /eqmodP/orP[/eqP //|/andP[ /= + _]] := R. +by have := (@zero_one_neq X) => /[swap] ->. Qed. HB.instance Definition _ := @isBiPointed.Build - (bpwedge X Y) (bpwedgel zero) (bpwedger one) wedge_neq. + bpwedge (@bpwedgei true zero) (@bpwedgei false one) wedge_neq. End bpwedge. +Notation bpwedge X Y := (@wedge bool (wedge2 X Y) (wedge2p X Y)). +Notation bpwedgei X Y := (@wedgei bool (wedge2 X Y) (wedge2p X Y)). + (* Such a structure is very much like [a,b] in that one can split it in half like `[0,1] \/ [0,1] ~ [0,2] ~ [0,1] *) HB.mixin Record isSelfSplit (X : Type) of BiPointedTopological X := { - to_wedge : X -> @wedge X X one zero; - from_wedge : @wedge X X one zero -> X; - to_wedge_zero : to_wedge zero = @wedgel X X one zero zero; - to_wedge_one : to_wedge one = @wedger X X one zero one; + to_wedge : X -> bpwedge X X; + from_wedge : bpwedge X X -> X; + to_wedge_zero : to_wedge zero = zero; + to_wedge_one : to_wedge one = one; to_wedgeK : cancel to_wedge from_wedge; from_wedgeK : cancel from_wedge to_wedge; to_wedge_cts : continuous to_wedge; @@ -2069,8 +2056,10 @@ Section wedge_path. Context {T : topologicalType} {i : selfSplitType} (x y z: T). Context {p : {path i from x to y}} {q : {path i from y to z}}. -Definition path_concat {T : topologicalType} (f g : i -> T) := - wedge_fun f g \o to_wedge. +Check @wedge_fun. +Definition path_concat (f g : i -> T) : i -> T := + wedge_fun (fun b => if b return wedge2 i i b -> T then f else g) \o to_wedge. + Notation "f '<>' g" := (path_concat f g).