From ec24ca894f8180d59e171af1f48c0581e68df706 Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Sun, 9 Feb 2025 19:48:27 +0100 Subject: [PATCH] connectivity of wedge inclusion Signed-off-by: Ali Caglayan --- theories/Homotopy/Wedge.v | 125 +++++++++++++++++++++++++++++++++++--- theories/Types/Paths.v | 19 ++++++ 2 files changed, 137 insertions(+), 7 deletions(-) diff --git a/theories/Homotopy/Wedge.v b/theories/Homotopy/Wedge.v index 9db9cfa3d4..47971f4009 100644 --- a/theories/Homotopy/Wedge.v +++ b/theories/Homotopy/Wedge.v @@ -3,6 +3,8 @@ Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension. +Require Import Truncations.Core Truncations.Connectedness. +Require Import Modalities.ReflectiveSubuniverse. Local Set Universe Minimization ToSet. @@ -79,6 +81,56 @@ Proof. - reflexivity. Defined. +Definition wedge_ind {X Y : pType} (P : X \/ Y -> Type) + (f : forall x, P (wedge_inl x)) (g : forall y, P (wedge_inr y)) + (w : wglue # f pt = g pt) + : forall xy, P xy. +Proof. + snrapply (Pushout_ind P f g). + intros []. + exact w. +Defined. + +Definition wedge_ind_beta_wglue {X Y : pType} (P : X \/ Y -> Type) + (f : forall x, P (wedge_inl x)) (g : forall y, P (wedge_inr y)) + (w : wglue # f pt = g pt) + : apD (wedge_ind P f g w) wglue = w + := Pushout_ind_beta_pglue P _ _ _ _. + +Definition wedge_ind_FlFr {X Y Z : pType} {f g : X \/ Y -> Z} + (l : f o wedge_inl == g o wedge_inl) + (r : f o wedge_inr == g o wedge_inr) + (w : ap f wglue @ r pt = l pt @ ap g wglue) + : f == g. +Proof. + snrapply (wedge_ind _ l r). + nrapply transport_paths_FlFr'. + exact w. +Defined. + +Definition wedge_ind_FFl {X Y Z W : pType} (f : X \/ Y -> Z) (g : Z -> W) + {y : W} + (l : forall x, g (f (wedge_inl x)) = y) + (r : forall x, g (f (wedge_inr x)) = y) + (w : ap g (ap f wglue) @ r pt = l pt) + : forall x, g (f x) = y. +Proof. + snrapply (wedge_ind _ l r); simpl. + nrapply transport_paths_FFl'. + exact w. +Defined. + +Definition wedge_ind_FFlr {X Y Z : pType} (f : X \/ Y -> Z) (g : Z -> X \/ Y) + (l : g o f o wedge_inl == wedge_inl) + (r : g o f o wedge_inr == wedge_inr) + (w : ap g (ap f wglue) @ r pt = l pt @ wglue) + : g o f == idmap. +Proof. + snrapply (wedge_ind _ l r); simpl. + nrapply transport_paths_FFlr'. + exact w. +Defined. + (** 1-universal property of wedge. *) Lemma wedge_up X Y Z (f g : X \/ Y $-> Z) : f $o wedge_inl $== g $o wedge_inl @@ -87,9 +139,7 @@ Lemma wedge_up X Y Z (f g : X \/ Y $-> Z) Proof. intros p q. snrapply Build_pHomotopy. - - snrapply (Pushout_ind _ p q). - intros []. - nrapply transport_paths_FlFr'. + - snrapply (wedge_ind_FlFr p q). lhs nrapply (whiskerL _ (dpoint_eq q)). rhs nrapply (whiskerR (dpoint_eq p)). clear p q. @@ -131,7 +181,7 @@ Proof. - intros Z f g. snrapply Build_pHomotopy. 1: reflexivity. - by simpl; pelim f. + symmetry; apply concat_pp_V. - intros Z f g. snrapply Build_pHomotopy. 1: reflexivity. @@ -142,9 +192,9 @@ Proof. apply moveR_Mp. apply moveL_pV. apply moveR_Vp. - refine (Pushout_rec_beta_pglue _ f g _ _ @ _). - simpl. - by pelim f g. + lhs nrapply wedge_rec_beta_wglue. + f_ap; f_ap; symmetry. + apply concat_1p. - intros Z f g p q. by apply wedge_up. Defined. @@ -370,3 +420,64 @@ Proof. - reflexivity. Defined. +(** ** Connectivity of wedge inclusion *) + +Definition conn_map_wedge_incl `{Univalence} {m n : trunc_index} (X Y : pType) + `{!IsConnected m.+1 X, !IsConnected n.+1 Y} + : IsConnMap (m +2+ n) (wedge_incl X Y). +Proof. + rewrite trunc_index_add_comm. + apply conn_map_from_extension_elim. + intros P h d. + transparent assert (f : (forall x y, P (x, y))). + { intros x y; revert y x. + rapply (wedge_incl_elim (n:=m) (m:=n) + (point Y) (point X) (fun y x => P (x, y)) + (d o wedge_inl) (d o wedge_inr)). + rhs_V nrapply (apD d wglue). + rhs nrapply transport_compose. + nrapply (transport2 _ (p:=1) _^). + apply wedge_incl_beta_wglue. } + transparent assert (p : (forall x : X, + prod_ind P f (wedge_incl X Y (wedge_inl x)) = d (wedge_inl x))). + 1: nrapply wedge_incl_comp1. + transparent assert (q : (forall y : Y, + prod_ind P f (wedge_incl X Y (wedge_inr y)) = d (wedge_inr y))). + 1: nrapply wedge_incl_comp2. + transparent assert (pq + : (q pt = p pt @ + ((transport2 P wedge_incl_beta_wglue^ (d (wedge_inl pt)) + @ (transport_compose P (wedge_incl X Y) wglue (d (pushl pt)))^) + @ apD d wglue))). + 1: nrapply wedge_incl_comp3. + clearbody f p q pq. + exists (prod_ind _ f). + nrapply (wedge_ind _ p q). + rhs nrapply pq. + lhs nrapply (transport_paths_FlFr_D wglue). + lhs nrapply concat_pp_p. + apply moveR_Vp. + rhs nrapply concat_p_pp. + rhs nrapply concat_p_pp. + apply whiskerR. + unshelve lhs nrapply ap_homotopic_id. + { intros x. + lhs nrapply transport_compose. + nrapply (transport2 _ (q:=1)). + apply wedge_incl_beta_wglue. } + cbn beta. + apply concat2. + - apply whiskerR. + symmetry. + lhs nrapply apD_compose. + apply whiskerL. + lhs_V nrapply (apD _ wedge_incl_beta_wglue^). + nrapply moveR_transport_V. + symmetry. + nrapply (transport_paths_Fl' wedge_incl_beta_wglue). + nrapply concat_p1. + - symmetry. + rhs nrapply inv_pp. + apply whiskerR. + exact (transport2_V P wedge_incl_beta_wglue _). +Defined. diff --git a/theories/Types/Paths.v b/theories/Types/Paths.v index e1009289ab..dc593c4e48 100644 --- a/theories/Types/Paths.v +++ b/theories/Types/Paths.v @@ -140,6 +140,25 @@ Proof. exact h^. Defined. +Definition transport_paths_Fl' {A B : Type} {f : A -> B} {x1 x2 : A} {y : B} + (p : x1 = x2) (q : f x1 = y) (r : f x2 = y) (h : ap f p @ r = q) + : transport (fun x => f x = y) p q = r. +Proof. + refine (transport_paths_Fl _ _ @ _). + apply moveR_Vp. + exact h^. +Defined. + +Definition transport_paths_FFl' {A B C : Type} {f : A -> B} {g : B -> C} + {x1 x2 : A} {y : C} (p : x1 = x2) (q : g (f x1) = y) (r : g (f x2) = y) + (h : ap g (ap f p) @ r = q) + : transport (fun x => g (f x) = y) p q = r. +Proof. + refine (transport_paths_FFl _ _ @ _). + apply moveR_Vp. + exact h^. +Defined. + Definition transport_paths_FlFr' {A B : Type} {f g : A -> B} {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1) (r : (f x2) = (g x2)) (h : (ap f p) @ r = q @ (ap g p))