From 391d42dc7df53c61f92d0599694db28f5afa7e03 Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 6 Nov 2024 13:45:53 -0500 Subject: [PATCH 1/6] wedges_part1 --- CHANGELOG_UNRELEASED.md | 8 ++ _CoqProject | 3 + theories/Make | 3 + theories/homotopy_theory/homotopy.v | 2 + theories/homotopy_theory/wedge_sigT.v | 192 ++++++++++++++++++++++++++ 5 files changed, 208 insertions(+) create mode 100644 theories/homotopy_theory/homotopy.v create mode 100644 theories/homotopy_theory/wedge_sigT.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d48bcd8dc..68ac0454b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -77,6 +77,14 @@ + 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`, `wedgei` + + new lemmas `wedgei_continuous`, `wedgei_nbhs`, `wedge_openP`, + `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, + `wedge_compact`, `wedge_connected`. + ### 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/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..310410438 --- /dev/null +++ b/theories/homotopy_theory/homotopy.v @@ -0,0 +1,2 @@ + +From mathcomp Require Export wedge_sigT. \ No newline at end of file diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v new file mode 100644 index 000000000..83a7cf222 --- /dev/null +++ b/theories/homotopy_theory/wedge_sigT.v @@ -0,0 +1,192 @@ +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` *) +(* wedgei i == the lifting of elements of (X i) into the wedge *) +(* *) +(* The structure `wedge p0` is endowed with the structures of: *) +(* - topology via `quotient_topology` *) +(* - quotient *) +(* *) +(******************************************************************************) + +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). + +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. move=> a b. +suff : (is_true (wedge_rel' a b) <-> is_true (wedge_rel' b a)). + case: (wedge_rel' a b) => //; case: (wedge_rel' b a) => // []. + by case=> ->. + by case=> _ ->. +by split; rewrite /wedge_rel'=> /orP [/eqP -> // /[!eqxx] //|] /andP [] /eqP ->; + move=> /eqP ->; rewrite ?eqxx /= orbT. +Qed. + +Local Lemma wedge_rel_trans : transitive wedge_rel'. +Proof. +move=> a b c /orP [/eqP -> //|] + /orP [ /eqP <- // |]. +rewrite /wedge_rel'; case/andP=> /eqP -> /eqP <- /andP [] /eqP _ ->. +by apply/orP; right; rewrite eqxx. +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 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). +Proof. by move=> ?; apply: continuous_comp => //; exact: pi_continuous. Qed. + +HB.instance Definition _ (i : I) := @isContinuous.Build _ _ + (@wedgei i) (@wedgei_continuous i). + +Lemma wedgei_nbhs (i : I) (x : X i) : + closed [set p0 i] -> x != p0 _ -> (@wedgei i) @ x = nbhs (@wedgei _ x). +Proof. +move=> clx0 xNx0; rewrite eqEsubset; split => U; first last. + by move=> ?; apply: wedgei_continuous. +rewrite ?nbhsE /=; case => V [oV Vx VU]. +exists ((@wedgei i) @` (V `&` ~`[set p0 i])); first last. + by move=> ? /= [l] [Vl lx] <-; apply: VU. +split; last by exists x => //; split => //=; apply/eqP. +rewrite /open /= /quotient_open /wedgei /=. +suff -> : \pi_wedge @^-1` ((@wedgei 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. +case/eqmodP/orP => [/eqP <- |]; first by exists l. +by move=> /= /andP [/eqP]; move: lNx0 => /[swap] ->. +Qed. + +Lemma wedge_openP (U : set wedge) : + open U <-> (forall i, open (@wedgei i @^-1` U)). +Proof. +split. + move=> oU i; apply: open_comp => // ? _. + by apply: continuous_comp => //; exact: pi_continuous. +move=> oiU. +have : open (\bigcup_i (@wedgei i @` (@wedgei 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 /orP [/eqP R|]. + have E : j = i by move: R; apply: eq_sigT_fst. + move: x R; rewrite -E => x R; move: Uy; congr(U (_ _)); move: R. + apply: Eqdep_dec.inj_pair2_eq_dec. + by move => p q; case: (pselect (p = q)) => ?; [left | right]. + case/andP=> /eqP/= + /eqP ->; move: Uy => /[swap] ->; congr(_ _). + by apply/eqmodP; apply/orP; right; rewrite ?eqxx. +congr(open _); rewrite eqEsubset; split => /= z. + by case=> i _ /= [x] Ux <-. +move=> Uz; exists (projT1 (repr z)) => //=. +by exists (projT2 (repr z)); rewrite /wedgei /= -?sigT_eta ?reprK. +Qed. + +Lemma wedge_pointE i j : existT _ i (p0 i) = existT _ j (p0 j) %[mod wedge]. +Proof. by apply/eqmodP; apply/orP; right; rewrite ?eqxx. Qed. + +Lemma wedge_point_nbhs i0 : + nbhs (wedgei (p0 i0)) = \bigcap_i ((@wedgei i) @ p0 i). +Proof. +rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl. + case=> V [/= oV Vp] VU j _; apply: wedgei_continuous. + move/filterS: VU; apply => //; first exact: (@nbhs_filter wedge). + apply: open_nbhs_nbhs; split => //; move: Vp; congr( _ _). + by rewrite /wedgei /=; exact: wedge_pointE. +move=> Uj; have V_ : forall i, {V : set (X i) | + [/\ open V, V (p0 i) & V `<=` (@wedgei i) @^-1` U]}. + (move=> j; have Ij : [set: I] j by done); apply: cid. + by move: (Uj _ Ij); rewrite nbhsE /=; case=> B [? ? ?]; exists B. +pose W := \bigcup_i (@wedgei 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 /orP [/eqP [E]| ]. + move: w svw; rewrite E => w svw R. + have <- // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ R. + by move=> a b; case: (pselect (a = b)) => ?; [left | right]. + by case/andP=> /eqP /= _ /eqP ->. +- by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0). +- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); apply. +Qed. + +Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := + | WedgeIsPoint i0 : + wedge_nbhs_spec z (wedgei (p0 i0)) (\bigcap_i ((@wedgei i) @ p0 i)) + | WedgeNotPoint (i : I) (x : X i) of (x != p0 i): + wedge_nbhs_spec z (wedgei x) (@wedgei 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). +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 wedgeTE : \bigcup_i (@wedgei i) @` setT = [set: wedge]. +Proof. +rewrite -subTset=> z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. +by exists (projT2 (repr z)); rewrite // reprK /wedgei /= -sigT_eta reprK. +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. +by apply: continuous_subspaceT; exact: wedgei_continuous. +Qed. + +Lemma wedge_connected : (forall i, connected [set: X i]) -> + connected [set: wedge]. +Proof. +move=> ctdX; rewrite -wedgeTE. +case: (pselect ([set: I] !=set0)); first last. + move=> I0; have := @connected0 (wedge); congr (_ _). + by rewrite eqEsubset; split => ? // [] x ?; move: I0; apply: absurd; exists x. +case=> i0 Ii0; apply: bigcup_connected. + exists (@wedgei i0 (p0 _)) => i Ii; exists (p0 i) => //. + by rewrite /wedgei /=; apply/eqmodP; apply/orP; right; rewrite ?eqxx. +move=> i ? /=; apply: connected_continuous_connected => //. +by exact/continuous_subspaceT/wedgei_continuous. +Qed. + +End wedge. From f889f1da40f800be2bd0eebb0d8bc9aec4045e7e Mon Sep 17 00:00:00 2001 From: zstone Date: Wed, 6 Nov 2024 13:56:55 -0500 Subject: [PATCH 2/6] pwedge --- CHANGELOG_UNRELEASED.md | 2 +- theories/homotopy_theory/wedge_sigT.v | 30 ++++++++++++++++++++++----- 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 68ac0454b..8482e41f3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -80,7 +80,7 @@ - file `homotopy_theory/homotopy.v` - file `homotopy_theory/wedge_sigT.v` - in file `homotopy_theory/wedge_sigT.v` - + new definitions `wedge_rel`, `wedge`, `wedgei` + + new definitions `wedge_rel`, `wedge`, `wedgei`, `pwedge`. + new lemmas `wedgei_continuous`, `wedgei_nbhs`, `wedge_openP`, `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, `wedge_compact`, `wedge_connected`. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 83a7cf222..b42173c18 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -12,15 +12,22 @@ Require Import EqdepFacts. (* 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` *) -(* wedgei i == the lifting of elements of (X i) into the wedge *) +(* 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` *) +(* wedgei i == the lifting of elements of (X i) into the wedge *) +(* pwedge p0 == the wedge of ptopologicalTypes at their designated *) +(* point *) (* *) -(* The structure `wedge p0` is endowed with the structures of: *) +(* 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. @@ -190,3 +197,16 @@ by exact/continuous_subspaceT/wedgei_continuous. Qed. End wedge. + +Section pwedge. +Context {I : pointedType} (X : I -> ptopologicalType). + +Definition pwedge := wedge (fun i => @point (X i)). + +Let pwedge_point : pwedge := wedgei _ (@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. From 3ea21feb77df7d39c916e5bb2bf0088a38330e2a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 9 Nov 2024 17:48:25 +0900 Subject: [PATCH 3/6] add existT_inj, shorten --- CHANGELOG_UNRELEASED.md | 3 + classical/boolp.v | 7 ++ theories/homotopy_theory/homotopy.v | 4 +- theories/homotopy_theory/wedge_sigT.v | 152 ++++++++++++-------------- theories/separation_axioms.v | 10 +- 5 files changed, 87 insertions(+), 89 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 8482e41f3..73365b0c3 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -85,6 +85,9 @@ `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/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/homotopy_theory/homotopy.v b/theories/homotopy_theory/homotopy.v index 310410438..33e29737b 100644 --- a/theories/homotopy_theory/homotopy.v +++ b/theories/homotopy_theory/homotopy.v @@ -1,2 +1,2 @@ - -From mathcomp Require Export wedge_sigT. \ No newline at end of file +(* 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 index b42173c18..56cc5e977 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,3 +1,4 @@ +(* 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. @@ -11,14 +12,14 @@ Require Import EqdepFacts. (* 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. *) +(* (p0 j) for some i and j *) (* wedge p0 == the quotient of {i : X i} along `wedge_rel p0` *) (* wedgei 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 *) @@ -40,117 +41,107 @@ 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}) := +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. move=> a b. -suff : (is_true (wedge_rel' a b) <-> is_true (wedge_rel' b a)). - case: (wedge_rel' a b) => //; case: (wedge_rel' b a) => // []. - by case=> ->. - by case=> _ ->. -by split; rewrite /wedge_rel'=> /orP [/eqP -> // /[!eqxx] //|] /andP [] /eqP ->; - move=> /eqP ->; rewrite ?eqxx /= orbT. +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 /orP [/eqP -> //|] + /orP [ /eqP <- // |]. -rewrite /wedge_rel'; case/andP=> /eqP -> /eqP <- /andP [] /eqP _ ->. -by apply/orP; right; rewrite eqxx. +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 wedgei (i : I) : X i -> wedge := \pi_wedge \o (existT X i). +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). +Lemma wedgei_continuous i : continuous (@wedgei i). Proof. by move=> ?; apply: continuous_comp => //; exact: pi_continuous. Qed. -HB.instance Definition _ (i : I) := @isContinuous.Build _ _ - (@wedgei i) (@wedgei_continuous i). +HB.instance Definition _ i := + @isContinuous.Build _ _ (@wedgei i) (@wedgei_continuous i). -Lemma wedgei_nbhs (i : I) (x : X i) : +Lemma wedgei_nbhs i (x : X i) : closed [set p0 i] -> x != p0 _ -> (@wedgei i) @ x = nbhs (@wedgei _ x). Proof. move=> clx0 xNx0; rewrite eqEsubset; split => U; first last. - by move=> ?; apply: wedgei_continuous. -rewrite ?nbhsE /=; case => V [oV Vx VU]. -exists ((@wedgei i) @` (V `&` ~`[set p0 i])); first last. - by move=> ? /= [l] [Vl lx] <-; apply: VU. -split; last by exists x => //; split => //=; apply/eqP. + by move=> ?; exact: wedgei_continuous. +rewrite ?nbhsE /= => -[V [oV Vx VU]]. +exists (@wedgei 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 /wedgei /=. -suff -> : \pi_wedge @^-1` ((@wedgei i) @` (V `&` ~`[set p0 i])) = - (existT X i) @` (V `&` ~`[set p0 i]). +suff -> : \pi_wedge @^-1` (@wedgei 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. -case/eqmodP/orP => [/eqP <- |]; first by exists l. -by move=> /= /andP [/eqP]; move: lNx0 => /[swap] ->. +by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l. Qed. Lemma wedge_openP (U : set wedge) : - open U <-> (forall i, open (@wedgei i @^-1` U)). + open U <-> forall i, open (@wedgei i @^-1` U). Proof. -split. - move=> oU i; apply: open_comp => // ? _. - by apply: continuous_comp => //; exact: pi_continuous. -move=> oiU. -have : open (\bigcup_i (@wedgei i @` (@wedgei i @^-1` U) )). - apply/sigT_openP => i; move: (oiU i); congr(open _). +split=> [oU i|oiU]. + by apply: open_comp => // x _; exact: wedgei_continuous. +have : open (\bigcup_i (@wedgei i @` (@wedgei 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 /orP [/eqP R|]. - have E : j = i by move: R; apply: eq_sigT_fst. - move: x R; rewrite -E => x R; move: Uy; congr(U (_ _)); move: R. - apply: Eqdep_dec.inj_pair2_eq_dec. - by move => p q; case: (pselect (p = q)) => ?; [left | right]. - case/andP=> /eqP/= + /eqP ->; move: Uy => /[swap] ->; congr(_ _). - by apply/eqmodP; apply/orP; right; rewrite ?eqxx. -congr(open _); rewrite eqEsubset; split => /= z. + 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. + rewrite -E in x R *; move: Uy; congr (U (_ _)). + exact: existT_inj R. + case/andP => /eqP/= + /eqP ->; move: Uy => /[swap] ->; congr (_ _). + by apply/eqmodP/orP; right; rewrite !eqxx. +congr open; rewrite eqEsubset; split => /= z. by case=> i _ /= [x] Ux <-. -move=> Uz; exists (projT1 (repr z)) => //=. +move=> Uz; exists (projT1 (repr z)) => //=. by exists (projT2 (repr z)); rewrite /wedgei /= -?sigT_eta ?reprK. Qed. -Lemma wedge_pointE i j : existT _ i (p0 i) = existT _ j (p0 j) %[mod wedge]. +Lemma wedge_pointE i j : existT _ i (p0 i) = existT _ j (p0 j) %[mod wedge]. Proof. by apply/eqmodP; apply/orP; right; rewrite ?eqxx. Qed. -Lemma wedge_point_nbhs i0 : - nbhs (wedgei (p0 i0)) = \bigcap_i ((@wedgei i) @ p0 i). +Lemma wedge_point_nbhs i0 : + nbhs (wedgei (p0 i0)) = \bigcap_i (@wedgei i @ p0 i). Proof. rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl. case=> V [/= oV Vp] VU j _; apply: wedgei_continuous. - move/filterS: VU; apply => //; first exact: (@nbhs_filter wedge). - apply: open_nbhs_nbhs; split => //; move: Vp; congr( _ _). + apply: (filterS VU); first exact: (@nbhs_filter wedge). + apply: open_nbhs_nbhs; split => //; move: Vp; congr (_ _). by rewrite /wedgei /=; exact: wedge_pointE. -move=> Uj; have V_ : forall i, {V : set (X i) | - [/\ open V, V (p0 i) & V `<=` (@wedgei i) @^-1` U]}. - (move=> j; have Ij : [set: I] j by done); apply: cid. - by move: (Uj _ Ij); rewrite nbhsE /=; case=> B [? ? ?]; exists B. +move=> Uj; have V_ : forall i, {V : set (X i) | + [/\ open V, V (p0 i) & V `<=` @wedgei i @^-1` U]}. + move=> j; apply: cid; have /Uj : [set: I] j by []. + by rewrite nbhsE /= => -[B [? ? ?]]; exists B. pose W := \bigcup_i (@wedgei 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 /orP [/eqP [E]| ]. - move: w svw; rewrite E => w svw R. - have <- // := Eqdep_dec.inj_pair2_eq_dec _ _ _ _ _ _ R. - by move=> a b; case: (pselect (a = b)) => ?; [left | right]. - by case/andP=> /eqP /= _ /eqP ->. + 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); apply. +- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact. Qed. -Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := +Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := | WedgeIsPoint i0 : wedge_nbhs_spec z (wedgei (p0 i0)) (\bigcap_i ((@wedgei i) @ p0 i)) | WedgeNotPoint (i : I) (x : X i) of (x != p0 i): @@ -159,41 +150,40 @@ Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := 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). -move=> i x; case: (pselect (x = p0 i)). - move=> ->; rewrite wedge_point_nbhs => /=; apply: WedgeIsPoint. -by move/eqP => xpi; rewrite /= -wedgei_nbhs //; apply: WedgeNotPoint. +move=> clP; rewrite -[z](@reprK _ wedge); case: (repr z) => i x. +have [->|xpi] := eqVneq x (p0 i). + by rewrite wedge_point_nbhs => /=; exact: WedgeIsPoint. +by rewrite /= -wedgei_nbhs //; exact: WedgeNotPoint. Qed. Lemma wedgeTE : \bigcup_i (@wedgei i) @` setT = [set: wedge]. -Proof. -rewrite -subTset=> z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. -by exists (projT2 (repr z)); rewrite // reprK /wedgei /= -sigT_eta reprK. +Proof. +rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. +by exists (projT2 (repr z)) => //; rewrite reprK /wedgei /= -sigT_eta reprK. Qed. -Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> +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. +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. +exact/continuous_subspaceT/wedgei_continuous. Qed. -Lemma wedge_connected : (forall i, connected [set: X i]) -> +Lemma wedge_connected : (forall i, connected [set: X i]) -> connected [set: wedge]. Proof. -move=> ctdX; rewrite -wedgeTE. -case: (pselect ([set: I] !=set0)); first last. - move=> I0; have := @connected0 (wedge); congr (_ _). - by rewrite eqEsubset; split => ? // [] x ?; move: I0; apply: absurd; exists x. -case=> i0 Ii0; apply: bigcup_connected. +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 (@wedgei i0 (p0 _)) => i Ii; exists (p0 i) => //. - by rewrite /wedgei /=; apply/eqmodP; apply/orP; right; rewrite ?eqxx. + by apply/eqmodP/orP; right; rewrite !eqxx. move=> i ? /=; apply: connected_continuous_connected => //. -by exact/continuous_subspaceT/wedgei_continuous. +exact/continuous_subspaceT/wedgei_continuous. Qed. End wedge. 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. From 15d289b6905bcb12e0b3cb0eee07b8d84f2ceb28 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 10 Nov 2024 00:05:58 +0900 Subject: [PATCH 4/6] nitpick --- theories/homotopy_theory/wedge_sigT.v | 29 ++++++++++++++------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 56cc5e977..0378615ca 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -65,7 +65,7 @@ Definition wedge_rel := EquivRel _ wedge_rel_refl wedge_rel_sym wedge_rel_trans. Global Opaque wedge_rel. Definition wedge := {eq_quot wedge_rel}. -Definition wedgei (i : I) : X i -> wedge := \pi_wedge \o existT X i. +Definition wedgei 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. @@ -94,6 +94,9 @@ rewrite eqEsubset; split => t /= [l [Vl] lNx0]; last by move=> <-; exists l. by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l. Qed. +Let wedgei_p0 i (x : X i) j (y : X j) : wedgei (p0 j) = wedgei (p0 i). +Proof. by apply/eqmodP/orP; right; rewrite !eqxx. Qed. + Lemma wedge_openP (U : set wedge) : open U <-> forall i, open (@wedgei i @^-1` U). Proof. @@ -105,14 +108,13 @@ have : open (\bigcup_i (@wedgei i @` (@wedgei i @^-1` U))). 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. - rewrite -E in x R *; move: Uy; congr (U (_ _)). - exact: existT_inj R. - case/andP => /eqP/= + /eqP ->; move: Uy => /[swap] ->; congr (_ _). - by apply/eqmodP/orP; right; rewrite !eqxx. + by rewrite -E in x R *; rewrite -(existT_inj R). + case/andP => /eqP/= + /eqP -> => yj. + by rewrite yj (wedgei_p0 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 /wedgei /= -?sigT_eta ?reprK. +by exists (projT2 (repr z)); rewrite /wedgei /= -sigT_eta reprK. Qed. Lemma wedge_pointE i j : existT _ i (p0 i) = existT _ j (p0 j) %[mod wedge]. @@ -124,8 +126,8 @@ Proof. rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl. case=> V [/= oV Vp] VU j _; apply: wedgei_continuous. apply: (filterS VU); first exact: (@nbhs_filter wedge). - apply: open_nbhs_nbhs; split => //; move: Vp; congr (_ _). - by rewrite /wedgei /=; exact: wedge_pointE. + apply: open_nbhs_nbhs; split => //. + by rewrite (wedgei_p0 (p0 i0)). move=> Uj; have V_ : forall i, {V : set (X i) | [/\ open V, V (p0 i) & V `<=` @wedgei i @^-1` U]}. move=> j; apply: cid; have /Uj : [set: I] j by []. @@ -133,8 +135,8 @@ move=> Uj; have V_ : forall i, {V : set (X i) | pose W := \bigcup_i (@wedgei 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]| ]. + 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). @@ -143,7 +145,7 @@ Qed. Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := | WedgeIsPoint i0 : - wedge_nbhs_spec z (wedgei (p0 i0)) (\bigcap_i ((@wedgei i) @ p0 i)) + wedge_nbhs_spec z (wedgei (p0 i0)) (\bigcap_i (@wedgei i @ p0 i)) | WedgeNotPoint (i : I) (x : X i) of (x != p0 i): wedge_nbhs_spec z (wedgei x) (@wedgei i @ x). @@ -159,7 +161,7 @@ Qed. Lemma wedgeTE : \bigcup_i (@wedgei i) @` setT = [set: wedge]. Proof. rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //. -by exists (projT2 (repr z)) => //; rewrite reprK /wedgei /= -sigT_eta reprK. +by exists (projT2 (repr z)) => //; rewrite /wedgei/= -sigT_eta. Qed. Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> @@ -180,8 +182,7 @@ 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 (@wedgei i0 (p0 _)) => i Ii; exists (p0 i) => //. - by apply/eqmodP/orP; right; rewrite !eqxx. + by exists (@wedgei i0 (p0 _)) => i Ii; exists (p0 i) => //; exact: wedgei_p0. move=> i ? /=; apply: connected_continuous_connected => //. exact/continuous_subspaceT/wedgei_continuous. Qed. From fc68dede598c69b7d8beccfad23893cd5d5d516f Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 9 Nov 2024 23:57:44 -0500 Subject: [PATCH 5/6] renaming wedgei --- CHANGELOG_UNRELEASED.md | 4 +- theories/homotopy_theory/wedge_sigT.v | 69 +++++++++++++-------------- 2 files changed, 36 insertions(+), 37 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 73365b0c3..649aa56c1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -80,8 +80,8 @@ - file `homotopy_theory/homotopy.v` - file `homotopy_theory/wedge_sigT.v` - in file `homotopy_theory/wedge_sigT.v` - + new definitions `wedge_rel`, `wedge`, `wedgei`, `pwedge`. - + new lemmas `wedgei_continuous`, `wedgei_nbhs`, `wedge_openP`, + + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`. + + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`, `wedge_openP`, `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`, `wedge_compact`, `wedge_connected`. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 0378615ca..99688dff8 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -16,7 +16,7 @@ Require Import EqdepFacts. (* 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` *) -(* wedgei i == the lifting of elements of (X i) into the wedge *) +(* wedge_lift i == the lifting of elements of (X i) into the wedge *) (* pwedge p0 == the wedge of ptopologicalTypes at their designated *) (* point *) (* ``` *) @@ -65,44 +65,45 @@ Definition wedge_rel := EquivRel _ wedge_rel_refl wedge_rel_sym wedge_rel_trans. Global Opaque wedge_rel. Definition wedge := {eq_quot wedge_rel}. -Definition wedgei i : X i -> wedge := \pi_wedge \o existT X i. +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 wedgei_continuous i : continuous (@wedgei i). +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 _ _ (@wedgei i) (@wedgei_continuous i). + @isContinuous.Build _ _ (@wedge_lift i) (@wedge_lift_continuous i). -Lemma wedgei_nbhs i (x : X i) : - closed [set p0 i] -> x != p0 _ -> (@wedgei i) @ x = nbhs (@wedgei _ x). +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: wedgei_continuous. + by move=> ?; exact: wedge_lift_continuous. rewrite ?nbhsE /= => -[V [oV Vx VU]]. -exists (@wedgei i @` (V `&` ~` [set p0 i])); first last. +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 /wedgei /=. -suff -> : \pi_wedge @^-1` (@wedgei i @` (V `&` ~`[set p0 i])) = +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. -Let wedgei_p0 i (x : X i) j (y : X j) : wedgei (p0 j) = wedgei (p0 i). +Lemma wedge_lift_p0E 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 (@wedgei i @^-1` U). + open U <-> forall i, open (@wedge_lift i @^-1` U). Proof. split=> [oU i|oiU]. - by apply: open_comp => // x _; exact: wedgei_continuous. -have : open (\bigcup_i (@wedgei i @` (@wedgei i @^-1` U))). + 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. @@ -110,29 +111,26 @@ have : open (\bigcup_i (@wedgei i @` (@wedgei i @^-1` U))). 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 (wedgei_p0 x y) in Uy. + by rewrite yj (wedge_lift_p0E 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 /wedgei /= -sigT_eta reprK. +by exists (projT2 (repr z)); rewrite /wedge_lift /= -sigT_eta reprK. Qed. -Lemma wedge_pointE i j : existT _ i (p0 i) = existT _ j (p0 j) %[mod wedge]. -Proof. by apply/eqmodP; apply/orP; right; rewrite ?eqxx. Qed. - Lemma wedge_point_nbhs i0 : - nbhs (wedgei (p0 i0)) = \bigcap_i (@wedgei i @ p0 i). + 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: wedgei_continuous. + 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 (wedgei_p0 (p0 i0)). + by rewrite (wedge_lift_p0E (p0 i0)). move=> Uj; have V_ : forall i, {V : set (X i) | - [/\ open V, V (p0 i) & V `<=` @wedgei i @^-1` U]}. + [/\ 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 (@wedgei i) @` (projT1 (V_ i)). +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. @@ -144,24 +142,24 @@ exists W; split. Qed. Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type := - | WedgeIsPoint i0 : - wedge_nbhs_spec z (wedgei (p0 i0)) (\bigcap_i (@wedgei i @ p0 i)) + | 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 (wedgei x) (@wedgei i @ x). + 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: WedgeIsPoint. -by rewrite /= -wedgei_nbhs //; exact: WedgeNotPoint. + by rewrite wedge_point_nbhs => /=; exact: wedge_liftsPoint. +by rewrite /= -wedge_lift_nbhs //; exact: WedgeNotPoint. Qed. -Lemma wedgeTE : \bigcup_i (@wedgei i) @` setT = [set: wedge]. +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 /wedgei/= -sigT_eta. +by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= -sigT_eta. Qed. Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) -> @@ -171,7 +169,7 @@ 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/wedgei_continuous. +exact/continuous_subspaceT/wedge_lift_continuous. Qed. Lemma wedge_connected : (forall i, connected [set: X i]) -> @@ -182,9 +180,10 @@ 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. - by exists (@wedgei i0 (p0 _)) => i Ii; exists (p0 i) => //; exact: wedgei_p0. + exists (@wedge_lift i0 (p0 _)) => i Ii; exists (p0 i) => //. + exact: wedge_lift_p0E. move=> i ? /=; apply: connected_continuous_connected => //. -exact/continuous_subspaceT/wedgei_continuous. +exact/continuous_subspaceT/wedge_lift_continuous. Qed. End wedge. @@ -194,7 +193,7 @@ Context {I : pointedType} (X : I -> ptopologicalType). Definition pwedge := wedge (fun i => @point (X i)). -Let pwedge_point : pwedge := wedgei _ (@point (X (@point I))). +Let pwedge_point : pwedge := wedge_lift _ (@point (X (@point I))). HB.instance Definition _ := Topological.on pwedge. HB.instance Definition _ := Quotient.on pwedge. From be7981b07a582ad8aed5693d9071797cc96e98fb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 10 Nov 2024 21:59:01 +0900 Subject: [PATCH 6/6] fix changelog --- CHANGELOG_UNRELEASED.md | 3 ++- theories/homotopy_theory/wedge_sigT.v | 10 +++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 649aa56c1..4450c6f19 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,7 +81,8 @@ - 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_openP`, + + 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`. diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 99688dff8..08625921f 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -94,7 +94,7 @@ rewrite eqEsubset; split => t /= [l [Vl] lNx0]; last by move=> <-; exists l. by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l. Qed. -Lemma wedge_lift_p0E i (x : X i) j (y : X j) : +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. @@ -111,7 +111,7 @@ have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))). 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_lift_p0E x y) in Uy. + 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)) => //=. @@ -125,7 +125,7 @@ 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_lift_p0E (p0 i0)). + 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 []. @@ -180,8 +180,8 @@ 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_lift_p0E. + 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.