Merge pull request #1814 from jarlg/prop-2.19

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/ExactSequence.v

@@ -485,6 +485,16 @@ Proof.
   - exact (pfiber2_fmap_loops f).
 Defined.
 
+(** The connecting map associated to a pointed family. *)
+Definition connecting_map_family {Y : pType} (P : pFam Y)
+  : loops Y ->* [P pt, dpoint P].
+Proof.
+  srapply Build_pMap.
+  - intro l.
+    apply (transport P l).
+    apply P.
+  - reflexivity.
+Defined.
 
 (** ** Long exact sequences *)
 

theories/Homotopy/HomotopyGroup.v

@@ -1,6 +1,6 @@
-Require Import Basics Types Pointed.
+Require Import Basics Types Pointed HSet.
 Require Import Modalities.Modality.
-Require Import Truncations.Core.
+Require Import Truncations.Core Truncations.SeparatedTrunc.
 Require Import Algebra.AbGroups.
 Require Import WildCat.
 
@@ -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).
@@ -314,3 +318,34 @@ Definition pequiv_pi_Tr `{Univalence} (n : nat) (X : pType)
 Definition grp_iso_pi_Tr `{Univalence} (n : nat) (X : pType)
   : GroupIsomorphism (Pi n.+1 X) (Pi n.+1 (pTr n.+1 X))
   := grp_iso_pi_connmap n ptr.
+
+(** 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_strong_leq.
+  by apply issurj_iterated_loops_connmap.
+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 (r:=fmap (pPi n) r)).
+  intro x.
+  lhs_V rapply (fmap_comp (pPi n) s r x).
+  lhs rapply (fmap2 (pPi n) k x).
+  exact (fmap_id (pPi n) X x).
+Defined.
+

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,17 @@ 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_strong_leq {O1 O2 : ReflectiveSubuniverse} (leq : O1 << O2)
+  {X Y : Type} (f : X -> Y) `{IsConnMap O1 _ _ f}
+  : IsConnMap O1 (O_functor O2 f).
+Proof.
+  rapply (cancelR_conn_map _ (to O2 _)).
+  nrapply conn_map_homotopic.
+  1: symmetry; apply to_O_natural.
+  rapply conn_map_compose.
+Defined.
+
 
 (** ** Easy modalities *)
 

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.