Merge pull request #2367 from jdchristensen/EMspaces

Minor cleanups to homotopy groups, etc

Author: jdchristensen

theories/Homotopy/EMSpace.v

@@ -130,7 +130,7 @@ Section EilenbergMacLane.
       K( (Pi n.+2 X) n.+2)
    <~>* K( (Pi n.+1 (loops X)), n.+2)
    = pTr n.+2 (psusp K( (Pi n.+1 (loops X)), n.+1))  [by definition]
-   <~>* pTr n.+2 (psusp (loops X))
+   <~>* pTr n.+2 (psusp (loops X))                   [by induction]
    <~>* pTr n.+2 X
    <~>* X
 >>

theories/Homotopy/HomotopyGroup.v

@@ -34,6 +34,8 @@ Instance is01cat_homotopygroup_type (n : nat)
   : Is01Cat (HomotopyGroup_type n) := ltac:(destruct n; exact _).
 Instance is1cat_homotopygroup_type (n : nat)
   : Is1Cat (HomotopyGroup_type n) := ltac:(destruct n; exact _).
+Instance hasequivs_homotopygroup_type (n : nat)
+  : HasEquivs (HomotopyGroup_type n) := ltac:(destruct n; exact _).
 Instance is0functor_homotopygroup_type_ptype (n : nat)
   : Is0Functor (HomotopyGroup_type_ptype n)
   := ltac:(destruct n; exact _).

theories/Homotopy/Hopf.v

@@ -1,5 +1,7 @@
 From HoTT Require Import Basics Types Pointed Truncations.
 Require Import HSpace Suspension ExactSequence HomotopyGroup.
+(* Group not imported, as it confuses Rocq regarding [*.] notation. *)
+Require Algebra.Groups.Group.
 Require Import WildCat.Core WildCat.Universe WildCat.Equiv Modalities.ReflectiveSubuniverse Modalities.Descent.
 Require Import HSet Spaces.Nat.Core.
 Require Import Homotopy.Join Colimits.Pushout.
@@ -8,7 +10,6 @@ Local Open Scope pointed_scope.
 Local Open Scope trunc_scope.
 Local Open Scope mc_mult_scope.
 
-
 (** * The Hopf construction *)
 
 (** We define the Hopf construction associated to a left-invertible H-space, and use it to prove that H-spaces satisfy a strengthened version of Freudenthal's theorem (see [freudenthal_hspace] below). *)
@@ -24,7 +25,7 @@ Proof.
   - simpl. exact pt.
 Defined.
 
-(** *** Total space of the Hopf construction *)
+(** ** Total space of the Hopf construction *)
 
 (** The total space of the Hopf construction on [Susp X] is the join of [X] with itself. Note that we need both left and right multiplication to be equivalences. This is true when [X] is a 0-connected H-space for example. (This is lemma 8.5.7 in the HoTT book). *)
 Definition pequiv_hopf_total_join `{Univalence} (X : pType)
@@ -60,7 +61,7 @@ Proof.
   apply transport_path_universe.
 Defined.
 
-(** The connecting map associated to the Hopf construction of [X] is a retraction of [loop_susp_unit X] (Proposition 2.19 in https://arxiv.org/abs/2301.02636v1). *)
+(** The connecting map [loops (psusp X) ->* X] associated to the Hopf construction of [X] is a retraction of [loop_susp_unit X] (Proposition 2.19 in https://arxiv.org/abs/2301.02636v1). *)
 Proposition hopf_retraction `{Univalence} (X : pType)
   `{IsHSpace X} `{forall a, IsEquiv (a *.)}
   : connecting_map_family (hopf_construction X) o* loop_susp_unit X
@@ -78,8 +79,7 @@ Defined.
 
 (** It follows from [hopf_retraction] and Freudenthal's theorem that [loop_susp_unit] induces an equivalence on [Pi (2n+1)] for [n]-connected H-spaces (with n >= 0). Note that [X] is automatically left-invertible. *)
 Proposition isequiv_Pi_connected_hspace `{Univalence}
-  {n : nat} (X : pType) `{IsConnected n X}
-  `{IsHSpace X}
+  {n : nat} (X : pType) `{IsConnected n X} `{IsHSpace X}
   : IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)).
 Proof.
   napply isequiv_surj_emb.
@@ -93,6 +93,13 @@ Proof.
     apply hopf_retraction.
 Defined.
 
+(** Since the above equivalence is also a group homomorphism, we get an isomorphism of groups.  (We could also express the conclusion using the wild-category notation [$<~>], but then the goal would involve [HomotopyGroup_type _] instead of literally being in the category [Group].) *)
+Definition grp_iso_Pi_connected_hspace `{Univalence}
+  {n : nat} (X : pType) `{IsConnected n X} `{IsHSpace X}
+  : Group.GroupIsomorphism (Pi (n + n).+1 X) (Pi (n + n).+1 (loops (psusp X)))
+  := Group.Build_GroupIsomorphism _ _ (fmap (Pi (n + n).+1) (loop_susp_unit X))
+      (isequiv_Pi_connected_hspace X).
+
 (** By Freudenthal, [loop_susp_unit] induces an equivalence on lower homotopy groups as well, so it is a (2n+1)-equivalence.  We formalize it below with [m = n-1], and allow [n] to start at [-1].  We prove it using a more general result about reflective subuniverses, [OO_inverts_conn_map_factor_conn_map], but one could also use homotopy groups and the truncated Whitehead theorem. *)
 Definition freudenthal_hspace' `{Univalence}
   {m : trunc_index} (X : pType) `{IsConnected m.+1 X}

theories/Homotopy/PinSn.v

@@ -18,8 +18,6 @@ Local Open Scope pointed_scope.
 Section Pi1S1.
   Context `{Univalence}.
 
-  Local Open Scope pointed_scope.
-
   Theorem pi1_circle : Pi 1 [Circle, base] ≅ abgroup_Z.
   Proof.
     (** We give the isomorphism backwards, so we check the operation is preserved coming from the integer side. *)
@@ -57,9 +55,10 @@ Section Pi2S2.
   Proof.
     refine (pi1_s1 $oE _).
     change (Pi 2 ?X) with (Pi 1 (loops X)).
-    refine (compose_cate (b:=Pi 1 (pTr 1 (loops (psphere 2)))) _ _).
-    1: exact (emap (Pi 1) ptr_loops_s2_s1).
-    apply grp_iso_pi_Tr.
+    symmetry; exact (grp_iso_Pi_connected_hspace (psphere 1)).
+    (* The last line can also be replaced with
+         exact (compose_cate (A:=Group) (emap (Pi 1) ptr_loops_s2_s1)
+                                        (grp_iso_pi_Tr _ _)). *)
   Defined.
 
 End Pi2S2.
@@ -82,6 +81,6 @@ Section PinSn.
     apply (isconnmap_pred_add n.-2).
     rewrite 2 trunc_index_add_succ.
     change (IsConnMap (Tr (n +2+ n)) (loop_susp_unit (psphere n.+2))).
-    exact _. (* [conn_map_loop_susp_unit] *)
+    rapply conn_map_loop_susp_unit.
   Defined.
 End PinSn.