Timings for Hopf.v
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.
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). *)
(** 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).
apply (Susp_rec (Y:=Type) X X).
exact (fun x => path_universe (x *.)).
(** ** 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)
`{IsHSpace X} `{forall a, IsEquiv (a *.)} `{forall a, IsEquiv (.* a)}
: psigma (hopf_construction X) <~>* pjoin X X.
refine (_ oE equiv_pod_flatten (f := const_tt X) (g := const_tt X)
(@Build_poDescent _ _ _ (const_tt X) (const_tt X)
(Unit_ind (pointed_type X)) (Unit_ind (pointed_type X))
(fun x => Build_Equiv _ _ (x *.) (H1 x)))).
(* The equivalence [{x : X & X} <~> X * X] that we need sends [(x; y) to (y, x*y)]. *)
refine (equiv_sigma_prod0 _ _ oE _ oE equiv_sigma_symm0 _ _).
snapply equiv_functor_sigma_id.
exact (Build_Equiv _ _ (.* x) _).
1,2: exact (equiv_contr_sigma (Unit_ind (pointed_type X))).
(** ** Miscellaneous lemmas and corollaries about the Hopf construction *)
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.
refine (ap (fun z => transport idmap z y) _ @ _).
1: apply Susp_rec_beta_merid.
apply transport_path_universe.
(** 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
==* pmap_idmap.
napply hspace_phomotopy_from_homotopy.
refine (transport_pp _ _ _ _ @ _); unfold dpoint.
refine (transport_hopf_construction _ _
@ _ @ (transport_hopf_construction _ _)^).
exact (right_identity _ @ (left_identity _)^).
(** 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}
: IsEquiv (fmap (pPi (n + n).+1) (loop_susp_unit X)).
by apply (conn_map_loop_susp_unit (-1)).
rewrite <- trunc_index_add_nat_add.
by apply (conn_map_loop_susp_unit).
pose (is0connected_isconnected n.-2 _).
napply isembedding_pi_psect.
(** 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}
`{IsHSpace X} `{forall a, IsEquiv (a *.)}
: O_inverts (Tr (m +2+ m).+1) (loop_susp_unit X).
set (r:=connecting_map_family (hopf_construction X)).
napply (OO_inverts_conn_map_factor_conn_map _ (m +2+ m) _ r).
rapply (conn_map_homotopic _ equiv_idmap (r o loop_susp_unit X)).
(** Note that we don't really need the assumption that [X] is left-invertible in the previous result; for [m >= -1], it follows from connectivity. And for [m = -2], the conclusion is trivial. Here we state the version for [m >= -1] without left-invertibility. *)
Definition freudenthal_hspace `{Univalence}
{m : trunc_index} (X : pType) `{IsConnected m.+2 X}
`{IsHSpace X}
: O_inverts (Tr (m.+1 +2+ m.+1).+1) (loop_susp_unit X).
pose (is0connected_isconnected m _).
exact (freudenthal_hspace' (m:=m.+1) X).
(** Here we give a generalization of a result from Eilenberg-Mac Lane Spaces in Homotopy Type Theory, Dan Licata and Eric Finster. Their version corresponds to [m = -2] in our version. Their encode-decode proof was formalized in this library in EMSpace.v until this shorter and more general approach was found. *)
Definition licata_finster `{Univalence}
{m : trunc_index} (X : pType) `{IsConnected m.+2 X}
(k := (m.+1 +2+ m.+1).+1) `{IsHSpace X} `{IsTrunc k X}
: X <~>* pTr k (loops (psusp X)).
refine (_ o*E pequiv_ptr (n:=k)).
nrefine (pequiv_O_inverts k (loop_susp_unit X)).
rapply freudenthal_hspace.
(** Since [loops X] is an H-space, the Hopf construction provides a map [Join (loops X) (loops X) -> Susp (loops X)]. We show that this map is equivalent to the fiber of [loop_susp_counit X : Susp (loops X) -> X] over the base point, up to the automorphism of [Susp (loops X)] induced by inverting loops. *)
Definition pequiv_pfiber_loops_susp_counit_join `{Univalence} (X : pType)
: pfiber (loop_susp_counit X) <~>* pjoin (loops X) (loops X).
snrefine (pequiv_hopf_total_join (loops X) o*E _).
snapply equiv_functor_sigma'.
1: exact (emap psusp (equiv_path_inverse _ _)).
lhs rapply (transport_equiv (merid p) _ q).
lhs napply transport_paths_Fl.
lhs napply (ap inverse (ap_V _ _)).
apply Susp_rec_beta_merid.
lhs napply (transport_idmap_ap _ (merid p)).
lhs napply (transport2 idmap).
1: apply functor_susp_beta_merid.
apply Susp_rec_beta_merid.
lhs napply transport_path_universe.
(** As a corollary we get 2n-connectivity of [loop_susp_counit X] for an n-connected [X]. *)
Instance conn_map_loop_susp_counit `{Univalence}
{n : trunc_index} (X : pType) `{IsConnected n.+1 X}
: IsConnMap (n +2+ n) (loop_susp_counit X).
snapply (conn_point_elim (-1)).
exact (isconnected_pred_add' n 0 _).
napply (isconnected_equiv' _ _ (pequiv_pfiber_loops_susp_counit_join X)^-1).
napply isconnected_join; exact _.
(** In particular, we get the following result. All we are really using is that [n.+2 <= n +2+ n], but because of the use of [isconnmap_pred_add], the proof is a bit more specific to this case. *)
Definition pequiv_ptr_psusp_loops `{Univalence} (X : pType) (n : nat) `{IsConnected n.+1 X}
: pTr n.+2 (psusp (loops X)) <~>* pTr n.+2 X.
1: exact (fmap (pTr _) (loop_susp_counit _)).
napply O_inverts_conn_map.
napply (isconnmap_pred_add n.-2).
rewrite 2 trunc_index_add_succ.
exact (conn_map_loop_susp_counit X).