Merge pull request #1845 from Alizter/ps/branch/pinch_map_of_suspension

pinch map of suspension

Author: Alizter

theories/Homotopy/Wedge.v

@@ -1,7 +1,8 @@
 Require Import Basics Types.
-Require Import Pointed.Core.
+Require Import Pointed.Core Pointed.pSusp.
 Require Import Colimits.Pushout.
 Require Import WildCat.
+Require Import Homotopy.Suspension.
 
 (* Here we define the Wedge sum of two pointed types *)
 
@@ -37,10 +38,15 @@ Proof.
   - snrapply Pushout_rec.
     + exact f.
     + exact g.
-    + by pelim f g.
+    + intro.
+      exact (point_eq f @ (point_eq g)^).
   - exact (point_eq f).
 Defined.
 
+Definition wedge_rec_beta_wglue {X Y Z : pType} (f : X $-> Z) (g : Y $-> Z)
+  : ap (wedge_rec f g) wglue = point_eq f @ (point_eq g)^
+  := Pushout_rec_beta_pglue _ f g _ tt.
+
 Definition wedge_pr1 {X Y : pType} : X \/ Y $-> X
   := wedge_rec pmap_idmap pconst.
 
@@ -51,7 +57,7 @@ Definition wedge_incl {X Y : pType} : X \/ Y -> X * Y
   := pprod_corec _ wedge_pr1 wedge_pr2.
 
 (** 1-universal property of wedge. *)
-(** TODO: remove rewrites. For some reason pelim is not able to immediately abstract the goal so some shuffling around is necessery. *)
+(** TODO: remove rewrites. For some reason pelim is not able to immediately abstract the goal so some shuffling around is necessary. *)
 Lemma wedge_up X Y Z (f g : X \/ Y $-> Z)
   : f $o wedge_inl $== g $o wedge_inl
   -> f $o wedge_inr $== g $o wedge_inr
@@ -101,15 +107,47 @@ Proof.
     apply moveL_pV.
     apply moveR_Vp.
     refine (Pushout_rec_beta_pglue _ f g _ _  @ _).
-    simpl.  
+    simpl.
     by pelim f g.
   - intros Z f g p q.
     by apply wedge_up.
 Defined.
 
+(** *** Lemmas about wedge functions *)
+
+Lemma wedge_pr1_inl {X Y} : wedge_pr1 $o (@wedge_inl X Y) $== pmap_idmap.
+Proof.
+  reflexivity.
+Defined.
+
+Lemma wedge_pr1_inr {X Y} : wedge_pr1 $o (@wedge_inr X Y) $== pconst.
+Proof.
+  snrapply Build_pHomotopy.
+  1: reflexivity.
+  rhs nrapply concat_p1.
+  rhs nrapply concat_p1.
+  rhs nrapply (ap_V _ wglue).
+  exact (inverse2 (wedge_rec_beta_wglue pmap_idmap pconst)^).
+Defined.
+
+Lemma wedge_pr2_inl {X Y} : wedge_pr2 $o (@wedge_inl X Y) $== pconst.
+Proof.
+  reflexivity.
+Defined.
+
+Lemma wedge_pr2_inr {X Y} : wedge_pr2 $o (@wedge_inr X Y) $== pmap_idmap.
+Proof.
+  snrapply Build_pHomotopy.
+  1: reflexivity.
+  rhs nrapply concat_p1.
+  rhs nrapply concat_p1.
+  rhs nrapply (ap_V _ wglue).
+  exact (inverse2 (wedge_rec_beta_wglue pconst pmap_idmap)^).
+Defined.
+
 (** Wedge of an indexed family of pointed types *)
 
-(** Note that the index type is not necesserily pointed. An empty wedge is the unit type which is the zero object in the category of pointed types. *)
+(** Note that the index type is not necessarily pointed. An empty wedge is the unit type which is the zero object in the category of pointed types. *)
 Definition FamilyWedge (I : Type) (X : I -> pType) : pType.
 Proof.
   snrapply Build_pType.
@@ -143,7 +181,7 @@ Proof.
   - exact idpath.
 Defined.
 
-(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge should land. This makes it somewhat awkward to work with, however in practice we typically only care about decidable index sets. *) 
+(** Wedge inclusions into the product can be defined if the indexing type has decidable paths. This is because we need to choose which factor a given wedge should land. This makes it somewhat awkward to work with, however in practice we typically only care about decidable index sets. *)
 Definition fwedge_incl `{Funext} (I : Type) `(DecidablePaths I) (X : I -> pType)
   : FamilyWedge I X $-> pproduct X.
 Proof.
@@ -155,3 +193,118 @@ Proof.
   - destruct p; exact pmap_idmap.
   - exact pconst.
 Defined.
+
+(** ** The pinch map on the suspension *)
+
+(** Given a suspension, there is a natural map from the suspension to the wedge of the suspension with itself. This is known as the pinch map.
+
+This is the image to keep in mind:
+<<
+                                    *
+                                   /|\
+                                  / | \
+    Susp X                       /  |  \
+                                /   |   \
+       *                       * merid(x)*
+      /|\                       \   |   /
+     / | \                       \  |  /
+    /  |  \                       \ | /
+   /   |   \      Pinch            \|/
+  * merid(x)*   ---------->         *
+   \   |   /                       /|\
+    \  |  /                       / | \
+     \ | /                       /  |  \
+      \|/                       /   |   \
+       *                       * merid(x)*
+                                \   |   /
+                                 \  |  /
+                                  \ | /
+                                   \|/
+                                    *
+>>
+
+Note that this is only a conceptual picture as we aren't working with "reduced suspensions". This means we have to track back along [merid pt] making this map a little trickier to imagine. *)
+
+(** The pinch map for a suspension. *)
+Definition psusp_pinch (X : pType) : psusp X ->* psusp X \/ psusp X.
+Proof.
+  refine (Build_pMap _ _ (Susp_rec pt pt _) idpath).
+  intros x.
+  refine (ap wedge_inl _ @ wglue @ ap wedge_inr _ @ wglue^).
+  1,2: exact (loop_susp_unit X x).
+Defined.
+
+(** It should compute when [ap]ed on a merid. *)
+Definition psusp_pinch_beta_merid {X : pType} (x : X)
+  : ap (psusp_pinch X) (merid x)
+    = ap wedge_inl (loop_susp_unit X x) @ wglue
+    @ ap wedge_inr (loop_susp_unit X x) @ wglue^.
+Proof.
+  rapply Susp_rec_beta_merid.
+Defined.
+
+(** Doing wedge projections on the pinch map gives the identity. *)
+Definition wedge_pr1_psusp_pinch {X}
+  : wedge_pr1 $o psusp_pinch X ==* Id (psusp X).
+Proof.
+  snrapply Build_pHomotopy.
+  - snrapply Susp_ind_FlFr.
+    + reflexivity.
+    + exact (merid pt).
+    + intros x.
+      rhs nrapply concat_1p.
+      rhs nrapply ap_idmap.
+      apply moveR_pM.
+      change (?t = _) with (t = loop_susp_unit X x).
+      lhs nrapply (ap_compose (psusp_pinch X)).
+      lhs nrapply (ap _ (psusp_pinch_beta_merid x)).
+      lhs nrapply ap_pp.
+      lhs nrapply (ap (fun x => _ @ x) (ap_V _ _)).
+      apply moveR_pV.
+      rhs nrapply (whiskerL _ (wedge_rec_beta_wglue _ _)).
+      lhs nrapply ap_pp.
+      lhs nrapply (ap (fun x => _ @ x)).
+      { lhs_V nrapply ap_compose.
+        apply ap_const. }
+      lhs nrapply concat_p1.
+      lhs nrapply ap_pp.
+      lhs nrapply (ap (fun x => _ @ x) (wedge_rec_beta_wglue _ _)).
+      f_ap.
+      lhs_V nrapply (ap_compose wedge_inl).
+      apply ap_idmap.
+  - reflexivity.
+Defined.
+
+Definition wedge_pr2_psusp_pinch {X}
+  : wedge_pr2 $o psusp_pinch X ==* Id (psusp X).
+Proof.
+  snrapply Build_pHomotopy.
+  - snrapply Susp_ind_FlFr.
+    + reflexivity.
+    + exact (merid pt).
+    + intros x.
+      rhs nrapply concat_1p.
+      rhs nrapply ap_idmap.
+      apply moveR_pM.
+      change (?t = _) with (t = loop_susp_unit X x).
+      lhs nrapply (ap_compose (psusp_pinch X)).
+      lhs nrapply (ap _ (psusp_pinch_beta_merid x)).
+      lhs nrapply ap_pp.
+      lhs nrapply (ap (fun x => _ @ x) (ap_V _ _)).
+      apply moveR_pV.
+      rhs nrapply (whiskerL _ (wedge_rec_beta_wglue _ _)).
+      lhs nrapply ap_pp.
+      lhs nrapply (ap (fun x => _ @ x) _).
+      { lhs_V nrapply ap_compose.
+        apply ap_idmap. }
+      rhs nrapply concat_p1.
+      apply moveR_pM.
+      lhs nrapply ap_pp.
+      rhs nrapply concat_pV.
+      lhs nrapply (ap _ (wedge_rec_beta_wglue _ _)).
+      apply moveR_pM.
+      lhs_V nrapply (ap_compose wedge_inl).
+      rapply ap_const.
+  - reflexivity.
+Defined.
+