diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d48bcd8dc..4450c6f19 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -77,6 +77,18 @@ + new lemmas `swap_continuous`, `prodA_continuous`, and `prodAr_continuous`. +- file `homotopy_theory/homotopy.v` +- file `homotopy_theory/wedge_sigT.v` +- in file `homotopy_theory/wedge_sigT.v` + + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`. + + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`, + `wedge_liftE`, `wedge_openP`, + `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, + `wedge_compact`, `wedge_connected`. + +- in `boolp.`: + + lemma `existT_inj` + ### Changed - in file `normedtype.v`, diff --git a/_CoqProject b/_CoqProject index b72bbf69d..e36c71dae 100644 --- a/_CoqProject +++ b/_CoqProject @@ -61,6 +61,9 @@ theories/topology_theory/quotient_topology.v theories/topology_theory/one_point_compactification.v theories/topology_theory/sigT_topology.v +theories/homotopy_theory/homotopy.v +theories/homotopy_theory/wedge_sigT.v + theories/separation_axioms.v theories/function_spaces.v theories/ereal.v diff --git a/classical/boolp.v b/classical/boolp.v index ab36ee72c..07b4c2e09 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -88,6 +88,13 @@ 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. +Proof. +apply: Eqdep_dec.inj_pair2_eq_dec => a b. +by have [|/eqP] := eqVneq a b; [left|right]. +Qed. + Record mextensionality := { _ : forall (P Q : Prop), (P <-> Q) -> (P = Q); _ : forall {T U : Type} (f g : T -> U), diff --git a/theories/Make b/theories/Make index 787082052..0d77fa421 100644 --- a/theories/Make +++ b/theories/Make @@ -29,6 +29,9 @@ topology_theory/quotient_topology.v topology_theory/one_point_compactification.v topology_theory/sigT_topology.v +homotopy_theory/homotopy.v +homotopy_theory/wedge_sigT.v + separation_axioms.v function_spaces.v cantor.v diff --git a/theories/homotopy_theory/homotopy.v b/theories/homotopy_theory/homotopy.v new file mode 100644 index 000000000..33e29737b --- /dev/null +++ b/theories/homotopy_theory/homotopy.v @@ -0,0 +1,2 @@ +(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Export wedge_sigT. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v new file mode 100644 index 000000000..08625921f --- /dev/null +++ b/theories/homotopy_theory/wedge_sigT.v @@ -0,0 +1,202 @@ +(* 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. + +(**md**************************************************************************) +(* # wedge sum for sigT *) +(* A foundational construction for homotopy theory. It glues a dependent sum *) +(* at a single point. It's classicaly used in the proof that every free group *) +(* is a fundamental group of some space. We also will use it as part of our *) +(* construction of paths and path concatenation. *) +(* ``` *) +(* wedge_rel p0 x y == x and y are equal, or they are (p0 i) and *) +(* (p0 j) for some i and j *) +(* wedge p0 == the quotient of {i : X i} along `wedge_rel p0` *) +(* wedge_lift i == the lifting of elements of (X i) into the wedge *) +(* pwedge p0 == the wedge of ptopologicalTypes at their designated *) +(* point *) +(* ``` *) +(* The type `wedge p0` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* *) +(* The type `pwedge` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* - pointed *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +Section wedge. +Context {I : choiceType} (X : I -> topologicalType) (p0 : forall i, X i). +Implicit Types i : I. + +Let wedge_rel' (a b : {i & X i}) := + (a == b) || ((projT2 a == p0 _) && (projT2 b == p0 _)). + +Local Lemma wedge_rel_refl : reflexive wedge_rel'. +Proof. by move=> ?; rewrite /wedge_rel' eqxx. Qed. + +Local Lemma wedge_rel_sym : symmetric wedge_rel'. +Proof. +by move=> a b; apply/is_true_inj/propext; rewrite /wedge_rel'; split; + rewrite (eq_sym b) andbC. +Qed. + +Local Lemma wedge_rel_trans : transitive wedge_rel'. +Proof. +move=> a b c /predU1P[-> //|] + /predU1P[<- //|]; rewrite /wedge_rel'. +by move=> /andP[/eqP -> /eqP <-] /andP[_ /eqP <-]; rewrite !eqxx orbC. +Qed. + +Definition wedge_rel := EquivRel _ wedge_rel_refl wedge_rel_sym wedge_rel_trans. +Global Opaque wedge_rel. + +Definition wedge := {eq_quot wedge_rel}. +Definition wedge_lift 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 wedge_lift_continuous i : continuous (@wedge_lift i). +Proof. by move=> ?; apply: continuous_comp => //; exact: pi_continuous. Qed. + +HB.instance Definition _ i := + @isContinuous.Build _ _ (@wedge_lift i) (@wedge_lift_continuous i). + +Lemma wedge_lift_nbhs i (x : X i) : + closed [set p0 i] -> x != p0 _ -> @wedge_lift i @ x = nbhs (@wedge_lift _ x). +Proof. +move=> clx0 xNx0; rewrite eqEsubset; split => U; first last. + by move=> ?; exact: wedge_lift_continuous. +rewrite ?nbhsE /= => -[V [oV Vx VU]]. +exists (@wedge_lift i @` (V `&` ~` [set p0 i])); first last. + by move=> ? /= [l] [Vl lx] <-; exact: VU. +split; last by exists x => //; split => //=; exact/eqP. +rewrite /open /= /quotient_open /wedge_lift /=. +suff -> : \pi_wedge @^-1` (@wedge_lift i @` (V `&` ~`[set p0 i])) = + existT X i @` (V `&` ~` [set p0 i]). + by apply: existT_open_map; apply: openI => //; exact: closed_openC. +rewrite eqEsubset; split => t /= [l [Vl] lNx0]; last by move=> <-; exists l. +by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l. +Qed. + +Lemma wedge_liftE i (x : X i) j (y : X j) : + wedge_lift (p0 j) = wedge_lift (p0 i). +Proof. by apply/eqmodP/orP; right; rewrite !eqxx. Qed. + +Lemma wedge_openP (U : set wedge) : + open U <-> forall i, open (@wedge_lift i @^-1` U). +Proof. +split=> [oU i|oiU]. + by apply: open_comp => // x _; exact: wedge_lift_continuous. +have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))). + apply/sigT_openP => i; move: (oiU i); congr open. + 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). + 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. +Qed. + +Lemma wedge_point_nbhs i0 : + nbhs (wedge_lift (p0 i0)) = \bigcap_i (@wedge_lift i @ p0 i). +Proof. +rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl. + case=> V [/= oV Vp] VU j _; apply: wedge_lift_continuous. + apply: (filterS VU); first exact: (@nbhs_filter wedge). + apply: open_nbhs_nbhs; split => //. + by rewrite (wedge_liftE (p0 i0)). +move=> Uj; have V_ : forall i, {V : set (X i) | + [/\ open V, V (p0 i) & V `<=` @wedge_lift i @^-1` U]}. + move=> j; apply: cid; have /Uj : [set: I] j by []. + by rewrite nbhsE /= => -[B [? ? ?]]; exists B. +pose W := \bigcup_i (@wedge_lift i) @` (projT1 (V_ i)). +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 case/andP => /eqP /= _ /eqP ->. +- by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0). +- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact. +Qed. + +Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := + | wedge_liftsPoint i0 : + wedge_nbhs_spec z (wedge_lift (p0 i0)) (\bigcap_i (@wedge_lift i @ p0 i)) + | WedgeNotPoint (i : I) (x : X i) of (x != p0 i): + wedge_nbhs_spec z (wedge_lift x) (@wedge_lift i @ x). + +Lemma wedge_nbhs_specP (z : wedge) : (forall i, closed [set p0 i]) -> + wedge_nbhs_spec z z (nbhs z). +Proof. +move=> clP; rewrite -[z](@reprK _ wedge); case: (repr z) => i x. +have [->|xpi] := eqVneq x (p0 i). + by rewrite wedge_point_nbhs => /=; exact: wedge_liftsPoint. +by rewrite /= -wedge_lift_nbhs //; exact: WedgeNotPoint. +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. +Qed. + +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. +exact/continuous_subspaceT/wedge_lift_continuous. +Qed. + +Lemma wedge_connected : (forall i, connected [set: X i]) -> + connected [set: wedge]. +Proof. +move=> ctdX; rewrite -wedgeTE. +have [I0|/set0P[i0 Ii0]] := eqVneq [set: I] set0. + rewrite [X in connected X](_ : _ = set0); first exact: connected0. + by rewrite I0 bigcup_set0. +apply: bigcup_connected. + exists (@wedge_lift i0 (p0 _)) => i Ii; exists (p0 i) => //. + exact: wedge_liftE. +move=> i ? /=; apply: connected_continuous_connected => //. +exact/continuous_subspaceT/wedge_lift_continuous. +Qed. + +End wedge. + +Section pwedge. +Context {I : pointedType} (X : I -> ptopologicalType). + +Definition pwedge := wedge (fun i => @point (X i)). + +Let pwedge_point : pwedge := wedge_lift _ (@point (X (@point I))). + +HB.instance Definition _ := Topological.on pwedge. +HB.instance Definition _ := Quotient.on pwedge. +HB.instance Definition _ := isPointed.Build pwedge pwedge_point. + +End pwedge. diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v index ff6f7702c..afd1f4ad6 100644 --- a/theories/separation_axioms.v +++ b/theories/separation_axioms.v @@ -1114,12 +1114,11 @@ Lemma perfectTP_ex {T} : perfect_set [set: T] <-> forall (U : set T), open U -> U !=set0 -> exists x y, [/\ U x, U y & x != y] . Proof. -apply: iff_trans; first exact: perfectTP; split. +apply: (iff_trans perfectTP); split. move=> nx1 U oU [] x Ux; exists x. have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1. - apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset. - (split => //; last by move=> ? ->); move=> y Uy; have /not_and3P := Uyx y. - by case => // /negP; rewrite negbK => /eqP ->. + apply: contra_notP => /not_existsP/contrapT=> Uyx; rewrite eqEsubset. + by split => [y Uy|? ->//]; have /not_and3P[//|//|/negP/negPn/eqP] := Uyx y. move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x. by move=> y [] ? [->] -> /eqP. Qed. @@ -1140,8 +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 => //. -rewrite (Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ lr)// in Vr. -by move=> a b; exact: pselect. +by rewrite -(existT_inj lr). Qed. End sigT_separations.