From 97d07798ab1fd1889ed707181c06cf98c438e408 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Sun, 17 Nov 2024 11:43:17 -0500 Subject: [PATCH] Wedge fun (#1398) * trying to fix joint continuity * functions on wedges * linting --------- Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 12 +- classical/boolp.v | 16 ++- theories/homotopy_theory/wedge_sigT.v | 197 ++++++++++++++++++++++++-- theories/separation_axioms.v | 2 +- 4 files changed, 212 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6d64c0812..f3151abe6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,7 +88,7 @@ `wedge_compact`, `wedge_connected`. - in `boolp.`: - + lemma `existT_inj` + + lemma `existT_inj2` - in file `order_topology.v` + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and `max_fun_continuous`. @@ -102,6 +102,16 @@ + new lemmas `continuous_curry_fun`, `continuous_curry_cvg`, `eval_continuous`, and `compose_continuous` +- in file `wedge_sigT.v`, ++ new definitions `wedge_fun`, and `wedge_prod`. ++ new lemmas `wedge_fun_continuous`, `wedge_lift_funE`, + `wedge_fun_comp`, `wedge_prod_pointE`, `wedge_prod_inj`, + `wedge_prod_continuous`, `wedge_prod_open`, `wedge_hausdorff`, and + `wedge_fun_joint_continuous`. + +- in `boolp.v`: + + lemmas `existT_inj1`, `surjective_existT` + ### Changed - in file `normedtype.v`, diff --git a/classical/boolp.v b/classical/boolp.v index 5f63c4e63..f1ece5aa2 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -88,13 +88,21 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a. by apply: cid; case: PQA => x; exists x. Qed. -Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) : - existT P p x = existT P p y -> x = y. +Lemma existT_inj1 (T : Type) (P : T -> Type) (x y : T) (Px : P x) (Py : P y) : + existT P x Px = existT P y Py -> x = y. +Proof. by case. Qed. + +Lemma existT_inj2 (T : eqType) (P : T -> Type) (x : T) (Px1 Px2 : P x) : + existT P x Px1 = existT P x Px2 -> Px1 = Px2. Proof. -apply: Eqdep_dec.inj_pair2_eq_dec => a b. -by have [|/eqP] := eqVneq a b; [left|right]. +apply: Eqdep_dec.inj_pair2_eq_dec => y z. +by have [|/eqP] := eqVneq y z; [left|right]. Qed. +Lemma surjective_existT (T : Type) (P : T -> Type) (p : {x : T & P x}): + existT [eta P] (projT1 p) (projT2 p) = p. +Proof. by case: p. Qed. + Record mextensionality := { _ : forall (P Q : Prop), (P <-> Q) -> (P = Q); _ : forall {T U : Type} (f g : T -> U), diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 08625921f..d39fddba0 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2024 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 boolp classical_sets functions. -From mathcomp Require Import cardinality mathcomp_extra fsbigop. -From mathcomp Require Import reals signed topology separation_axioms. -Require Import EqdepFacts. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals signed topology. +From mathcomp Require Import separation_axioms function_spaces. (**md**************************************************************************) (* # wedge sum for sigT *) @@ -19,7 +18,14 @@ Require Import EqdepFacts. (* wedge_lift i == the lifting of elements of (X i) into the wedge *) (* pwedge p0 == the wedge of ptopologicalTypes at their designated *) (* point *) +(* wedge_fun f == lifts a family of functions on each component into *) +(* a function on the wedge, when they all agree at the *) +(* wedge point *) +(* wedge_prod == the mapping from the wedge as a quotient of sums to *) +(* the wedge as a subspace of the product topology. *) +(* It's an embedding when the index is finite. *) (* ``` *) +(* *) (* The type `wedge p0` is endowed with the structures of: *) (* - topology via `quotient_topology` *) (* - quotient *) @@ -108,14 +114,14 @@ have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))). rewrite eqEsubset; split => x /=. by move=> Ux; exists i => //; exists x. case=> j _ /= [] y Uy /eqmodP /predU1P[R|]. - have E : j = i by move: R; exact: eq_sigT_fst. - by rewrite -E in x R *; rewrite -(existT_inj R). + have E : j = i by move: R; apply: existT_inj1. + by rewrite -E in x R *; rewrite -(existT_inj2 R). case/andP => /eqP/= + /eqP -> => yj. by rewrite yj (wedge_liftE x y) in Uy. congr open; rewrite eqEsubset; split => /= z. by case=> i _ /= [x] Ux <-. move=> Uz; exists (projT1 (repr z)) => //=. -by exists (projT2 (repr z)); rewrite /wedge_lift /= -sigT_eta reprK. +by exists (projT2 (repr z)); rewrite /wedge_lift /= surjective_existT reprK. Qed. Lemma wedge_point_nbhs i0 : @@ -135,7 +141,7 @@ exists W; split. - apply/wedge_openP => i; rewrite /W; have [+ Vpj _] := projT2 (V_ i). congr (_ _); rewrite eqEsubset; split => z; first by move=> Viz; exists i. case => j _ /= [] w /= svw /eqmodP /predU1P[[E]|]. - by rewrite E in w svw * => R; rewrite -(existT_inj R). + by rewrite E in w svw * => R; rewrite -(existT_inj2 R). by case/andP => /eqP /= _ /eqP ->. - by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0). - by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact. @@ -159,7 +165,7 @@ Qed. Lemma wedgeTE : \bigcup_i (@wedge_lift i) @` setT = [set: wedge]. Proof. rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. -by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= -sigT_eta. +by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= surjective_existT. Qed. Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> @@ -186,6 +192,179 @@ move=> i ? /=; apply: connected_continuous_connected => //. exact/continuous_subspaceT/wedge_lift_continuous. Qed. +Definition wedge_fun {Z : Type} (f : forall i, X i -> Z) : wedge -> Z := + sigT_fun f \o repr. + +Lemma wedge_fun_continuous {Z : topologicalType} (f : forall i, X i -> Z) : + (forall i, continuous (f i)) -> (forall i j, f i (p0 i) = f j (p0 j)) -> + continuous (wedge_fun f). +Proof. +move=> cf fE; apply: repr_comp_continuous; first exact: sigT_continuous. +move=> a b /eqP/eqmodP /predU1P[-> //|/andP[/eqP + /eqP +]]. +by rewrite /sigT_fun /= => -> ->; exact/eqP. +Qed. + +Lemma wedge_lift_funE {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 (wedge_lift a) = f i0 a. +Proof. +move=> fE. +rewrite /wedge_fun/= /sigT_fun /=; case: piP => z /= /eqmodP. +by move/predU1P => [<- //|/andP[/= /eqP -> /eqP ->]]. +Qed. + +Lemma wedge_fun_comp {Z1 Z2 : Type} (h : Z1 -> Z2) (f : forall i, X i -> Z1) : + h \o wedge_fun f = wedge_fun (fun i => h \o f i). +Proof. exact/funext. Qed. + +(* 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 : wedge -> prod_topology X := wedge_fun (dfwith p0). + +Lemma wedge_prod_pointE (i j : I) : dfwith p0 i (p0 i) = dfwith p0 j (p0 j). +Proof. +apply: functional_extensionality_dep => k /=. +by case: dfwithP => [|*]; case: dfwithP. +Qed. + +Lemma wedge_prod_inj : injective wedge_prod. +Proof. +have dfwithp0 := wedge_prod_pointE. +move=> a b; rewrite -[a](@reprK _ wedge) -[b](@reprK _ wedge). +move Ea : (repr a)=> [i x]; move Eb : (repr b) => [j y]. +rewrite /wedge_prod !wedge_lift_funE//= => dfij; apply/eqmodP/orP. +have [E|E /=] := eqVneq i j. + rewrite -{}E in x y Ea Eb dfij *; left; apply/eqP; congr existT. + 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. +- have : dfwith p0 i x j = dfwith p0 j y j by rewrite dfij. + by rewrite dfwithin => <-; rewrite dfwithout. +Qed. + +Lemma wedge_prod_continuous : continuous wedge_prod. +Proof. +apply: wedge_fun_continuous; last exact: wedge_prod_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)) (wedge_prod x) (wedge_prod @` A). +Proof. +move=> fsetI clI; case: wedge_nbhs_specP => [//|i0 bcA|i z zNp0 /= wNz]. + pose B_ i : set (subspace (range wedge_prod)) := + proj i @^-1` (@wedge_lift i @^-1` A). + have /finite_fsetP[fI fIE] := fsetI. + have /filterS : (\bigcap_(i in [set` fI]) B_ i) `&` range wedge_prod + `<=` wedge_prod @` A. + move=> _ [] /[swap] [] [z _] <- /= Bwz; exists z => //. + have /Bwz : [set` fI] (projT1 (repr z)) by rewrite -fIE. + congr (A _); rewrite /wedge_lift /= -[RHS]reprK. + apply/eqmodP/orP; left; rewrite /proj /=. + by rewrite /wedge_prod/= /wedge_fun /sigT_fun/= dfwithin surjective_existT. + apply; apply/nbhs_subspace_ex; first by exists (wedge_lift (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 /bcA : [set: I] i by []. + congr (nbhs _ _). + rewrite /proj /wedge_prod wedge_lift_funE; first by case: dfwithP. + exact: wedge_prod_pointE. +rewrite [x in nbhs x _]/wedge_prod /= wedge_lift_funE; first last. + exact: wedge_prod_pointE. +have : wedge_prod @` (A `&` (@wedge_lift i @` ~`[set p0 i])) + `<=` wedge_prod @` A. + by move=> ? [] ? [] + /= [w] wpi => /[swap] <- Aw <-; exists (wedge_lift w). +move/filterS; apply; apply/nbhs_subspace_ex. + exists (wedge_lift z) => //. + by rewrite /wedge_prod wedge_lift_funE //; exact: wedge_prod_pointE. +exists (proj i @^-1` (@wedge_lift i @^-1` + (A `&` (@wedge_lift i @` ~`[set p0 i])))). + apply/ proj_continuous; rewrite /proj dfwithin preimage_setI; apply: filterI. + exact: wNz. + have /filterS := @preimage_image _ _ (@wedge_lift i) (~` [set p0 i]). + by apply; apply: open_nbhs_nbhs; split; [exact: closed_openC|exact/eqP]. +rewrite eqEsubset; split => // prodX; case => /[swap] [][] r _ <- /=. + case => _ /[swap] /wedge_prod_inj -> [+ [e /[swap]]] => /[swap]. + move=> <- Awe eNpi; rewrite /proj /wedge_prod /=. + rewrite wedge_lift_funE; last exact: wedge_prod_pointE. + rewrite dfwithin; split => //; first by split => //; exists e. + exists (wedge_lift e) => //. + by rewrite wedge_lift_funE //; exact: wedge_prod_pointE. +case=> /[swap] [][y] yNpi E Ay. +have [riE|R] := eqVneq i (projT1 (repr r)); last first. + apply: absurd yNpi. + move: E; rewrite /proj/wedge_prod /wedge_fun /=/sigT_fun /=. + rewrite dfwithout //; last by rewrite eq_sym. + by case/eqmodP/orP => [/eqP E|/andP[/= /eqP//]]; exact: (existT_inj2 E). +split; exists (wedge_lift y); [by split; [rewrite E | exists y]| |by []|]. +- congr wedge_prod; rewrite E. + rewrite /proj /wedge_prod /wedge_fun /=/sigT_fun. + by rewrite riE dfwithin /wedge_lift /= surjective_existT reprK. +- congr wedge_prod; rewrite E. + rewrite /proj /wedge_prod /wedge_fun /=/sigT_fun. + by rewrite riE dfwithin /wedge_lift /= surjective_existT 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_inj/hf => U V /wedge_prod_continuous nU. +move=> /wedge_prod_continuous nV; have := clxy _ _ nU nV. +by case => z [/= ? ?]; exists (wedge_prod z). +Qed. + +Lemma wedge_fun_joint_continuous (T R : topologicalType) + (k : forall (x : I), T -> X x -> R): + finite_set [set: I] -> + (forall x, closed [set p0 x]) -> + (forall t x y, k x t (p0 x) = k y t (p0 y)) -> + (forall x, continuous (uncurry (k x))) -> + continuous (uncurry (fun t => wedge_fun (k^~ t))). +Proof. +move=> Ifin clp0 kE kcts /= [t u] U. +case : (wedge_nbhs_specP u) => [//|i0 /=|]. + rewrite wedge_lift_funE // => Ukp0. + have pq_ x : {PQ : set T * set (X x) | [/\ nbhs (p0 x) PQ.2, + nbhs t PQ.1 & PQ.1 `*` PQ.2 `<=` uncurry (k x) @^-1` U]}. + apply: cid. + move: Ukp0; rewrite (@kE t i0 x). + rewrite -[k x ]uncurryK /curry=> /kcts[[P Q] [Pt Qp0 pqU]]. + by exists (P, Q). + have UPQ : nbhs (wedge_lift (p0 i0)) + (\bigcup_x (@wedge_lift x) @` (projT1 (pq_ x)).2). + rewrite wedge_point_nbhs => r _. + by case: (projT2 (pq_ r)) => /filterS + ? ?; apply => z /= ?; exists r. + have /finite_fsetP [fI fIE] := Ifin. + have UPt : nbhs t (\bigcap_(r in [set` fI]) (projT1 (pq_ r)).1). + by apply: filter_bigI => x ?; case: (projT2 (pq_ x)). + near_simpl => /=; near=> t1 t2 => /=. + have [//|x _ [w /=] ? <-]:= near UPQ t2. + rewrite wedge_lift_funE //. + case: (projT2 (pq_ x)) => ? Npt /(_ (t1, w)) => /=; apply; split => //. + by apply: (near UPt t1) => //; rewrite -fIE. +move=> x {}u uNp0 /=; rewrite wedge_lift_funE //= -[k x]uncurryK /curry. +move/kcts; rewrite nbhs_simpl /= => -[[P Q] [Pt Qu] PQU]. +have wQu : nbhs (wedge_lift u) ((@wedge_lift x) @` Q). + by rewrite -wedge_lift_nbhs //=; apply: filterS Qu => z; exists z. +near_simpl; near=> t1 t2 => /=. +have [//|l ? <-] := near wQu t2; rewrite wedge_lift_funE//. +by apply: (PQU (t1,l)); split => //; exact: (near Pt t1). +Unshelve. all: by end_near. Qed. + End wedge. Section pwedge. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index afd1f4ad6..c136e2bfd 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1139,7 +1139,7 @@ rewrite {}ji {j} in x y cl *. congr existT; apply: hX => U V Ux Vy. have [] := cl (existT X i @` U) (existT X i @` V); [exact: existT_nbhs..|]. move=> z [] [l Ul <-] [r Vr lr]; exists l; split => //. -by rewrite -(existT_inj lr). +by rewrite -(existT_inj2 lr). Qed. End sigT_separations.