diff --git a/theories/topology.v b/theories/topology.v index ece7e588d1..aa0ac8b976 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -1636,30 +1636,30 @@ Lemma near_powerset_map {T U : Type} (f : T -> U) (F : set (set T)) Proof. move=> FF [] G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from F). - by apply: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD. near=> M; apply: GP; apply: (Gs D) => //. apply: filterS; first exact: preimage_image. - by apply: (near (near_small_set _) M). -have : M `<=` f @^-1` D by apply: (near (small_set_sub FfD) M). -by move/image_subset/subset_trans; apply; apply: image_preimage_subset. + exact: (near (near_small_set _) M). +have : M `<=` f @^-1` D by exact: (near (small_set_sub FfD) M). +by move/image_subset/subset_trans; apply; exact: image_preimage_subset. Unshelve. all: by end_near. Qed. -Lemma near_map_powerset {T U : Type} (f : T -> U) (F : set (set T)) +Lemma near_powerset_map_monoE {T U : Type} (f : T -> U) (F : set (set T)) (P : (set U) -> Prop) : (forall X Y, X `<=` Y -> P Y -> P X) -> ProperFilter F -> - (\forall y \near powerset_filter_from F, P (f @` y)) -> + (\forall y \near powerset_filter_from F, P (f @` y)) = (\forall y \near powerset_filter_from (f x @[x --> F]), P y). Proof. -move=> Psub FF [] G /= [Gf Gs [D GD GP]]. +move=> Pmono FF; rewrite propeqE; split; last exact: near_powerset_map. +case=> G /= [Gf Gs [D GD GP]]. have PpF : ProperFilter (powerset_filter_from (f x @[x-->F])). - by apply: powerset_filter_from_filter. -have /= := Gf _ GD; rewrite nbhs_simpl => FfD. -have ffiD : fmap f F (f@` D). + exact: powerset_filter_from_filter. +have /= := Gf _ GD; rewrite nbhs_simpl => FfD; have ffiD : fmap f F (f@` D). by rewrite /fmap /=; apply: filterS; first exact: preimage_image. -near=> M; have FfM : (fmap f F M) by apply (near (near_small_set _) M). -apply: (@Psub _ (f@`D)); first exact: (near (small_set_sub ffiD) M). +near=> M; have FfM : (fmap f F M) by exact: (near (near_small_set _) M). +apply: (@Pmono _ (f@`D)); first exact: (near (small_set_sub ffiD) M). exact: GP. Unshelve. all: by end_near. Qed. @@ -2449,8 +2449,7 @@ Lemma fst_open {U V : topologicalType} (A : set (U * V)) : Proof. rewrite ?openE=> oA z [[a b/=] Aab <-]; rewrite /interior. have [[P Q] [Pa ?] pqA] := oA _ Aab; apply: (@filterS _ _ _ P) => //. -move=> p Pp; exists (p, b) => //; apply: pqA; split => //. -exact: nbhs_singleton. +by move=> p ?; exists (p, b); [apply: pqA; split|]; [|exact: nbhs_singleton|]. Qed. Lemma snd_open {U V : topologicalType} (A : set (U * V)) : @@ -3058,17 +3057,10 @@ Definition near_covering_within (K : set X) := Lemma near_covering_withinP (K : set X): near_covering_within K <-> near_covering K. Proof. -split. - move=> cvrW I F P FF cvr. - near=> i; suff : K `<=` (fun q : X => K q -> P i q). - by move=> KKP k Kk; apply: KKP. - near: i; apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app. - by near=> j => /=. -move=> cvrW I F P FF cvr. -near=> i; suff : K `<=` (fun q : X => K q -> P i q). - by move=> KKP k Kk; apply: KKP. -near: i. -have := (cvrW I F (fun i q => K q -> P i q) FF). +split; move=> cvrW I F P FF cvr; near=> i; + (suff : K `<=` fun q : X => K q -> P i q by move=> + k Kk; apply); near: i. + by apply: cvrW=> x Kx; move: (cvr x Kx); apply: filter_app; near=> j. +have := (cvrW _ _ (fun i q => K q -> P i q) FF). apply => x Kx; have := cvr x Kx; apply: filter_app. by near=> j => + ?; apply. Unshelve. all: by end_near. Qed. @@ -3082,12 +3074,11 @@ rewrite ?compact_near_coveringP => cptP cptQ I F Pr Ff cvfPQ. have := cptP I F (fun i u => forall q, Q q -> Pr i (u,q)) Ff. set R := (R in (R -> _) -> _); suff R' : R. by move/(_ R'); apply:filter_app; near=> i => + [a b] [Pa Qb]; apply. -rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)). -move=> v Qv. +rewrite /R => x Px; apply: (@cptQ _ (filter_prod _ _)) => v Qv. case: (cvfPQ (x,v)) => // [[N G]] /= [[[N1 N2 /= [N1x N2v]]]] N1N2N FG ngPr. exists (N2,(N1`*`G)); first by split => //; exists (N1, G) => //. case=> a [b i] /= [? [?]] ?. -by apply: (ngPr (b,a, i)); split => //; apply: N1N2N. +by apply: (ngPr (b,a, i)); split => //; exact: N1N2N. Unshelve. all: by end_near. Qed. Section Tychonoff. @@ -6621,7 +6612,7 @@ Unshelve. all: by end_near. Qed. (* It turns out {family compact, U -> V} can be generalized to only assume *) (* `topologicalType` on V. This topology is called the compact-open topology. *) -(* This topology is special becaise it _only_ topology that will allow *) +(* This topology is special becaise it is the _only_ topology that will allow *) (* curry/uncurry to be continuous. *) Section compact_open. @@ -6648,7 +6639,7 @@ apply: filter_from_filter; first by exists setT; split => //; exact: openT. move=> P Q [fKP oP] [fKQ oQ]; exists (P `&` Q); first split. - by move=> ? [z Kz M-]; split; [apply: fKP | apply: fKQ]; exists z. - exact: openI. -by move=> g /= gPQ; split; apply: (subset_trans gPQ) => ? []. +by move=> g /= gPQ; split; exact: (subset_trans gPQ) => ? []. Qed. Program Definition compact_openK_topological_mixin : @@ -6659,7 +6650,7 @@ Next Obligation. move=> f; rewrite eqEsubset; split => A /=. case=> B /= [fKB oB gKBA]; exists [set g | g @` K `<=` B]; split => //. by move=> h /= hKB; exists B. -by case=> B [oB Bf /filterS]; apply; apply: oB. +by case=> B [oB Bf /filterS]; apply; exact: oB. Qed. Next Obligation. done. Qed. @@ -8408,7 +8399,7 @@ move=> z /= clEz; apply: ER; apply: subset_split_ent => //. have [] := clEz (to_set (E' `&` E'^-1%classic) z). rewrite -nbhs_entourageE; exists (E' `&` E'^-1%classic) => //. exact: filterI. -move=> y /= [[? ?]] [? ?]; exists y => //. +by move=> y /= [[? ?]] [? ?]; exists y. Qed. #[global] Hint Resolve uniform_regular : core. @@ -8418,17 +8409,39 @@ Local Notation "U '~>' V" := ({compact-open, [topologicalType of U] -> [topologicalType of V]}) (at level 99, right associativity). +Section cartesian_closed. Context {U V W : topologicalType}. +(* In this section, we consider under what conditions + [f in U ~> V ~> W | continuous f /\ forall u, continuous (f u)] + and + [f in U * V ~> W | continuous f] + are homeomorphic + - Always: + curry sends cts functions to cts functions + - V locally_compact + regular or hausdorff + uncurry sends cts functions to cts functions + - U regular or hausdorff + curry itself is a continuous map + - U regular or hausdorff AND V locally_compact + regular or hausdorff + uncurry itself is a continuous map + Therefore curry/uncurry are homeomorphisms + So the category of locally compact regular spaces is cartesian closed +*) + Lemma continuous_curry (f : U * V ~> W) : - continuous f -> continuous (curry f : (U ~> V ~> W)). + continuous f -> + continuous (curry f : (U ~> V ~> W)) /\ forall u, continuous (curry f u). Proof. -move=> ctsf x; apply/compact_open_cvgP => K O /= cptK oO fKO. +move=> ctsf; split; first last. + move=> u z; apply: continuous_comp; last exact: ctsf. + by apply: cvg_pair => //=; exact: cvg_cst. +move=> x; apply/compact_open_cvgP => K O /= cptK oO fKO. near=> z => w /= [+ + <-]; near: z. move/compact_near_coveringP/near_covering_withinP: cptK; apply. move=> v Kv; have [[P Q] [Px Qv] PQfO]: nbhs (x,v) (f@^-1` O). by apply: ctsf; move: oO; rewrite openE; apply; apply: fKO; exists v. -by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; apply: PQfO. +by exists (Q,P); [split => // |]; case=> b a /= [Qb Pa] Kb; exact: PQfO. Unshelve. all: by end_near. Qed. Lemma continuous_uncurry_regular (f : U ~> V ~> W): @@ -8437,7 +8450,7 @@ Lemma continuous_uncurry_regular (f : U ~> V ~> W): Proof. move=> lcV reg cf cfp /= [u v] D; rewrite /= nbhsE; case=> O [oO Ofuv] /filterS. apply; have [B] := @lcV v I; rewrite withinET; move=> Bv [cptB clB]. -have [R Rv RO] : exists2 R, nbhs v R & (forall z, closure R z -> O (f u z)). +have [R Rv RO] : exists2 R, nbhs v R & forall z, closure R z -> O (f u z). have [] := reg v ((f u)@^-1` O); first by apply: cfp; exact: open_nbhs_nbhs. by move=> R ? ?; exists R. exists (f @^-1` ([set g | g @` (B `&` closure R) `<=` O]), (B `&` closure R)). @@ -8470,7 +8483,7 @@ have [] := fKD (curry f u); first by exists u. move=> E /[dup]/[swap]/OfinIo [N Asub <- DIN INf]. suff : \forall x' \near u & i \near nbhs f, K x' -> (\bigcap_(i in [set` N]) i) (curry i x'). - apply: filter_app; near=> a b => + Ka => /(_ Ka) => ?. + apply: filter_app; near=> a b => /[apply] ?. by exists (\bigcap_(i in [set` N]) i). apply: filter_bigI_within=> R RN; have /set_mem [[M cptM _]] := Asub _ RN. have Rfu : R (curry f u) by exact: INf. @@ -8503,9 +8516,10 @@ Proof. move=> lcV regV regU ctsf ctsfp; apply/compact_open_cvgP. by apply: fmap_filter; exact:nbhs_filter. move=> /= K O cptK oO fKO; near=> h => ? [+ + <-]; near: h. -move/compact_near_coveringP/near_covering_withinP : (cptK); apply. +move/compact_near_coveringP/near_covering_withinP: (cptK); apply. case=> u v Kuv. -have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. +have : exists P Q, [/\ closed P, compact Q, nbhs u P, + nbhs v Q & P `*` Q `<=` uncurry f @^-1` O]. have : continuous (uncurry f) by apply: continuous_uncurry_regular. move/continuousP/(_ _ oO); rewrite openE => /(_ (u,v)) []. by apply: fKO; exists (u,v). @@ -8521,12 +8535,11 @@ have : exists P Q, [/\ closed P, compact Q, nbhs u P, nbhs v Q & P `*` Q `<=` un case=> P [Q [clP cptQ Pu Qv PQfO]]; pose R := [set g : V ~> W | g @` Q `<=` O]. (have oR : open R by exact: compact_open_open); pose P' := f@^-1` R. pose L := [set h : U ~> V ~> W | h @` (fst @` K `&` P) `<=` R]. -exists (((P`&` P') `*` Q), L). - split => /=. - exists (P `&` P', Q) => //; split => //=; apply: filterI => //. - apply: ctsf; apply: open_nbhs_nbhs; split => // ? [b ? <-]. - by apply: (PQfO (u,b)); split => //; exact: nbhs_singleton. - rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. +exists (((P`&` P') `*` Q), L); first split => /=. +- exists (P `&` P', Q) => //; split => //=; apply: filterI => //. + apply: ctsf; apply: open_nbhs_nbhs; split => // ? [b ? <-]. + by apply: (PQfO (u,b)); split => //; exact: nbhs_singleton. +- rewrite nbhs_simpl /=; apply: open_nbhs_nbhs; split. apply: compact_open_open => //; apply: compact_closedI => //. apply: continuous_compact => //; apply: continuous_subspaceT => ?. exact: cvg_fst. @@ -8536,4 +8549,4 @@ case; case => a b h [/= [[? ?] ? Lh] ?]. apply: (Lh (h a)); first by exists a => //; split => //; exists (a,b). by exists b. Unshelve. all: by end_near. Qed. -End currying. +End cartesian_closed.