A strengthening of Freudenthal's theorem for H-spaces

theories/Basics/Trunc.v

@@ -57,6 +57,15 @@ Definition nat_to_trunc_index@{} (n : nat) : trunc_index
 
 Coercion nat_to_trunc_index : nat >-> trunc_index.
 
+Definition trunc_index_inc'_0n (n : nat)
+  : trunc_index_inc' 0%nat n = n.
+Proof.
+  induction n as [|n p].
+  1: reflexivity.
+  refine (trunc_index_inc'_succ _ _ @ _).
+  exact (ap _ p).
+Defined.
+
 Definition int_to_trunc_index@{} (v : Decimal.int) : option trunc_index
   := match v with
      | Decimal.Pos d => Some (nat_to_trunc_index (Nat.of_uint d))

theories/Homotopy/HomotopyGroup.v

@@ -1,4 +1,4 @@
-Require Import Basics Types Pointed.
+Require Import Basics Types Pointed HSet.
 Require Import Modalities.Modality.
 Require Import Truncations.Core.
 Require Import Algebra.AbGroups.
@@ -102,6 +102,10 @@ Module PiUtf8.
   Notation "'π'" := Pi.
 End PiUtf8.
 
+Global Instance ishset_pi {n : nat} {X : pType}
+  : IsHSet (Pi n X)
+  := ltac:(destruct n; exact _).
+
 (** When n >= 2 we have that the nth homotopy group is an abelian group. Note that we don't actually define it as an abelian group but merely show that it is one. This would cause lots of complications with the typechecker. *)
 Global Instance isabgroup_pi (n : nat) (X : pType)
   : IsAbGroup (Pi n.+2 X).
@@ -290,6 +294,37 @@ Proof.
   destruct n; rapply isequiv_pi_connmap'.
 Defined.
 
+(** An [n]-connected map induces a surjection on [n+1]-fold loop spaces and [Pi (n+1)]. *)
+Definition issurj_iterated_loops_connmap `{Univalence} (n : nat)
+  {X Y : pType} (f : X ->* Y) {C : IsConnMap n f}
+  : IsSurjection (fmap (iterated_loops (n.+1)) f).
+Proof.
+  apply isconnected_iterated_fmap_loops. cbn.
+  rewrite trunc_index_inc'_0n; assumption.
+Defined.
+
+Definition issurj_pi_connmap `{Univalence} (n : nat) {X Y : pType}
+  (f : X ->* Y) {C : IsConnMap n f}
+  : IsConnMap (Tr (-1)) (fmap (pPi n.+1) f).
+Proof.
+  rapply conn_map_O_functor_leq.
+  2: by apply issurj_iterated_loops_connmap.
+  by apply O_leq_Tr_leq.
+Defined.
+
+(** Pointed sections induce embeddings on homotopy groups. *)
+Proposition isembedding_pi_psect {n : nat} {X Y : pType}
+  (s : X ->* Y) (r : Y ->* X) (k : r o* s ==* pmap_idmap)
+  : IsEmbedding (fmap (pPi n) s).
+Proof.
+  apply isembedding_isinj_hset.
+  rapply isinj_section.
+  intro x.
+  refine (_ @ (fmap2 (pPi n) k) x @ _).
+  2: exact (fmap_id (pPi n) X x).
+  exact (fmap_comp (pPi n) s r x)^.
+Defined.
+
 Definition pequiv_pi_connmap `{Univalence} (n : nat) {X Y : pType} (f : X ->* Y)
   `{!IsConnMap n f}
   : Pi n X <~>* Pi n Y

theories/Homotopy/Hopf.v

@@ -0,0 +1,69 @@
+Require Import Types Basics Pointed Truncations.
+Require Import HSpace Suspension ExactSequence HomotopyGroup.
+Require Import WildCat Modalities.ReflectiveSubuniverse.
+Require Import HSet Spaces.Nat.
+
+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).
+
+We have not yet included various standard results about the Hopf construction, such as the total space being the join of the fibre. *)
+
+(** The Hopf construction associated to a left-invertible H-space (Definition 8.5.6 in the HoTT book). *)
+Definition hopf_construction `{Univalence} (X : pType)
+  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
+  : pFam (psusp X).
+Proof.
+  srapply Build_pFam.
+  - apply (Susp_rec (Y:=Type) X X).
+    exact (fun x => path_universe (x *.)).
+  - simpl. exact pt.
+Defined.
+
+Lemma transport_hopf_construction `{Univalence} {X : pType}
+  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
+  : forall x y : X, transport (hopf_construction X) (merid x) y = x * y.
+Proof.
+  intros x y.
+  transport_to_ap.
+  refine (ap (fun z => transport idmap z y) _ @ _).
+  1: apply Susp_rec_beta_merid.
+  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). *)
+Proposition hopf_retraction `{Univalence} (X : pType)
+  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
+  : connecting_map_family (hopf_construction X) o* loop_susp_unit X
+    ==* pmap_idmap.
+Proof.
+  nrapply hspace_phomotopy_from_homotopy.
+  1: assumption.
+  intro x; cbn.
+  refine (transport_pp _ _ _ _ @ _); unfold dpoint.
+  apply moveR_transport_V.
+  refine (transport_hopf_construction _ _
+            @ _ @ (transport_hopf_construction _ _)^).
+  exact (right_identity _ @ (left_identity _)^).
+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). *)
+Proposition freudenthal_hspace `{Univalence}
+  {n : nat} {X : pType} `{IsConnected n X}
+  `{IsHSpace X} `{forall a, IsEquiv (a *.)}
+  : IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)).
+Proof.
+  nrapply isequiv_surj_emb.
+  - apply issurj_pi_connmap.
+    destruct n.
+    + by apply (conn_map_loop_susp_unit (-1)).
+    + rewrite <- trunc_index_add_nat_add.
+      by apply (conn_map_loop_susp_unit).
+  - nrapply isembedding_pi_psect.
+    apply hopf_retraction.
+Defined.

theories/Modalities/Modality.v

@@ -373,6 +373,19 @@ Global Instance conn_map_to_O {O : Modality} (A : Type)
   : IsConnMap O (to O A)
   := _.
 
+(** When [O1 <= O2], [O_functor O2] preserves [O1]-connected maps. *)
+Proposition conn_map_O_functor_leq {O1 O2 : Modality} (leq : O1 <= O2)
+  {X Y : Type} (f : X -> Y) `{IsConnMap O1 _ _ f}
+  : IsConnMap O1 (O_functor O2 f).
+Proof.
+  nrapply (cancelR_conn_map _ (to O2 _)).
+  1: rapply conn_map_O_leq.
+  nrapply conn_map_homotopic.
+  1: intro x; symmetry; apply O_rec_beta.
+  rapply conn_map_compose.
+  rapply conn_map_O_leq.
+Defined.
+
 
 (** ** Easy modalities *)
 

theories/Pointed/Loops.v

@@ -40,6 +40,17 @@ Proof.
   reflexivity.
 Defined. 
 
+(** The connecting map associated to a pointed family. *)
+Definition connecting_map_family {X : pType} (P : pFam X)
+  : loops X ->* [P pt, dpoint P].
+Proof.
+  srapply Build_pMap.
+  - intro l.
+    apply (transport P l).
+    apply P.
+  - reflexivity.
+Defined.
+
 (** ** Functoriality of loop spaces *)
 
 (** Action on 1-cells *)

theories/Spaces/Nat/Core.v

@@ -727,3 +727,19 @@ Lemma not_lt_n_0 n : ~ (n < 0).
 Proof.
   apply not_leq_Sn_0.
 Defined.
+
+(** ** Arithmetic relations between [trunc_index] and [nat]. *)
+
+Lemma trunc_index_add_nat_add (n : nat)
+  : trunc_index_add n n = n.+1 + n.+1.
+Proof.
+  induction n as [|n IH]; only 1: reflexivity.
+  refine (trunc_index_add_succ _ _ @ _).
+  refine (ap trunc_S _ @ _).
+  { refine (trunc_index_add_comm _ _ @ _).
+    refine (trunc_index_add_succ _ _ @ _).
+    exact (ap trunc_S IH). }
+  refine (_ @ ap nat_to_trunc_index _).
+  2: exact (ap _ (add_Sn_m _ _)^ @ add_n_Sm _ _).
+  reflexivity.
+Defined.