Wedge fun (#1398)

* trying to fix joint continuity

* functions on wedges

* linting

---------

Co-authored-by: Reynald Affeldt <[email protected]>

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`,

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),

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.

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.