diff --git a/theories/Algebra/AbSES/Classification.v b/theories/Algebra/AbSES/Classification.v new file mode 100644 index 00000000000..8b6ddd33e0c --- /dev/null +++ b/theories/Algebra/AbSES/Classification.v @@ -0,0 +1,1125 @@ +From HoTT Require Import Basics Types Truncations.Core + Truncations.Connectedness Truncations.SeparatedTrunc. +From HoTT.WildCat Require Import Core Equiv. +Require Import Pointed. +Require Import AbelianGroup. +Require Import Algebra.AbSES.Core Algebra.AbSES.Ext. +Require Import Universes.Smallness. +Require Import Homotopy.HomotopyGroup Homotopy.EMSpace Homotopy.ExactSequence. +Require Import Groups.Group. +Require Import HSet. +Require Import Modalities.Identity Modalities.Descent. + +(** * Classification of short exact sequences + + Short exact sequences [A -> E -> B] of abelian groups are classified by + pointed maps [K(B,2) ->* K(A,3)] (Christensen and Flaten, "Ext groups in + homotopy type theory", Theorem 2.2.2). *) + +Local Open Scope pointed_scope. + +(** ** Vanishing of homotopy groups *) + +(** Homotopy groups below the connectivity vanish. *) +Definition contr_pi_isconnected `{Univalence} (n : nat) (X : pType) + `{IsConnected n X} + : Contr (Pi n X). +Proof. + revert X H0; induction n; intros X H0. + - exact H0. + - nrefine (contr_equiv' (Pi n (loops X)) _). + 1: exact (pi_loops n X)^-1*. + napply IHn. + rapply isconnected_loops. +Defined. + +(** A successor-connectivity criterion: an [n.+1]-connected type with + trivial [Pi n.+2] is [n.+2]-connected. *) +Definition isconnected_succ_contr_pi `{Univalence} (n : nat) (X : pType) + `{IsConnected n.+1 X} (c : Contr (Pi n.+2 X)) + : IsConnected n.+2 X. +Proof. + pose proof (isconnected_trunc n.+1 n.+2 (X := X)). + nrefine (contr_equiv' K(Build_AbGroup (Pi n.+2 (pTr n.+2 X)) _, n.+2) _). + 1: exact (pequiv_em_connected_truncated (pTr n.+2 X) n.+1). + napply contr_em_contr. + nrefine (contr_equiv' (Pi n.+2 X) _). + 1: exact (grp_iso_pi_Tr n.+1 X). + exact c. + Unshelve. + all: exact _. +Defined. + +(** ** Injectivity of homotopy groups of fiber inclusions + + If the [n.+1]-st homotopy group of the double fiber of [g] vanishes, + then [Pi n.+1] of the fiber inclusion of [g] is an embedding. *) +Instance isembedding_pi_pfib `{Univalence} {X Y : pType} (g : X ->* Y) + (n : nat) `{Contr (Pi n.+1 (pfiber (pfib g)))} + : IsEmbedding (fmap (Pi n.+1) (pfib g)). +Proof. + snapply isembedding_istrivial_kernel. + intros z w. + pose proof (c := @center _ + (conn_map_isexact + (i := fmap (pTr 0) (fmap (iterated_loops n.+1) (pfib (pfib g)))) + (f := fmap (pTr 0) (fmap (iterated_loops n.+1) (pfib g))) + (z; w))). + strip_truncations. + destruct c as [u q]. + refine ((ap pr1 q)^ @ _). + refine (ap _ (path_contr u (point _)) @ _). + exact (point_eq (fmap (pTr 0) (fmap (iterated_loops n.+1) + (pfib (pfib g))))). +Defined. + +Section EMFiberSequence. + Context `{Univalence} {B A : AbGroup@{u}} (E : AbSES B A) (n : nat). + + (** Applying [K(-,n.+1)] to a short exact sequence yields a complex. *) + Definition iscomplex_em_abses + : IsComplex (em_fmap (inclusion E) n.+1) (em_fmap (projection E) n.+1). + Proof. + refine ((em_fmap_compose (inclusion E) (projection E) n.+1)^* @* _). + refine (phomotopy_path + (ap (fun h => em_fmap h n.+1) (_ : _ = grp_homo_const)) + @* em_fmap_const n.+1). + apply equiv_path_grouphomomorphism; intro a. + exact (iscomplex_abses E a). + Defined. + + (** The [n.+1]-st homotopy group of the double fiber of + [em_fmap (projection E) n.+1] vanishes. *) + Local Instance contr_pi_pfiber_pfib + : Contr (Pi n.+1 (pfiber (pfib (em_fmap (projection E) n.+1)))). + Proof. + nrefine (contr_equiv' (Pi n.+2 K(B, n.+1)) _). + 1: exact (grp_iso_compose + (groupiso_pi_functor n + (pequiv_inverse (pfiber2_loops (em_fmap (projection E) n.+1)))) + (groupiso_pi_loops n K(B, n.+1))). + exact (contr_pi_succ_istrunc n K(B, n.+1)). + Defined. + + (** [Pi n.+1] of the comparison map [cxfib] is surjective. *) + Local Definition issurj_pi_cxfib + : IsSurjection (fmap (Pi n.+1) (cxfib iscomplex_em_abses)). + Proof. + intro y. + rapply contr_inhabited_hprop. + (* The image of [y] in [Pi n.+1 K(E, n.+1)] is killed by the projection. *) + pose (x := fmap (Pi n.+1) (pfib (em_fmap (projection E) n.+1)) y). + pose proof (w := cx_isexact + (i := fmap (pTr 0) (fmap (iterated_loops n.+1) + (pfib (em_fmap (projection E) n.+1)))) + (f := fmap (pTr 0) (fmap (iterated_loops n.+1) + (em_fmap (projection E) n.+1))) + y). + (* Hence its preimage in [E] is killed by [projection E]. *) + pose (ee := (equiv_g_pi_n_em E n)^-1 x). + assert (pe : projection E ee = mon_unit). + { apply (equiv_inj (equiv_g_pi_n_em B n)). + refine ((pi_em_fmap (projection E) n ee)^ @ _). + refine (ap (fmap (Pi n.+1) (em_fmap (projection E) n.+1)) + (eisretr (equiv_g_pi_n_em E n) x) @ _). + refine (w @ _). + exact (grp_homo_unit (equiv_g_pi_n_em B n))^. } + (* By exactness, [ee] merely comes from [A]. *) + pose proof (m := @center _ (conn_map_isexact + (i := inclusion E) (f := projection E) (ee; pe))). + strip_truncations. + destruct m as [a q]. + apply tr. + exists (equiv_g_pi_n_em A n a). + (* The two candidates agree after the embedding [pi (pfib _)]. *) + napply (isinj_embedding _ + (isembedding_pi_pfib (em_fmap (projection E) n.+1) n)). + 1: exact _. + refine ((fmap_comp (Pi n.+1) (cxfib iscomplex_em_abses) + (pfib (em_fmap (projection E) n.+1)) _)^ @ _). + refine (fmap2 (Pi n.+1) (pfib_cxfib _) _ @ _). + refine (pi_em_fmap (inclusion E) n a @ _). + exact (ap (equiv_g_pi_n_em E n) (ap pr1 q) @ eisretr _ x). + Defined. + + (** Therefore the comparison map is an equivalence: it is an isomorphism + on [Pi n.+1], and both sides are [n]-connected and [n.+1]-truncated. *) + Local Instance isequiv_pi_cxfib + : IsEquiv (fmap (Pi n.+1) (cxfib iscomplex_em_abses)). + Proof. + apply isequiv_surj_emb. + 1: exact issurj_pi_cxfib. + snapply isembedding_istrivial_kernel. + intros z w. + (* [z] is killed by [Pi n.+1] of [em_fmap (inclusion E) n.+1]. *) + assert (wi : fmap (Pi n.+1) (em_fmap (inclusion E) n.+1) z = mon_unit). + { refine ((fmap2 (Pi n.+1) (pfib_cxfib _) z)^ @ _). + refine (fmap_comp (Pi n.+1) (cxfib iscomplex_em_abses) + (pfib (em_fmap (projection E) n.+1)) z @ _). + refine (ap (fmap (Pi n.+1) (pfib (em_fmap (projection E) n.+1))) w @ _). + apply grp_homo_unit. } + (* Hence [z] vanishes, since the inclusion is an embedding. *) + pose (a := (equiv_g_pi_n_em A n)^-1 z). + refine ((eisretr (equiv_g_pi_n_em A n) z)^ @ _). + refine (ap (equiv_g_pi_n_em A n) (_ : a = mon_unit) @ _). + 2: apply grp_homo_unit. + rapply (isinj_embedding (inclusion E)). + refine (_ @ (grp_homo_unit (inclusion E))^). + apply (equiv_inj (equiv_g_pi_n_em E n)). + refine ((pi_em_fmap (inclusion E) n a)^ @ _). + refine (ap (fmap (Pi n.+1) (em_fmap (inclusion E) n.+1)) + (eisretr (equiv_g_pi_n_em A n) z) @ _). + refine (wi @ _). + exact (grp_homo_unit (equiv_g_pi_n_em E n))^. + Defined. + + (** Both sides of the comparison map are [n]-connected and + [n.+1]-truncated, so it is an equivalence. *) + Local Instance isequiv_cxfib_em : IsEquiv (cxfib iscomplex_em_abses). + Proof. + pose proof (isconnmap_em_fmap (projection E) n (point _)). + (* The identification of [A] with the fiber's homotopy group. *) + pose (psi := grp_iso_compose + (Build_GroupIsomorphism _ _ _ isequiv_pi_cxfib) + (equiv_g_pi_n_em A n)). + (* The induced equivalence onto the fiber. *) + pose (omega := pequiv_em_connected_truncated + (pfiber (em_fmap (projection E) n.+1)) n + o*E pequiv_em_group_iso n.+1 psi). + (* The conjugated comparison map is [em_fmap] of an isomorphism. *) + pose (chi := grp_iso_compose (grp_iso_inverse (equiv_g_pi_n_em A n)) + (grp_iso_compose (groupiso_pi_functor n (pequiv_inverse omega)) + (grp_iso_compose (Build_GroupIsomorphism _ _ _ isequiv_pi_cxfib) + (equiv_g_pi_n_em A n)))). + assert (q : em_fmap chi n.+1 + = pequiv_inverse omega o* cxfib iscomplex_em_abses). + { apply path_em_pmap_pi; intro u. + refine (ap (fmap (Pi n.+1) (em_fmap chi n.+1)) + (eisretr (equiv_g_pi_n_em A n) u)^ @ _). + refine (pi_em_fmap chi n ((equiv_g_pi_n_em A n)^-1 u) @ _). + refine (eisretr (equiv_g_pi_n_em A n) _ @ _). + refine (ap (fun v => fmap (Pi n.+1) (pequiv_inverse omega) + (fmap (Pi n.+1) (cxfib iscomplex_em_abses) v)) + (eisretr (equiv_g_pi_n_em A n) u) @ _). + exact (fmap_comp (Pi n.+1) (cxfib iscomplex_em_abses) + (pequiv_inverse omega) u)^. + } + snapply (isequiv_homotopic + (omega o (pequiv_inverse omega o* cxfib iscomplex_em_abses))). + - napply isequiv_compose. + 2: exact _. + exact (transport (fun (g : _ ->* _) => IsEquiv g) q + (pointed_isequiv _ _ (pequiv_em_fmap chi n.+1))). + - intro x; exact (eisretr omega _). + Defined. + + (** [K(-, n.+1)] sends short exact sequences of abelian groups to fiber + sequences of Eilenberg-Mac Lane spaces. *) + #[export] Instance isexact_em_abses + : IsExact purely (em_fmap (inclusion E) n.+1) + (em_fmap (projection E) n.+1). + Proof. + exists iscomplex_em_abses. + rapply conn_map_isequiv. + Defined. + +End EMFiberSequence. + +(** ** The classifying map of a short exact sequence + + The connecting map of the fiber sequence [K(A,3) -> K(E,3) -> K(B,3)], + expressed as a pointed map [K(B,2) ->* K(A,3)]. *) +Definition abses_classifying_map `{Univalence} {B A : AbGroup@{u}} + (E : AbSES B A) + : K(B, 2) ->* K(A, 3) + := connecting_map (em_fmap (inclusion E) 3) (em_fmap (projection E) 3) + o* pequiv_loops_em_em B 2. + +(** ** The short exact sequence of a pointed map + + Conversely, a pointed map [f : K(B,2) ->* K(A,3)] yields a short exact + sequence [A -> Pi 2 (pfiber f) -> B], by rotating the fiber sequence of + [f] and taking homotopy groups. *) + +(** The retraction law for [grp_iso_inverse], in the group-homomorphism + spelling. *) +Local Definition grp_iso_retr {G H : Group} (e : GroupIsomorphism G H) + (x : H) + : e (grp_iso_inverse e x) = x. +Proof. + destruct e; exact (eisretr _ x). +Defined. + +(** The companion section law. *) +Local Definition grp_iso_sect {G H : Group} (e : GroupIsomorphism G H) + (x : G) + : grp_iso_inverse e (e x) = x. +Proof. + destruct e; exact (eissect _ x). +Defined. + +Section AbSESPfiber. + Context `{Univalence} {B A : AbGroup@{u}} (n : nat) + (f : K(B, n.+2) ->* K(A, n.+3)). + + (** The middle group: [Pi n.+2] of the fiber, abelian by + Eckmann-Hilton. *) + Definition abgroup_pi_pfiber : AbGroup + := Build_AbGroup (Pi n.+2 (pfiber f)) _. + + (** The inclusion, through the rotated fiber sequence + [loops K(A,n+3) -> pfiber f -> K(B,n+2)]. *) + Definition abses_pfiber_incl : A $-> abgroup_pi_pfiber. + Proof. + nrefine (grp_homo_compose _ + (grp_homo_compose (groupiso_pi_loops n.+1 K(A, n.+3)) + (equiv_g_pi_n_em A n.+2))). + exact (fmap (Pi n.+2) (connecting_map (pfib f) f)). + Defined. + + (** The projection, induced by the fiber inclusion of [f]. *) + Definition abses_pfiber_proj : abgroup_pi_pfiber $-> B. + Proof. + nrefine (grp_homo_compose + (grp_iso_inverse (equiv_g_pi_n_em B n.+1)) _). + exact (fmap (Pi n.+2) (pfib f)). + Defined. + + (** The [n.+2]-nd homotopy group of the double fiber of [pfib f] + vanishes. *) + Local Instance contr_pi_pfiber2 + : Contr (Pi n.+2 (pfiber (pfib (pfib f)))). + Proof. + nrefine (contr_equiv' (Pi n.+3 K(B, n.+2)) _). + 1: exact (grp_iso_compose + (groupiso_pi_functor n.+1 (pequiv_inverse (pfiber2_loops (pfib f)))) + (groupiso_pi_loops n.+1 K(B, n.+2))). + exact (contr_pi_succ_istrunc n.+1 K(B, n.+2)). + Defined. + + (** The [n.+2]-nd homotopy group of [K(A,n+3)] vanishes. *) + Local Instance contr_pi_em : Contr (Pi n.+2 K(A, n.+3)). + Proof. + exact (contr_pi_isconnected n.+2 K(A, n.+3)). + Defined. + + Local Instance isembedding_abses_pfiber_incl + : IsEmbedding abses_pfiber_incl. + Proof. + snapply isembedding_istrivial_kernel. + intros a w. + (* The image of [a] in [Pi n.+2 (loops K(A,n+3))]. *) + pose (z := groupiso_pi_loops n.+1 K(A, n.+3) (equiv_g_pi_n_em A n.+2 a)). + assert (wz : fmap (Pi n.+2) ((connect_fiberseq (pfib f) f).2) z + = mon_unit). + { napply (isinj_embedding _ (isembedding_pi_pfib (pfib f) n.+1)). + 1: exact _. + refine ((fmap_comp (Pi n.+2) + ((connect_fiberseq (pfib f) f).2 : _ ->* _) + (pfib (pfib f)) z)^ @ _). + refine (w @ _). + exact (grp_homo_unit (fmap (Pi n.+2) (pfib (pfib f))))^. } + apply (equiv_inj (equiv_g_pi_n_em A n.+2)). + apply (equiv_inj (groupiso_pi_loops n.+1 K(A, n.+3))). + apply (equiv_inj (groupiso_pi_functor n.+1 + ((connect_fiberseq (pfib f) f).2))). + refine (wz @ _). + symmetry. + refine (ap _ (ap _ (grp_homo_unit (equiv_g_pi_n_em A n.+2))) @ _). + refine (ap _ (grp_homo_unit (groupiso_pi_loops n.+1 K(A, n.+3))) @ _). + exact (grp_homo_unit (groupiso_pi_functor n.+1 + ((connect_fiberseq (pfib f) f).2))). + Defined. + + Local Definition issurjection_abses_pfiber_proj + : IsSurjection abses_pfiber_proj. + Proof. + intro b. + rapply contr_inhabited_hprop. + pose proof (c := @center _ (conn_map_isexact + (i := fmap (pTr 0) (fmap (iterated_loops n.+2) (pfib f))) + (f := fmap (pTr 0) (fmap (iterated_loops n.+2) f)) + (equiv_g_pi_n_em B n.+1 b; path_contr _ _))). + strip_truncations. + destruct c as [u q]. + apply tr. + exists u. + apply (equiv_inj (equiv_g_pi_n_em B n.+1)). + refine (grp_iso_retr (equiv_g_pi_n_em B n.+1) _ @ _). + exact (ap pr1 q). + Defined. + + Local Instance isexact_abses_pfiber + : IsExact (Tr (-1)) abses_pfiber_incl abses_pfiber_proj. + Proof. + snapply Build_IsExact. + - (* The composite is constant. *) + srapply phomotopy_homotopy_hset. + intro a. + refine (ap (grp_iso_inverse (equiv_g_pi_n_em B n.+1)) _ + @ grp_homo_unit (grp_iso_inverse (equiv_g_pi_n_em B n.+1))). + refine (ap (fmap (Pi n.+2) (pfib f)) + (fmap_comp (Pi n.+2) ((connect_fiberseq (pfib f) f).2 : _ ->* _) + (pfib (pfib f)) _) @ _). + exact (cx_isexact + (i := fmap (pTr 0) (fmap (iterated_loops n.+2) (pfib (pfib f)))) + (f := fmap (pTr 0) (fmap (iterated_loops n.+2) (pfib f))) + (fmap (Pi n.+2) ((connect_fiberseq (pfib f) f).2) + (grp_homo_compose (groupiso_pi_loops n.+1 K(A, n.+3)) + (equiv_g_pi_n_em A n.+2) a))). + - (* Every element of the kernel merely comes from [A]. *) + intros [x w]. + rapply contr_inhabited_hprop. + assert (w' : fmap (Pi n.+2) (pfib f) x = mon_unit). + { refine ((grp_iso_retr (equiv_g_pi_n_em B n.+1) _)^ @ _ + @ grp_homo_unit (equiv_g_pi_n_em B n.+1)). + exact (ap (equiv_g_pi_n_em B n.+1) w). } + pose proof (c := @center _ (conn_map_isexact + (i := fmap (pTr 0) (fmap (iterated_loops n.+2) (pfib (pfib f)))) + (f := fmap (pTr 0) (fmap (iterated_loops n.+2) (pfib f))) + (x; w'))). + strip_truncations. + destruct c as [u q]. + apply tr. + pose (v := fmap (Pi n.+2) + (pequiv_inverse (connect_fiberseq (pfib f) f).2) u + : Pi n.+2 (loops K(A, n.+3))). + exists ((equiv_g_pi_n_em A n.+2)^-1 + ((groupiso_pi_loops n.+1 K(A, n.+3))^-1 v)). + apply path_sigma_hprop. + refine (ap (fmap (Pi n.+2) (connecting_map (pfib f) f)) + (ap (groupiso_pi_loops n.+1 K(A, n.+3)) + (eisretr (equiv_g_pi_n_em A n.+2) _) + @ eisretr (groupiso_pi_loops n.+1 K(A, n.+3)) _) @ _). + refine (fmap_comp (Pi n.+2) + ((connect_fiberseq (pfib f) f).2 : _ ->* _) + (pfib (pfib f)) _ @ _). + refine (ap (fmap (Pi n.+2) (pfib (pfib f))) _ @ ap pr1 q). + refine ((fmap_comp (Pi n.+2) + (pequiv_inverse (connect_fiberseq (pfib f) f).2 : _ ->* _) + ((connect_fiberseq (pfib f) f).2 : _ ->* _) u)^ @ _). + refine (fmap2 (Pi n.+2) + (peisretr ((connect_fiberseq (pfib f) f).2)) u @ _). + exact (fmap_id (Pi n.+2) _ u). + Defined. + + (** The short exact sequence associated to [f]. *) + Definition abses_pfiber : AbSES B A + := Build_AbSES abgroup_pi_pfiber abses_pfiber_incl abses_pfiber_proj + _ issurjection_abses_pfiber_proj _. + +End AbSESPfiber. + +Section PfiberDeloop. + Context `{Univalence} {B A : AbGroup@{u}} (psi : K(B, 3) ->* K(A, 4)). + + (** The fiber of a map [K(B,3) ->* K(A,4)] is 3-truncated. *) + Local Instance istrunc_pfiber_em : IsTrunc 3 (pfiber psi) + := _. + + (** Its second homotopy group is trivial: it embeds in the trivial + [Pi 2 K(B,3)], since the second homotopy group of the double fiber + is [Pi 3 K(A,4)], which is also trivial. *) + Local Instance contr_pi2_pfiber_em : Contr (Pi 2 (pfiber psi)). + Proof. + assert (contr_pi2_pfib2 : Contr (Pi 2 (pfiber (pfib psi)))). + { nrefine (contr_equiv' (Pi 3 K(A, 4)) _). + 1: exact (grp_iso_compose + (groupiso_pi_functor 1 (pequiv_inverse (pfiber2_loops psi))) + (groupiso_pi_loops 1 K(A, 4))). + exact (contr_pi_isconnected 3 K(A, 4)). } + apply (Build_Contr _ mon_unit). + intro y. + napply (isinj_embedding _ (isembedding_pi_pfib psi 1)). + 1: exact _. + napply path_contr. + exact (contr_pi_isconnected 2 K(B, 3)). + Defined. + + (** The fiber is 2-connected. *) + Local Instance isconnected_pfiber_em : IsConnected 2 (pfiber psi). + Proof. + napply (isconnected_succ_contr_pi 0). + - pose @O_lex_leq_Tr. + pose proof (@isconnected_pred 2 K(A, 4) (isconnected_em 3)). + pose proof (isconnected_em (G:=B) 2). + rapply OO_isconnected_hfiber. + - exact _. + Defined. + + (** The fiber is the Eilenberg-Mac Lane space of its third homotopy + group. *) + Local Definition pequiv_em_pfiber_psi + : K(abgroup_pi_pfiber 1 psi, 3) <~>* pfiber psi + := pequiv_em_connected_truncated (pfiber psi) 2. + + (** The induced identification of third homotopy groups. *) + Local Definition eta_pfiber_psi + : GroupIsomorphism (abgroup_pi_pfiber 1 psi) (abgroup_pi_pfiber 1 psi) + := grp_iso_compose + (groupiso_pi_functor 2 pequiv_em_pfiber_psi) + (equiv_g_pi_n_em (abgroup_pi_pfiber 1 psi) 2). + + (** The bridge, twisted by [eta_pfiber_psi]. *) + Local Definition pequiv_em_pfiber_psi' + : K(abgroup_pi_pfiber 1 psi, 3) <~>* pfiber psi. + Proof. + snapply Build_pEquiv. + 1: exact (pequiv_em_pfiber_psi + o* pequiv_em_fmap (grp_iso_inverse eta_pfiber_psi) 3). + exact (isequiv_compose + (pequiv_em_fmap (grp_iso_inverse eta_pfiber_psi) 3) + pequiv_em_pfiber_psi). + Defined. + + (** On [Pi 3], the bridge inverts [equiv_g_pi_n_em], by construction. *) + Local Definition pi_bridge_psi (x : Pi 3 K(abgroup_pi_pfiber 1 psi, 3)) + : fmap (Pi 3) (pequiv_em_pfiber_psi' : _ ->* _) x + = grp_iso_inverse (equiv_g_pi_n_em (abgroup_pi_pfiber 1 psi) 2) x. + Proof. + refine (fmap_comp (Pi 3) + (em_fmap (grp_iso_inverse eta_pfiber_psi) 3) + (pequiv_em_pfiber_psi : _ ->* _) x @ _). + refine (ap (fmap (Pi 3) (pequiv_em_pfiber_psi : _ ->* _)) + (ap (fmap (Pi 3) (em_fmap (grp_iso_inverse eta_pfiber_psi) 3)) + (grp_iso_retr + (equiv_g_pi_n_em (abgroup_pi_pfiber 1 psi) 2) x)^) @ _). + refine (ap (fmap (Pi 3) (pequiv_em_pfiber_psi : _ ->* _)) + (pi_em_fmap (grp_iso_inverse eta_pfiber_psi) 2 _) @ _). + exact (grp_iso_retr eta_pfiber_psi _). + Defined. + + (** Through the bridge, [em_fmap] of the projection is the fiber + inclusion of [psi]. *) + Local Definition path_em_proj_pfib_psi + : em_fmap (abses_pfiber_proj 1 psi) 3 + = pfib psi o* pequiv_em_pfiber_psi'. + Proof. + snapply (path_em_pmap_pi_connected 1). + 1: exact (isconnected_em (G:=B) 2). + 1: exact _. + intro x. + refine (ap (fmap (Pi 3) (em_fmap (abses_pfiber_proj 1 psi) 3)) + (grp_iso_retr (equiv_g_pi_n_em (abgroup_pi_pfiber 1 psi) 2) x)^ + @ _). + refine (pi_em_fmap (abses_pfiber_proj 1 psi) 2 _ @ _). + refine (grp_iso_retr (equiv_g_pi_n_em B 2) _ @ _). + refine (_ @ (fmap_comp (Pi 3) + (pequiv_em_pfiber_psi' : _ ->* _) (pfib psi) x)^). + exact (ap (fmap (Pi 3) (pfib psi)) (pi_bridge_psi x)^). + Defined. + + (** Through the bridge, [em_fmap] of the inclusion is the connecting + map of [psi], modulo the loop identification of [K(A,3)]. *) + Local Definition path_em_incl_delta_psi + : pequiv_em_pfiber_psi' o* em_fmap (abses_pfiber_incl 1 psi) 3 + = connecting_map (pfib psi) psi o* pequiv_loops_em_em A 3. + Proof. + snapply (path_em_pmap_pi_connected 1). + 1: exact _. + 1: exact _. + intro x. + refine (fmap_comp (Pi 3) + (em_fmap (abses_pfiber_incl 1 psi) 3) + (pequiv_em_pfiber_psi' : _ ->* _) x @ _). + refine (ap (fmap (Pi 3) (pequiv_em_pfiber_psi' : _ ->* _)) + (ap (fmap (Pi 3) (em_fmap (abses_pfiber_incl 1 psi) 3)) + (grp_iso_retr (equiv_g_pi_n_em A 2) x)^) @ _). + refine (ap (fmap (Pi 3) (pequiv_em_pfiber_psi' : _ ->* _)) + (pi_em_fmap (abses_pfiber_incl 1 psi) 2 _) @ _). + refine (pi_bridge_psi _ @ _). + refine (grp_iso_sect + (equiv_g_pi_n_em (abgroup_pi_pfiber 1 psi) 2) _ @ _). + refine (_ @ (fmap_comp (Pi 3) + (pequiv_loops_em_em A 3 : _ ->* _) + (connecting_map (pfib psi) psi) x)^). + refine (ap (fmap (Pi 3) (connecting_map (pfib psi) psi)) _). + refine (grp_iso_retr (groupiso_pi_loops 2 K(A, 4)) _ @ _). + exact (ap (fmap (Pi 3) (pequiv_loops_em_em A 3 : _ ->* _)) + (grp_iso_retr (equiv_g_pi_n_em A 2) x)). + Defined. + + (** The projection square as a square of pointed maps. *) + Local Definition square_em_proj_pfib_psi + : pequiv_pmap_idmap o* em_fmap (projection (abses_pfiber 1 psi)) 3 + ==* pfib psi o* pequiv_em_pfiber_psi' + := pmap_postcompose_idmap _ @* phomotopy_path path_em_proj_pfib_psi. + + (** The third homotopy group of the double fiber of [pfib psi] + vanishes, so [Pi 3] of its fiber inclusion is an embedding. *) + Local Instance contr_pi3_pfiber2_psi + : Contr (Pi 3 (pfiber (pfib (pfib psi)))) + := contr_pi_pfiber2 1 psi. + + (** Through the bridge, [cxfib] of the extracted sequence is the + connecting identification of [psi], modulo the loop identification + of [K(A,3)]. *) + Local Definition path_cxfib_connect_psi + : pequiv_pfiber pequiv_em_pfiber_psi' pequiv_pmap_idmap + square_em_proj_pfib_psi + o* pequiv_cxfib (i := em_fmap (inclusion (abses_pfiber 1 psi)) 3) + (f := em_fmap (projection (abses_pfiber 1 psi)) 3) + = (connect_fiberseq (pfib psi) psi).2 o* pequiv_loops_em_em A 3. + Proof. + snapply (path_em_pmap_pi_connected 1). + 1: exact (isconnected_equiv' 2 (loops K(A, 4)) + ((connect_fiberseq (pfib psi) psi).2) + (@isconnected_loops _ 2 K(A, 4) (isconnected_em 3))). + 1: exact _. + intro x. + napply (isinj_embedding _ (isembedding_pi_pfib (pfib psi) 2)). + 1: exact _. + refine (ap (fmap (Pi 3) (pfib (pfib psi))) + (fmap_comp (Pi 3) + (pequiv_cxfib (i := em_fmap (inclusion (abses_pfiber 1 psi)) 3) + (f := em_fmap (projection (abses_pfiber 1 psi)) 3) : _ ->* _) + (pequiv_pfiber pequiv_em_pfiber_psi' pequiv_pmap_idmap + square_em_proj_pfib_psi : _ ->* _) x) @ _). + refine ((fmap_comp (Pi 3) + (pequiv_pfiber pequiv_em_pfiber_psi' pequiv_pmap_idmap + square_em_proj_pfib_psi : _ ->* _) + (pfib (pfib psi)) _)^ @ _). + refine ((fmap2 (Pi 3) + (square_pequiv_pfiber pequiv_em_pfiber_psi' pequiv_pmap_idmap + square_em_proj_pfib_psi) _)^ @ _). + refine (fmap_comp (Pi 3) + (pfib (em_fmap (projection (abses_pfiber 1 psi)) 3)) + (pequiv_em_pfiber_psi' : _ ->* _) _ @ _). + refine (ap (fmap (Pi 3) (pequiv_em_pfiber_psi' : _ ->* _)) + ((fmap_comp (Pi 3) + (pequiv_cxfib (i := em_fmap (inclusion (abses_pfiber 1 psi)) 3) + (f := em_fmap (projection (abses_pfiber 1 psi)) 3) : _ ->* _) + (pfib (em_fmap (projection (abses_pfiber 1 psi)) 3)) x)^ + @ fmap2 (Pi 3) (pfib_cxfib _) x) @ _). + refine ((fmap_comp (Pi 3) + (em_fmap (abses_pfiber_incl 1 psi) 3) + (pequiv_em_pfiber_psi' : _ ->* _) x)^ @ _). + refine (ap (fun (m : _ ->* _) => fmap (Pi 3) m x) + path_em_incl_delta_psi @ _). + refine (fmap_comp (Pi 3) + (pequiv_loops_em_em A 3 : _ ->* _) + (connecting_map (pfib psi) psi) x @ _). + refine (fmap_comp (Pi 3) + ((connect_fiberseq (pfib psi) psi).2 : _ ->* _) + (pfib (pfib psi)) _ @ _). + exact (ap (fmap (Pi 3) (pfib (pfib psi))) + (fmap_comp (Pi 3) + (pequiv_loops_em_em A 3 : _ ->* _) + ((connect_fiberseq (pfib psi) psi).2 : _ ->* _) x))^. + Defined. + + (** The connecting identification of [psi] inverts [pfiber2_loops], + since the underlying [pequiv_pfiber] square is tautological. *) + Local Definition pfiber2_loops_connect_psi + : pfiber2_loops psi o* ((connect_fiberseq (pfib psi) psi).2 : _ ->* _) + ==* pmap_idmap. + Proof. + refine (pmap_prewhisker _ _ @* peisretr + ((pfiber2_loops psi) + o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib (pfib psi) psi)))). + refine (_ @* (compose_cate_fun (A:=pType) _ _)^*). + refine (_ @* (pmap_postwhisker _ (pequiv_pfiber_cxfib_taut psi) + @* pmap_precompose_idmap _)^*). + reflexivity. + Defined. + + (** Through the loop identification of [K(A,3)], the connecting map of + the extracted fiber sequence is [loops psi], twisted by loop + inversion. *) + Local Definition connecting_map_em_loops_psi + : pequiv_loops_em_em A 3 + o* connecting_map (em_fmap (inclusion (abses_pfiber 1 psi)) 3) + (em_fmap (projection (abses_pfiber 1 psi)) 3) + ==* fmap loops psi o* loops_inv K(B, 3). + Proof. + (* Insert the identity [pfiber2_loops psi o* connect] in front. *) + refine ((pmap_postcompose_idmap _)^* @* _). + refine (pmap_prewhisker _ pfiber2_loops_connect_psi^* @* _). + (* Reassociate to expose the connecting composite, then the cxfib + square. *) + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_postwhisker _ + (pmap_prewhisker _ (phomotopy_path path_cxfib_connect_psi^)) @* _). + (* Compare the connecting maps across the bridge. *) + refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _) @* _). + refine (pmap_postwhisker _ + (pmap_postwhisker _ (connecting_map_cxfib _ _)) @* _). + refine (pmap_postwhisker _ + (connecting_map_natural _ _ square_em_proj_pfib_psi) @* _). + refine (pmap_postwhisker _ + (pmap_postwhisker _ (fmap_id loops _) + @* pmap_precompose_idmap _) @* _). + exact (connecting_map_pfib2 psi). + Defined. + + (** Negation on [K(B,2)], as loop inversion conjugated by the loop + identification. *) + Local Definition pequiv_neg_em : K(B, 2) <~>* K(B, 2) + := (pequiv_loops_em_em B 2)^-1* + o*E (loops_inv K(B, 3) o*E pequiv_loops_em_em B 2). + + (** Under the loop identification, [pequiv_neg_em] is loop inversion. *) + Local Definition pequiv_neg_em_loops + : pequiv_loops_em_em B 2 o* pequiv_neg_em + ==* loops_inv K(B, 3) o* pequiv_loops_em_em B 2. + Proof. + refine (pmap_postwhisker _ + (compose_cate_fun (A:=pType) _ _) @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ (peisretr (pequiv_loops_em_em B 2)) @* _). + refine (pmap_postcompose_idmap _ @* _). + exact (compose_cate_fun (A:=pType) _ _). + Defined. + + (** The classifying map of the extracted sequence is the delooping + equivalence applied to [psi], twisted by [pequiv_neg_em]. *) + Local Definition abses_classifying_pfiber_deloop + : abses_classifying_map (abses_pfiber 1 psi) + ==* equiv_deloop_em_pmap B A 0 psi o* pequiv_neg_em. + Proof. + refine (_ @* (pmap_prewhisker pequiv_neg_em + (equiv_deloop_em_pmap_unfold B A 0 psi) + @* pmap_compose_assoc _ _ _ + @* pmap_postwhisker _ (pmap_compose_assoc _ _ _))^*). + refine (pmap_prewhisker (pequiv_loops_em_em B 2) + (moveL_pequiv_Vf _ _ _ connecting_map_em_loops_psi) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _) @* _). + napply pmap_postwhisker. + napply pmap_postwhisker. + symmetry; exact pequiv_neg_em_loops. + Defined. + +End PfiberDeloop. + +(** ** The first round trip + + The short exact sequence extracted from the classifying map of [E] is + [E] itself. *) + +Section ClassifyingRoundTrip. + Context `{Univalence} {B A : AbGroup@{u}} (E : AbSES B A). + + (** The classifying map equals the connecting map after the loop + identification, as a square. *) + Local Definition rt1_square + : pequiv_pmap_idmap o* abses_classifying_map E + ==* connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3) + o* pequiv_loops_em_em B 2 + := pmap_postcompose_idmap _. + + (** The fiber of the connecting map's defining presentation. *) + Local Definition rt1_pfiber_delta + : pfiber (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)) + <~>* pfiber (pfib (em_fmap (inclusion E) 3)). + Proof. + refine (pequiv_pfiber + ((connect_fiberseq (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)).2) + pequiv_pmap_idmap _). + exact (pmap_postcompose_idmap _). + Defined. + + (** Its defining square. *) + Local Definition rt1_pfiber_delta_square + : (connect_fiberseq (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)).2 + o* pfib (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)) + ==* pfib (pfib (em_fmap (inclusion E) 3)) o* rt1_pfiber_delta. + Proof. + refine (square_pequiv_pfiber + ((connect_fiberseq (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)).2) + pequiv_pmap_idmap _). + Defined. + + (** The fiber of the classifying map is [loops K(E,3)]. *) + Local Definition pequiv_pfiber_classifying + : pfiber (abses_classifying_map E) <~>* loops K(E, 3). + Proof. + snapply Build_pEquiv. + 1: exact (loops_inv _ + o* (pfiber2_loops (em_fmap (inclusion E) 3) + o* (rt1_pfiber_delta + o* pequiv_pfiber (pequiv_loops_em_em B 2) pequiv_pmap_idmap + rt1_square))). + exact _. + Defined. + + (** Through this identification, the fiber inclusion of the classifying + map is [loops] of the projection. *) + Local Definition rt1_pfib_square + : pequiv_loops_em_em B 2 o* pfib (abses_classifying_map E) + ==* fmap loops (em_fmap (projection E) 3) + o* pequiv_pfiber_classifying. + Proof. + assert (X : pfib (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)) + ==* fmap loops (em_fmap (projection E) 3) + o* (loops_inv _ + o* (pfiber2_loops (em_fmap (inclusion E) 3) + o* rt1_pfiber_delta))). + { refine ((pmap_postcompose_idmap _)^* @* _). + refine (pmap_prewhisker _ + (peisretr ((pfiber2_loops (em_fmap (projection E) 3)) + o*E (pequiv_pfiber _ _ + (square_pfib_pequiv_cxfib + (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)))))^* @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ rt1_pfiber_delta_square @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ (pfiber2_loops_pfib2 _ _) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + napply pmap_postwhisker. + exact (pmap_compose_assoc _ _ _). } + refine (square_pequiv_pfiber _ _ rt1_square @* _). + refine (pmap_prewhisker _ X @* _). + refine (pmap_compose_assoc _ _ _ @* _). + napply pmap_postwhisker. + refine (pmap_compose_assoc _ _ _ @* _). + napply pmap_postwhisker. + exact (pmap_compose_assoc _ _ _). + Defined. + + (** Loop inversion is an involution. *) + Local Definition loops_inv_inv (X : pType) + : loops_inv X o* loops_inv X ==* pmap_idmap. + Proof. + snapply Build_pHomotopy. + - intro p; exact (inv_V p). + - reflexivity. + Defined. + + (** Loop inversion is natural. *) + Local Definition loops_inv_natural {X Y : pType} (f : X ->* Y) + : fmap loops f o* loops_inv X ==* loops_inv Y o* fmap loops f. + Proof. + pointed_reduce_pmap f. + snapply Build_pHomotopy. + - intro p. + exact (whiskerL 1 (whiskerR (ap_V f p) 1) + @ (concat_1p _ @ concat_p1 _) + @ (inverse2 (concat_1p _ @ concat_p1 _))^). + - reflexivity. + Defined. + + (** Through [pequiv_pfiber_classifying], the connecting map of the + classifying map's fiber sequence is [loops] of the inclusion. *) + Local Definition rt1_conn_square + : pequiv_pfiber_classifying + o* connecting_map (pfib (abses_classifying_map E)) + (abses_classifying_map E) + ==* fmap loops (em_fmap (inclusion E) 3). + Proof. + assert (N1 : pequiv_pfiber (pequiv_loops_em_em B 2) pequiv_pmap_idmap + rt1_square + o* connecting_map (pfib (abses_classifying_map E)) + (abses_classifying_map E) + ==* connecting_map + (pfib (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3))) + (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3))). + { refine (connecting_map_natural _ _ rt1_square @* _). + refine (pmap_postwhisker _ (fmap_id loops _) @* _). + apply pmap_precompose_idmap. } + assert (N2 : rt1_pfiber_delta + o* connecting_map + (pfib (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3))) + (connecting_map (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3)) + ==* connecting_map + (pfib (pfib (em_fmap (inclusion E) 3))) + (pfib (em_fmap (inclusion E) 3))). + { refine (connecting_map_natural _ _ _ @* _). + refine (pmap_postwhisker _ (fmap_id loops _) @* _). + apply pmap_precompose_idmap. } + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _) @* _). + refine (pmap_postwhisker _ + (pmap_postwhisker _ (pmap_compose_assoc _ _ _)) @* _). + refine (pmap_postwhisker _ (pmap_postwhisker _ + (pmap_postwhisker _ N1)) @* _). + refine (pmap_postwhisker _ (pmap_postwhisker _ N2) @* _). + refine (pmap_postwhisker _ (connecting_map_pfib2 _) @* _). + refine (pmap_postwhisker _ + (loops_inv_natural (em_fmap (inclusion E) 3)) @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ (loops_inv_inv _) @* _). + apply pmap_postcompose_idmap. + Defined. + + (** The middle isomorphism of the round trip. *) + Local Definition rt1_middle + : GroupIsomorphism (abgroup_pi_pfiber 0 (abses_classifying_map E)) E. + Proof. + nrefine (grp_iso_compose (grp_iso_inverse (equiv_g_pi_n_em E 2)) _). + nrefine (grp_iso_compose + (grp_iso_inverse (groupiso_pi_loops 1 K(E, 3))) _). + exact (groupiso_pi_functor 1 pequiv_pfiber_classifying). + Defined. + + (** The inclusion square of the round trip. *) + Local Definition rt1_incl_square (a : A) + : rt1_middle (abses_pfiber_incl 0 (abses_classifying_map E) a) + = inclusion E a. + Proof. + apply (equiv_inj (equiv_g_pi_n_em E 2)). + refine (grp_iso_retr (equiv_g_pi_n_em E 2) _ @ _). + apply (equiv_inj (groupiso_pi_loops 1 K(E, 3))). + refine (grp_iso_retr (groupiso_pi_loops 1 K(E, 3)) _ @ _). + assert (CORE : fmap (Pi 2) (pequiv_pfiber_classifying : _ ->* _) + (fmap (Pi 2) + (connecting_map (pfib (abses_classifying_map E)) + (abses_classifying_map E)) + (groupiso_pi_loops 1 K(A, 3) + (equiv_g_pi_n_em A 2 a))) + = groupiso_pi_loops 1 K(E, 3) + (equiv_g_pi_n_em E 2 (inclusion E a))). + { refine ((fmap_comp (Pi 2) + (connecting_map (pfib (abses_classifying_map E)) + (abses_classifying_map E)) + (pequiv_pfiber_classifying : _ ->* _) + (groupiso_pi_loops 1 K(A, 3) + (equiv_g_pi_n_em A 2 a)))^ @ _). + refine (fmap2 (Pi 2) rt1_conn_square _ @ _). + refine ((fmap_pi_loops 2 (em_fmap (inclusion E) 3) + (equiv_g_pi_n_em A 2 a))^ @ _). + exact (ap (pi_loops 2 K(E, 3)) (pi_em_fmap (inclusion E) 2 a)). } + exact CORE. + Defined. + + (** The projection square of the round trip. *) + Local Definition rt1_proj_square (x : Pi 2 (pfiber (abses_classifying_map E))) + : abses_pfiber_proj 0 (abses_classifying_map E) x + = projection E (rt1_middle x). + Proof. + apply (equiv_inj (equiv_g_pi_n_em B 1)). + refine (grp_iso_retr (equiv_g_pi_n_em B 1) _ @ _). + apply (equiv_inj (groupiso_pi_functor 1 (pequiv_loops_em_em B 2))). + (* The left side, through the pointed square. *) + refine ((fmap_comp (Pi 2) (pfib (abses_classifying_map E)) + (pequiv_loops_em_em B 2 : _ ->* _) x)^ @ _). + refine (fmap2 (Pi 2) rt1_pfib_square x @ _). + refine (fmap_comp (Pi 2) (pequiv_pfiber_classifying : _ ->* _) + (fmap loops (em_fmap (projection E) 3)) x @ _). + (* The right side, through naturality of [pi_loops] and [pi_em_fmap]. *) + refine (ap (fmap (pPi 2) (fmap loops (em_fmap (projection E) 3))) + (grp_iso_retr (groupiso_pi_loops 1 K(E, 3)) + (fmap (Pi 2) (pequiv_pfiber_classifying : _ ->* _) x))^ @ _). + refine ((fmap_pi_loops 2 (em_fmap (projection E) 3) _)^ @ _). + refine (ap (groupiso_pi_loops 1 K(B, 3)) _ @ _). + { refine (ap (fmap (Pi 3) (em_fmap (projection E) 3)) + (grp_iso_retr (equiv_g_pi_n_em E 2) _)^ @ _). + exact (pi_em_fmap (projection E) 2 (rt1_middle x)). } + exact (grp_iso_retr (groupiso_pi_loops 1 K(B, 3)) _). + Defined. + + (** The first round trip: the short exact sequence extracted from the + classifying map of [E] is [E]. *) + Definition abses_pfiber_classifying + : abses_pfiber 0 (abses_classifying_map E) = E + := path_abses (E := abses_pfiber 0 (abses_classifying_map E)) (F := E) + rt1_middle rt1_incl_square rt1_proj_square. + +End ClassifyingRoundTrip. + +(** ** The classification theorem + + [abses_classifying_map] is an equivalence, with inverse [abses_pfiber]. *) + +Section Classification. + Context `{Univalence} {B A : AbGroup@{u}}. + + (** A section of the classifying map. *) + Local Definition abses_classifying_section (f : K(B, 2) ->* K(A, 3)) + : abses_classifying_map + (abses_pfiber 1 ((equiv_deloop_em_pmap B A 0)^-1 + (f o* pequiv_neg_em^-1*))) + = f. + Proof. + apply path_pforall. + refine (abses_classifying_pfiber_deloop _ @* _). + refine (pmap_prewhisker pequiv_neg_em + (phomotopy_path (eisretr (equiv_deloop_em_pmap B A 0) _)) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (peissect pequiv_neg_em) @* _). + apply pmap_precompose_idmap. + Defined. + + (** The second round trip. *) + Local Definition abses_classifying_map_pfiber (f : K(B, 2) ->* K(A, 3)) + : abses_classifying_map (abses_pfiber 0 f) = f. + Proof. + transitivity (abses_classifying_map + (abses_pfiber 1 ((equiv_deloop_em_pmap B A 0)^-1 + (f o* pequiv_neg_em^-1*)))). + - apply (ap abses_classifying_map). + refine ((ap (abses_pfiber 0) (abses_classifying_section f))^ @ _). + exact (abses_pfiber_classifying _). + - exact (abses_classifying_section f). + Defined. + + (** Short exact sequences [A -> E -> B] are classified by pointed maps + [K(B,2) ->* K(A,3)]. *) + Definition equiv_abses_classifying_map + : AbSES B A <~> (K(B, 2) ->* K(A, 3)) + := equiv_adjointify abses_classifying_map (abses_pfiber 0) + abses_classifying_map_pfiber abses_pfiber_classifying. + + (** Consequently [Ext B A] is the set of path components of the + classifying mapping type. *) + Definition equiv_ext_classifying + : Ext B A <~> Tr 0 (K(B, 2) ->* K(A, 3)) + := Trunc_functor_equiv 0 equiv_abses_classifying_map. + + (** [AbSES B A] is essentially small, and so is [Ext B A] (Remark 2.2.5). *) + Definition issmall_abses : IsSmall@{u _} (AbSES B A) + := issmall_equiv_issmall (equiv_abses_classifying_map)^-1%equiv + (issmall_in _). + + Definition issmall_ext : IsSmall@{u _} (Ext B A) + := issmall_equiv_issmall (equiv_ext_classifying)^-1%equiv + (issmall_in _). + +End Classification. + +(** ** Naturality of the classifying map + + A morphism of short exact sequences induces a commuting square relating + the two classifying maps. *) + +(** Keep the [cxfib] equivalence witnesses opaque so their inverses stay + inert. *) +Opaque isequiv_cxfib_em isequiv_cxfib. + +Section Naturality. + Context `{Univalence} {B A Y X : AbGroup@{u}} + {E : AbSES B A} {F : AbSES Y X} (phi : AbSESMorphism E F). + + (** [K(-,3)] of the projection square of [phi]. *) + Local Definition em_proj_square + : em_fmap (projection F) 3 o* em_fmap (component2 phi) 3 + ==* em_fmap (component3 phi) 3 o* em_fmap (projection E) 3. + Proof. + refine ((em_fmap_compose _ _ 3)^* @* _ @* em_fmap_compose _ _ 3). + refine (phomotopy_path (ap (fun h => em_fmap h 3) _)). + apply equiv_path_grouphomomorphism; intro e. + exact (right_square phi e). + Defined. + + (** [K(-,3)] of the inclusion square of [phi]. *) + Local Definition em_incl_square + : em_fmap (component2 phi) 3 o* em_fmap (inclusion E) 3 + ==* em_fmap (inclusion F) 3 o* em_fmap (component1 phi) 3. + Proof. + refine ((em_fmap_compose _ _ 3)^* @* _ @* em_fmap_compose _ _ 3). + refine (phomotopy_path (ap (fun h => em_fmap h 3) _)). + apply equiv_path_grouphomomorphism; intro a. + exact (left_square phi a)^. + Defined. + + (** The fiber inclusions, as equivalences. *) + Local Definition em_cxfib_E + : K(A, 3) <~>* pfiber (em_fmap (projection E) 3) + := @pequiv_cxfib _ _ _ (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3) (isexact_em_abses E 2). + + Local Definition em_cxfib_F + : K(X, 3) <~>* pfiber (em_fmap (projection F) 3) + := @pequiv_cxfib _ _ _ (em_fmap (inclusion F) 3) + (em_fmap (projection F) 3) (isexact_em_abses F 2). + + (** The fiber-inclusion comparison commutes with the morphism on + fibers. *) + Local Definition em_cxfib_square + : functor_pfiber (em_proj_square^*) o* em_cxfib_E + = em_cxfib_F o* em_fmap (component1 phi) 3. + Proof. + snapply (path_em_pmap_pi_connected 1). + 1: exact (isconnected_equiv' 2 K(X, 3) em_cxfib_F (isconnected_em 2)). + 1: exact _. + intro x. + napply (isinj_embedding _ + (@isembedding_pi_pfib _ _ _ (em_fmap (projection F) 3) 2 + (contr_pi_pfiber_pfib F 2))). + refine (ap (fmap (Pi 3) (pfib (em_fmap (projection F) 3))) + (fmap_comp (Pi 3) (em_cxfib_E : _ ->* _) + (functor_pfiber (em_proj_square^*) : _ ->* _) x) @ _). + refine ((fmap_comp (Pi 3) + (functor_pfiber (em_proj_square^*) : _ ->* _) + (pfib (em_fmap (projection F) 3)) _)^ @ _). + refine ((fmap2 (Pi 3) (square_functor_pfiber (em_proj_square^*)) _)^ @ _). + refine (fmap_comp (Pi 3) (pfib (em_fmap (projection E) 3)) + (em_fmap (component2 phi) 3) _ @ _). + refine (ap (fmap (Pi 3) (em_fmap (component2 phi) 3)) + ((fmap_comp (Pi 3) (em_cxfib_E : _ ->* _) + (pfib (em_fmap (projection E) 3)) x)^ + @ fmap2 (Pi 3) (pfib_cxfib _) x) @ _). + refine ((fmap_comp (Pi 3) (em_fmap (inclusion E) 3) + (em_fmap (component2 phi) 3) x)^ @ _). + refine (fmap2 (Pi 3) em_incl_square x @ _). + refine (fmap_comp (Pi 3) (em_fmap (component1 phi) 3) + (em_fmap (inclusion F) 3) x @ _). + refine ((fmap2 (Pi 3) (pfib_cxfib _) + (fmap (Pi 3) (em_fmap (component1 phi) 3) x))^ @ _). + refine (fmap_comp (Pi 3) (em_cxfib_F : _ ->* _) + (pfib (em_fmap (projection F) 3)) _ @ _). + exact (ap (fmap (Pi 3) (pfib (em_fmap (projection F) 3))) + (fmap_comp (Pi 3) (em_fmap (component1 phi) 3) + (em_cxfib_F : _ ->* _) x))^. + Qed. + + (** Hence the connecting maps of the two sequences are related by the + morphism, through the loop identification of the bases. *) + Local Definition cm_natural + : em_fmap (component1 phi) 3 + o* connecting_map (em_fmap (inclusion E) 3) (em_fmap (projection E) 3) + ==* connecting_map (em_fmap (inclusion F) 3) (em_fmap (projection F) 3) + o* fmap loops (em_fmap (component3 phi) 3). + Proof. + refine (pmap_prewhisker _ + (moveR_pequiv_Vf em_cxfib_F (em_fmap (component1 phi) 3) + (functor_pfiber (em_proj_square^*) o* em_cxfib_E) + (phomotopy_path em_cxfib_square))^* @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _) @* _). + refine (pmap_postwhisker _ (pmap_postwhisker _ + (connecting_map_cxfib (em_fmap (inclusion E) 3) + (em_fmap (projection E) 3))) @* _). + refine (pmap_postwhisker _ + (connecting_map_natural_functor (em_proj_square^*)) @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + napply pmap_prewhisker. + exact (moveR_pequiv_Vf em_cxfib_F + (connecting_map (em_fmap (inclusion F) 3) (em_fmap (projection F) 3)) + (connecting_map (pfib (em_fmap (projection F) 3)) + (em_fmap (projection F) 3)) + (connecting_map_cxfib (em_fmap (inclusion F) 3) + (em_fmap (projection F) 3))^*). + Defined. + + (** A morphism of short exact sequences induces a commuting square of + classifying maps. *) + Definition abses_classifying_map_natural + : em_fmap (component1 phi) 3 o* abses_classifying_map E + ==* abses_classifying_map F o* em_fmap (component3 phi) 2. + Proof. + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ cm_natural @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (em_fmap_loops_natural (component3 phi) 2) + @* _). + exact (pmap_compose_assoc _ _ _)^*. + Defined. + +End Naturality. + +Transparent isequiv_cxfib_em isequiv_cxfib. + diff --git a/theories/Homotopy/ClassifyingSpace.v b/theories/Homotopy/ClassifyingSpace.v index 3c015b8f89f..b1e89595d5a 100644 --- a/theories/Homotopy/ClassifyingSpace.v +++ b/theories/Homotopy/ClassifyingSpace.v @@ -29,6 +29,8 @@ Module Export ClassifyingSpace. Section ClassifyingSpace. + Local Set Polymorphic Inductive Cumulativity. + Private Inductive ClassifyingSpace (G : Group) := | bbase : ClassifyingSpace G. @@ -404,6 +406,16 @@ Section HSpace_bg. End HSpace_bg. +(** The classifying space of a contractible group is contractible. *) +Instance contr_pclassifyingspace `{Univalence} (G : Group) `{Contr G} + : Contr (B G). +Proof. + rapply (contr_equiv' pUnit (Build_Equiv _ _ pconst _)). + (* The map from [pUnit] is an equivalence, since it is one on loops, as both have contractible loop spaces. *) + pose proof (contr_equiv' G equiv_g_loops_bg). + rapply isequiv_is0connected_isequiv_loops. +Defined. + (** Functoriality of B(-) *) Instance is0functor_pclassifyingspace : Is0Functor B. @@ -442,6 +454,26 @@ Proof. apply pbloop_natural. Defined. +(** [fmap B] of a surjective group homomorphism is a 0-connected map. *) +Instance isconnmap_fmap_pclassifyingspace `{Univalence} {G K : Group} + (f : GroupHomomorphism G K) `{!IsSurjection f} + : IsConnMap 0 (fmap B f). +Proof. + (* By [isconnmap_isconnmap_ap_surj] it suffices to show that [fmap B f] and its [ap]s are surjective; both follow from surjectivity of [f]. *) + snapply isconnmap_isconnmap_ap_surj. + - rapply (isconnmap_isconnected (-1)). + - rapply (conn_point_elim (-1) (A:=B G)). + rapply (conn_point_elim (-1) (A:=B G)). + srapply (equiv_ind equiv_g_loops_bg). + intro h. + rapply contr_inhabited_hprop. + pose proof (m := center (Tr (-1) (hfiber f h))). + strip_truncations. + destruct m as [g p]. + exact (tr (bloop g; + ClassifyingSpace_rec_beta_bloop _ _ _ _ g @ ap bloop p)). +Defined. + Instance is1functor_pclassifyingspace : Is1Functor B. Proof. apply Build_Is1Functor. diff --git a/theories/Homotopy/EMSpace.v b/theories/Homotopy/EMSpace.v index 822edca9784..867f3269d87 100644 --- a/theories/Homotopy/EMSpace.v +++ b/theories/Homotopy/EMSpace.v @@ -1,10 +1,11 @@ From HoTT Require Import Basics Types. -From HoTT.WildCat Require Import Core Universe Equiv. +From HoTT.WildCat Require Import Core Universe Equiv PointedCat. Require Import Pointed. Require Import Cubical.DPath. Require Import Algebra.AbGroups.AbelianGroup. Require Import Homotopy.Suspension. Require Import Homotopy.ClassifyingSpace. +Import ClassifyingSpaceNotation. Require Import Homotopy.HSpace.Coherent. Require Import Homotopy.HomotopyGroup. Require Import Homotopy.Hopf. @@ -110,7 +111,7 @@ Section EilenbergMacLane. exact iscohhspace_loops. Defined. - (** If [G] and [G'] are isomorphic, then [K(G,n)] and [K(G',n)] are equivalent. TODO: We should show that [K(-,n)] is a functor, which implies this. *) + (** If [G] and [G'] are isomorphic, then [K(G,n)] and [K(G',n)] are equivalent. This also follows from [em_fmap] below. *) Definition pequiv_em_group_iso {G G' : Group} (n : nat) (e : G $<~> G') : K(G, n) <~>* K(G', n). @@ -118,6 +119,248 @@ Section EilenbergMacLane. by destruct (equiv_path_group e). Defined. + (** The action of [K(-,n)] on group homomorphisms, giving the functoriality of [K(-,n)]. Note that [fmap B] and the WildCat functoriality of [psusp] and [pTr] constrain the two groups to a single universe. *) + Definition em_fmap {G G' : AbGroup} (f : GroupHomomorphism G G') (n : nat) + : K(G, n) ->* K(G', n). + Proof. + induction n as [|n IHn]. + - exact (Build_pMap f (grp_homo_unit f)). + - destruct n as [|m]. + + exact (fmap B f). + + exact (fmap (pTr m.+2) (fmap psusp IHn)). + Defined. + + (** [em_fmap] preserves the identity. *) + Definition em_fmap_idmap {G : AbGroup} (n : nat) + : em_fmap (G:=G) grp_homo_id n ==* pmap_idmap. + Proof. + induction n as [|[|m] IH]. + - snapply Build_pHomotopy. + + reflexivity. + + rapply path_ishprop. + - exact (fmap_id B G). + - refine (_ @* fmap_id (pTr m.+2) _). + tapply (fmap2 (pTr m.+2)). + refine (_ @* fmap_id psusp _). + tapply (fmap2 psusp). + exact (pointed_htpy IH). + Defined. + + (** [em_fmap] preserves composition. *) + Definition em_fmap_compose {G G' G'' : AbGroup} + (f : GroupHomomorphism G G') (g : GroupHomomorphism G' G'') (n : nat) + : em_fmap (grp_homo_compose g f) n ==* em_fmap g n o* em_fmap f n. + Proof. + induction n as [|[|m] IH]. + - snapply Build_pHomotopy. + + reflexivity. + + rapply path_ishprop. + - exact (fmap_comp B f g). + - refine (_ @* fmap_comp (pTr m.+2) _ _). + tapply (fmap2 (pTr m.+2)). + refine (_ @* fmap_comp psusp _ _). + tapply (fmap2 psusp). + exact (pointed_htpy IH). + Defined. + + (** [K(-,n)] is a functor from abelian groups to pointed types, with [em_fmap] as its action on morphisms. *) + #[export] Instance is0functor_em (n : nat) + : Is0Functor (fun G : AbGroup => K(G, n)). + Proof. + napply Build_Is0Functor. + intros G G' f; exact (em_fmap f n). + Defined. + + #[export] Instance is1functor_em (n : nat) + : Is1Functor (fun G : AbGroup => K(G, n)). + Proof. + napply Build_Is1Functor. + - intros G G' f g p. + napply phomotopy_path. + napply (ap (fun h => em_fmap h n)). + apply equiv_path_grouphomomorphism. + exact p. + - intros G; exact (em_fmap_idmap n). + - intros G G' G'' f g; exact (em_fmap_compose f g n). + Defined. + + (** At positive levels, [pequiv_loops_em_em] is the canonical comparison map: the loop-suspension unit followed by [loops] of the truncation map. This presentation makes its naturality transparent, without reference to the Hopf-construction input used to show that it is an equivalence. *) + Definition loops_em_em_ptr_unit (G : AbGroup) (n : nat) + : pequiv_loops_em_em G n.+1 + ==* fmap loops ptr o* loop_susp_unit K(G, n.+1). + Proof. + destruct n as [|n]. + all: refine (compose_cate_fun (A:=pType) _ _ @* _). + all: refine (pmap_postwhisker _ (compose_cate_fun (A:=pType) _ _) @* _). + 1: refine (pmap_postwhisker _ (pto_O_natural (Tr _) _) @* _). + 2: refine (pmap_postwhisker _ (ptr_natural _ _) @* _). + all: refine ((pmap_compose_assoc _ _ _)^* @* _). + all: exact (pmap_prewhisker _ (ptr_loops_commutes _ _)). + Defined. + + (** [em_fmap] commutes with the loop-space identifications, so it is a map of spectra. *) + Definition em_fmap_loops_natural {G G' : AbGroup} + (f : GroupHomomorphism G G') (n : nat) + : fmap loops (em_fmap f n.+1) o* pequiv_loops_em_em G n + ==* pequiv_loops_em_em G' n o* em_fmap f n. + Proof. + destruct n as [|n]. + - exact (pbloop_natural G G' f). + - refine (pmap_postwhisker _ (loops_em_em_ptr_unit G n) @* _). + refine (_ @* pmap_prewhisker _ (loops_em_em_ptr_unit G' n)^*). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ (fmap_comp loops _ _)^* @* _). + refine (pmap_prewhisker _ (fmap2 loops (ptr_natural _ _)) @* _). + refine (pmap_prewhisker _ (fmap_comp loops _ _) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (loop_susp_unit_natural _)^* @* _). + exact (pmap_compose_assoc _ _ _)^*. + Defined. + + (** [equiv_g_pi_n_em] at level [n.+1] unfolds to the level-[n] map conjugated by [groupiso_pi_loops] and [pequiv_loops_em_em]. *) + Local Definition equiv_g_pi_n_em_succ (G : AbGroup) (n : nat) (x : G) + : equiv_g_pi_n_em G n.+1 x + = grp_iso_inverse (groupiso_pi_loops _ _) + (groupiso_pi_functor _ (pequiv_loops_em_em G n.+1) + (equiv_g_pi_n_em G n x)) + := idpath. + + (** The action of [em_fmap f n.+1] on [Pi n.+1] agrees with [f] under the identifications [equiv_g_pi_n_em]. *) + Definition pi_em_fmap {G G' : AbGroup} + (f : GroupHomomorphism G G') (n : nat) + : fmap (Pi n.+1) (em_fmap f n.+1) o equiv_g_pi_n_em G n + == equiv_g_pi_n_em G' n o f. + Proof. + induction n as [|n IHn]; intro g. + - exact (ap tr (bloop_natural G G' f g)). + - lhs napply (ap _ (equiv_g_pi_n_em_succ G n g)). + rhs napply (equiv_g_pi_n_em_succ G' n (f g)). + apply (equiv_inj (groupiso_pi_loops n _)). + rhs napply (eisretr (groupiso_pi_loops n _) _). + lhs napply (fmap_pi_loops n.+1 (em_fmap f n.+2) _). + lhs napply (ap _ (eisretr (groupiso_pi_loops n _) _)). + lhs_V exact (fmap_comp (pPi n.+1) + (pequiv_loops_em_em G n.+1 : _ ->* _) + (fmap loops (em_fmap f n.+2)) (equiv_g_pi_n_em G n g)). + lhs exact (fmap2 (pPi n.+1) (em_fmap_loops_natural f n.+1) + (equiv_g_pi_n_em G n g)). + lhs exact (fmap_comp (pPi n.+1) + (em_fmap f n.+1) (pequiv_loops_em_em G' n.+1 : _ ->* _) + (equiv_g_pi_n_em G n g)). + exact (ap _ (IHn g)). + Defined. + + (** Eilenberg-Mac Lane spaces of a contractible group are contractible. *) + #[export] Instance contr_em_contr {G : AbGroup} `{Contr G} (n : nat) + : Contr K(G, n). + Proof. + induction n as [|[|n] IHn]. + - exact _. + - exact _. + - apply (Build_Contr _ (tr (center _))). + srapply Trunc_ind; intro a. + exact (ap tr (contr a)). + Defined. + + (** [K(-,n)] is a pointed functor. *) + #[export] Instance ispointedfunctor_em (n : nat) + : IsPointedFunctor (fun G : AbGroup => K(G, n)). + Proof. + rapply Build_IsPointedFunctor'. + snapply Build_pEquiv. + 1: exact pconst. + rapply isequiv_contr_contr. + Defined. + + (** [em_fmap] sends the constant homomorphism to the constant map. *) + Definition em_fmap_const {G G' : AbGroup} (n : nat) + : em_fmap (G:=G) (G':=G') grp_homo_const n ==* pconst + := fmap_zero_morphism (fun G : AbGroup => K(G, n)). + + (** [em_fmap f n.+1] of a surjective homomorphism is an [n]-connected map. Both surjectivity of the map and of its [ap]s reduce to the previous level through the loop-space identifications. *) + #[export] Instance isconnmap_em_fmap {G G' : AbGroup} + (f : GroupHomomorphism G G') `{!IsSurjection f} (n : nat) + : IsConnMap n (em_fmap f n.+1). + Proof. + induction n as [|n IHn]. + - exact (isconnmap_fmap_pclassifyingspace f). + - snapply isconnmap_isconnmap_ap_surj. + + rapply (isconnmap_isconnected (-1)). + + assert (c : IsConnMap n (fmap loops (em_fmap f n.+2))). + { napply (conn_map_homotopic _ + ((pequiv_loops_em_em G' n.+1 o* em_fmap f n.+1) + o* (pequiv_loops_em_em G n.+1)^-1*) _ + (fun p => + (moveR_pequiv_fV _ _ _ (em_fmap_loops_natural f n.+1))^* p)). + exact _. } + snapply (conn_point_elim (-1) (A:=K(G, n.+2))). + 1,2: exact _. + snapply (conn_point_elim (-1) (A:=K(G, n.+2))). + 1,2: exact _. + intro q. + pose (e2 := equiv_concat_l (point_eq (em_fmap f n.+2))^ _ + oE equiv_concat_r (point_eq (em_fmap f n.+2)) _). + exact (isconnected_equiv' n _ + (equiv_functor_sigma_id (fun p => equiv_ap e2 _ _))^-1%equiv + (c _)). + Defined. + + (** [em_fmap] is an equivalence from group homomorphisms to pointed maps, extending [isequiv_fmap_pclassifyingspace] to all levels. In particular, pointed maps between Eilenberg-Mac Lane spaces of the same level are determined by their effect on homotopy groups. *) + #[export] Instance isequiv_em_fmap (G G' : AbGroup) (n : nat) + : IsEquiv (fun f : GroupHomomorphism G G' => em_fmap f n.+1). + Proof. + induction n as [|n IHn]. + - exact (isequiv_fmap_pclassifyingspace G G'). + - (* The ladder [pequiv_ptr_rec], [loop_susp_adjoint], postcomposition with [pequiv_loops_em_em], and the inductive hypothesis. *) + pose (L := ((Build_Equiv _ _ _ IHn)^-1%equiv) + oE (pequiv_pequiv_postcompose (pequiv_loops_em_em G' n.+1)^-1* + : (K(G, n.+1) ->** loops K(G', n.+2)) <~> _) + oE (loop_susp_adjoint K(G, n.+1) K(G', n.+2) + : (psusp K(G, n.+1) ->** _) <~> _) + oE (pequiv_ptr_rec + : (K(G, n.+2) ->** K(G', n.+2)) <~> _)). + napply (isequiv_homotopic' L^-1%equiv). + intro f. + apply moveR_equiv_V; symmetry. + apply moveR_equiv_V. + apply path_pforall. + lhs' refine (pmap_postwhisker _ + (pmap_prewhisker _ (fmap2 loops (ptr_natural _ _)))). + lhs' refine (pmap_postwhisker _ + (pmap_prewhisker _ (fmap_comp loops _ _))). + lhs' refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _)). + lhs' refine (pmap_postwhisker _ + (pmap_postwhisker _ (loop_susp_unit_natural _)^*)). + lhs' refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _)^*). + lhs' refine (pmap_postwhisker _ + (pmap_prewhisker _ (loops_em_em_ptr_unit G' n)^*)). + lhs_V' refine (pmap_compose_assoc _ _ _). + lhs' refine (pmap_prewhisker _ (peissect _)). + apply pmap_postcompose_idmap. + Defined. + + (** Pointed maps between Eilenberg-Mac Lane spaces of the same level which agree on homotopy groups are equal. *) + Definition path_em_pmap_pi {G G' : AbGroup} (n : nat) + (phi psi : K(G, n.+1) ->* K(G', n.+1)) + (h : fmap (Pi n.+1) phi == fmap (Pi n.+1) psi) + : phi = psi. + Proof. + pose (e := Build_Equiv _ _ _ (isequiv_em_fmap G G' n)). + refine ((eisretr e phi)^ @ ap e _ @ eisretr e psi). + apply equiv_path_grouphomomorphism; intro g. + apply (equiv_inj (equiv_g_pi_n_em G' n)). + refine ((pi_em_fmap _ n g)^ @ _ @ pi_em_fmap _ n g). + refine (ap (fun (m : _ ->* _) => fmap (Pi n.+1) m _) (eisretr e phi) @ _). + refine (_ @ ap (fun (m : _ ->* _) => fmap (Pi n.+1) m _) (eisretr e psi)^). + apply h. + Defined. + + (** [em_fmap] of a group isomorphism is a pointed equivalence. *) + Definition pequiv_em_fmap {G G' : AbGroup} + (e : GroupIsomorphism G G') (n : nat) + : K(G, n) <~>* K(G', n) + := emap (fun G : AbGroup => K(G, n)) (Build_CatEquiv e). + (** Every pointed (n-1)-connected n-type is an Eilenberg-Mac Lane space. *) Definition pequiv_em_connected_truncated (X : pType) (n : nat) `{IsConnected n X} `{IsTrunc n.+1 X} @@ -146,3 +389,136 @@ Section EilenbergMacLane. Defined. End EilenbergMacLane. + +(** ** Delooping Eilenberg-Mac Lane mapping types *) + +(** The [k]-fold loop space of a [k]-truncated type is a set. *) +Definition istrunc_iterated_loops_O `{Funext} (k : nat) (X : pType) `{H0 : IsTrunc k X} + : IsTrunc 0 (iterated_loops k X). +Proof. + revert X H0; induction k as [|k IH]; intros X H0. + - exact H0. + - rewrite (unfold_iterated_loops k X). + rapply IH. +Defined. + +Section Deloop. + Context `{Univalence} (B A : AbGroup@{u}) (n : nat). + + (** [Pi n.+4 (psusp K(B,n.+2))] is trivial. *) + Local Instance contr_pi_psusp_em : Contr (Pi n.+4 (psusp K(B, n.+2))). + Proof. + nrefine (contr_equiv' (Pi n.+3 (loops (psusp K(B, n.+2)))) _). + 1: exact (grp_iso_inverse (groupiso_pi_loops n.+2 (psusp K(B, n.+2)))). + assert (C : IsConnMap n.+2 (loop_susp_unit K(B, n.+2))). + { napply (isconnmap_pred_add n.-2). + rewrite 2 trunc_index_add_succ. + exact (conn_map_loop_susp_unit n K(B, n.+2)). } + pose proof (contr_pi_succ_istrunc n.+1 K(B, n.+2)). + pose proof (S := issurj_pi_connmap n.+2 (loop_susp_unit K(B, n.+2))). + pose (fu := fmap (pPi n.+3) (loop_susp_unit K(B, n.+2)) + : Pi n.+3 K(B, n.+2) -> Pi n.+3 (loops (psusp K(B, n.+2)))). + apply (Build_Contr _ (fu (center _))). + intro y. + pose proof (m := @center _ (S y)). + strip_truncations. + destruct m as [x p]. + refine (_ @ p). + exact (ap _ (path_contr _ x)). + Defined. + + (** [pTr n.+4 (psusp K(B,n.+2))] is [n.+3]-truncated. *) + Local Instance istrunc_ptr_psusp_em + : IsTrunc n.+3 (pTr n.+4 (psusp K(B, n.+2))). + Proof. + apply (equiv_istrunc_contr_iterated_loops n.+4 _)^-1. + pose proof (istrunc_iterated_loops_O n.+4 (pTr n.+4 (psusp K(B, n.+2)))). + pose proof (@isconnected_susp n.+1 K(B, n.+2) (isconnected_em n.+1)). + pose proof (is0connected_isconnected n (psusp K(B, n.+2))). + pose proof (isconnected_trunc 0 n.+4 (X := psusp K(B, n.+2))). + snapply (conn_point_elim (-1)). + 1,2: exact _. + nrefine (contr_equiv' (Pi n.+4 (pTr n.+4 (psusp K(B, n.+2)))) _). + 1: exact (equiv_tr 0 _)^-1%equiv. + nrefine (contr_equiv' (Pi n.+4 (psusp K(B, n.+2))) _). + 1: exact (grp_iso_pi_Tr n.+3 (psusp K(B, n.+2))). + exact _. + Defined. + + (** [K(B,n.+3)] is the [n.+3]-truncation of [pTr n.+4 (psusp K(B,n.+2))]. *) + Local Definition pequiv_ptr_ptr_psusp_em + : K(B, n.+3) <~>* pTr n.+3 (pTr n.+4 (psusp K(B, n.+2))). + Proof. + snapply Build_pEquiv. + 1: exact (fmap (pTr n.+3) ptr). + napply O_inverts_conn_map. + exact (isconnmap_pred' n.+4 _). + Defined. + + (** The canonical equivalence between the [n.+4]- and [n.+3]-truncations. *) + Local Definition pequiv_ptr_psusp_em + : pTr n.+4 (psusp K(B, n.+2)) <~>* K(B, n.+3) + := pequiv_ptr_ptr_psusp_em^-1* o*E pequiv_ptr (n:=n.+3). + + (** [pequiv_ptr_psusp_em] commutes with the truncation unit [ptr]. *) + Local Definition tau_ptr_psusp_em + : pequiv_ptr_psusp_em o* ptr ==* ptr. + Proof. + refine (pmap_prewhisker ptr (compose_cate_fun (A:=pType) _ _) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (ptr_natural n.+3 ptr)^* @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker ptr (peissect pequiv_ptr_ptr_psusp_em) @* _). + apply pmap_postcompose_idmap. + Defined. + + (** Pointed maps [K(B,n.+3) ->* K(A,n.+4)] are equivalent to pointed maps [K(B,n.+2) ->* K(A,n.+3)]. *) + Definition equiv_deloop_em_pmap + : (K(B, n.+3) ->* K(A, n.+4)) <~> (K(B, n.+2) ->* K(A, n.+3)) + := pequiv_pequiv_postcompose (pequiv_loops_em_em A n.+3)^-1* + oE loop_susp_adjoint K(B, n.+2) K(A, n.+4) + oE pequiv_ptr_rec + oE pequiv_pequiv_precompose pequiv_ptr_psusp_em. + + (** [equiv_deloop_em_pmap] as looping conjugated by the loop identifications. *) + Definition equiv_deloop_em_pmap_unfold (psi : K(B, n.+3) ->* K(A, n.+4)) + : equiv_deloop_em_pmap psi + ==* (pequiv_loops_em_em A n.+3)^-1* + o* (fmap loops psi o* pequiv_loops_em_em B n.+2). + Proof. + transitivity ((pequiv_loops_em_em A n.+3)^-1* + o* (fmap loops (psi o* pequiv_ptr_psusp_em o* ptr) + o* loop_susp_unit K(B, n.+2))). + 1: reflexivity. + symmetry. + napply pmap_postwhisker. + refine (pmap_postwhisker _ (loops_em_em_ptr_unit B n.+1) @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ (fmap_comp loops _ _)^* @* _). + napply pmap_prewhisker. + tapply (fmap2 loops). + exact (pmap_compose_assoc psi _ ptr + @* pmap_postwhisker psi tau_ptr_psusp_em)^*. + Defined. + +End Deloop. + +(** Pointed maps from an Eilenberg-Mac Lane space to a connected truncated type of the same level which agree on homotopy groups are equal. *) +Definition path_em_pmap_pi_connected `{Univalence} {G : AbGroup@{u}} + (n : nat) {Y : pType} `{IsConnected n.+1 Y} `{IsTrunc n.+2 Y} + (phi psi : K(G, n.+2) ->* Y) + (h : fmap (Pi n.+2) phi == fmap (Pi n.+2) psi) + : phi = psi. +Proof. + apply (equiv_inj (pequiv_pequiv_postcompose + (pequiv_em_connected_truncated Y n.+1)^-1*)). + napply (path_em_pmap_pi (G' := Build_AbGroup (Pi n.+2 Y) _)). + intro x. + refine (fmap_comp (Pi n.+2) phi + ((pequiv_em_connected_truncated Y n.+1)^-1* : _ ->* _) x @ _). + refine (ap _ (h x) @ _). + exact (fmap_comp (Pi n.+2) psi + ((pequiv_em_connected_truncated Y n.+1)^-1* : _ ->* _) x)^%path. + Unshelve. + all: exact _. +Defined. diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v index 4cdfb4c6329..70b5a4c5487 100644 --- a/theories/Homotopy/ExactSequence.v +++ b/theories/Homotopy/ExactSequence.v @@ -492,6 +492,164 @@ Proof. - reflexivity. Defined. +(** ** Naturality and rotation of the connecting map *) + +(** The fiber functor of the tautological [cxfib] square is the identity. *) +Definition pequiv_pfiber_cxfib_taut {X Y : pType} (f : X ->* Y) + : pequiv_pfiber pequiv_cxfib pequiv_pmap_idmap + (square_pfib_pequiv_cxfib (pfib f) f) + ==* pmap_idmap. +Proof. + pointed_reduce_pmap f. + snapply Build_pHomotopy. + - intros [[x w] v]. + snapply path_sigma'. + + reflexivity. + + cbn. + exact (concat_p1 _ @ (concat_1p _ @ ap_idmap v)). + - reflexivity. +Defined. + +(** The connecting map of the tautological fiber sequence is natural in arbitrary squares of pointed maps. *) +Definition connecting_map_natural_functor {X Y X' Y' : pType} + {f : X ->* Y} {f' : X' ->* Y'} {h : X' ->* X} {k : Y' ->* Y} + (q : k o* f' ==* f o* h) + : functor_pfiber q o* connecting_map (pfib f') f' + ==* connecting_map (pfib f) f o* fmap loops k. +Proof. + (* The inverse-free square between the double-fiber identifications. *) + assert (S : ((pfiber2_loops f) + o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib (pfib f) f)) + : _ ->* _) + o* functor_pfiber (square_functor_pfiber q) + ==* fmap loops k + o* ((pfiber2_loops f') + o*E (pequiv_pfiber _ _ + (square_pfib_pequiv_cxfib (pfib f') f')) + : _ ->* _)). + { refine (pmap_prewhisker _ (compose_cate_fun (A:=pType) _ _) @* _ + @* pmap_postwhisker _ (compose_cate_fun (A:=pType) _ _)^*). + refine (pmap_prewhisker _ + (pmap_postwhisker _ (pequiv_pfiber_cxfib_taut f) + @* pmap_precompose_idmap _) @* _ + @* pmap_postwhisker _ + (pmap_postwhisker _ (pequiv_pfiber_cxfib_taut f') + @* pmap_precompose_idmap _)^*). + exact (pfiber2_loops_natural_functor q). } + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ + (square_functor_pfiber (square_functor_pfiber q)) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (_ @* (pmap_compose_assoc _ _ _)^*). + napply pmap_postwhisker. + napply moveL_pequiv_Vf. + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ S @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (peisretr _) @* _). + apply pmap_precompose_idmap. +Defined. + +(** The same for an equivalence square. *) +Definition connecting_map_natural {X Y X' Y' : pType} + {f : X ->* Y} {f' : X' ->* Y'} (h : X' <~>* X) (k : Y' <~>* Y) + (q : k o* f' ==* f o* h) + : pequiv_pfiber h k q o* connecting_map (pfib f') f' + ==* connecting_map (pfib f) f o* fmap loops k + := connecting_map_natural_functor q. + +(** Through [cxfib], the connecting map of an exact sequence agrees with the connecting map of the tautological fiber sequence. *) +Definition connecting_map_cxfib {F X Y : pType} + (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} + : pequiv_cxfib o* connecting_map i f ==* connecting_map (pfib f) f. +Proof. + assert (WQV : ((pfiber2_loops f) + o*E (pequiv_pfiber _ _ + (square_pfib_pequiv_cxfib (pfib f) f)) + : _ ->* _) + o* pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f) + ==* ((pfiber2_loops f) + o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)) + : _ ->* _)). + { refine (pmap_prewhisker _ (compose_cate_fun (A:=pType) _ _) @* _ + @* (compose_cate_fun (A:=pType) _ _)^*). + refine (pmap_compose_assoc _ _ _ @* _). + napply pmap_postwhisker. + refine (pmap_prewhisker _ (pequiv_pfiber_cxfib_taut f) @* _). + apply pmap_postcompose_idmap. } + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ + (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)) @* _). + refine (pmap_compose_assoc _ _ _ @* _). + napply pmap_postwhisker. + refine (_ @* pmap_precompose_idmap _). + napply moveL_pequiv_Vf. + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ WQV @* _). + exact (peisretr _). +Defined. + +(** Through [pfiber2_loops], the connecting map of the doubly-iterated tautological fiber sequence is loop inversion followed by [loops] of the map. *) +Definition connecting_map_pfib2 {F X : pType} (i : F ->* X) + : pfiber2_loops i o* connecting_map (pfib (pfib i)) (pfib i) + ==* fmap loops i o* loops_inv F. +Proof. + assert (S : pfiber2_loops i o* pfib (pfib (pfib i)) + ==* (fmap loops i o* loops_inv F) + o* ((pfiber2_loops (pfib i)) + o*E (pequiv_pfiber _ _ + (square_pfib_pequiv_cxfib + (pfib (pfib i)) (pfib i))) + : _ ->* _)). + { refine (pfiber2_fmap_loops i @* _). + refine ((pmap_compose_assoc _ _ _)^* @* _). + napply pmap_postwhisker. + refine (_ @* (compose_cate_fun (A:=pType) _ _)^*). + refine (_ @* (pmap_postwhisker _ (pequiv_pfiber_cxfib_taut (pfib i)) + @* pmap_precompose_idmap _)^*). + reflexivity. } + refine ((pmap_compose_assoc _ _ _)^* @* _). + refine (pmap_prewhisker _ S @* _). + refine (pmap_compose_assoc _ _ _ @* _). + refine (pmap_postwhisker _ (peisretr _) @* _). + apply pmap_precompose_idmap. +Defined. + +(** Through [pfiber2_loops], the double fiber projection of an exact sequence is loop inversion followed by [loops] of the projection. *) +Definition pfiber2_loops_pfib2 {F X Y : pType} + (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f} + : ((pfiber2_loops f) + o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)) : _ ->* _) + o* pfib (pfib i) + ==* fmap loops f o* (loops_inv X o* pfiber2_loops i). +Proof. + destruct H as [cx conn]; revert conn. + destruct cx as [cxpw cxcell]; intro conn. + pointed_reduce. + snapply Build_pHomotopy. + - intros [[u w] v]. + cbn in v. + revert w; revert v; revert u. + refine (paths_ind_r _ _ _). + intro w. + refine (pfiber2_loops_beta f 1 (i point1) (cxpw point1) _ @ _). + refine (whiskerL _ (whiskerL _ cxcell) @ _). + exact (ap (concat 1) + (whiskerR + (inverse2 (ap (ap f) (concat_p1 _ @ (concat_1p _ @ ap_idmap w))) + @ (ap_V f w)^) _)). + - cbn; cbv beta iota delta + [point_htpy square_pfib_pequiv_cxfib phomotopy_transitive + phomotopy_symmetric pmap_postcompose_idmap pfib_cxfib pequiv_cxfib + cxfib HFiber.functor_hfiber2 ispointed_fiber functor_sigma + functor_pfiber pmap_compose pointed_htpy point_eq]; + cbn. + generalize dependent (cxpw point1). + refine (paths_ind_r _ _ _). + cbn. + reflexivity. +Defined. + (** ** Long exact sequences *) Record LongExactSequence (k : Modality) (N : SuccStr) : Type := diff --git a/theories/Homotopy/HomotopyGroup.v b/theories/Homotopy/HomotopyGroup.v index 067cc000054..f06b29b7db5 100644 --- a/theories/Homotopy/HomotopyGroup.v +++ b/theories/Homotopy/HomotopyGroup.v @@ -350,3 +350,14 @@ Proof. exact (fmap_id (pPi n) X x). Defined. +(** The [n.+2]-nd homotopy group of an [n.+1]-truncated type vanishes. *) +Definition contr_pi_succ_istrunc `{Univalence} (n : nat) (X : pType) + `{IsTrunc n.+1 X} + : Contr (Pi n.+2 X). +Proof. + pose proof (c := equiv_istrunc_contr_iterated_loops n.+2 X _ (point _)). + apply (Build_Contr _ (tr (center _))). + srapply Trunc_ind; intro a. + exact (ap tr (contr a)). +Defined. + diff --git a/theories/Pointed/Core.v b/theories/Pointed/Core.v index b5f4d48a568..2681d55c4ea 100644 --- a/theories/Pointed/Core.v +++ b/theories/Pointed/Core.v @@ -509,11 +509,12 @@ Definition ppMap (A B : pType) : pType Infix "->**" := ppMap : pointed_scope. -Lemma pmap_punit_pconst {A : pType} (f : A ->* pUnit) : pconst ==* f. +Lemma phomotopy_pconst_contr {A B : pType} `{Contr B} (f : A ->* B) + : pconst ==* f. Proof. - srapply Build_pHomotopy. - 1: intro; apply path_unit. - apply path_contr. + snapply Build_pHomotopy. + - intro x; apply path_contr. + - apply path_contr. Defined. Lemma punit_pmap_pconst {A : pType} (f : pUnit ->* A) : pconst ==* f. @@ -594,7 +595,7 @@ Proof. exact punit_pmap_pconst. + intro B. exists pconst. - exact pmap_punit_pconst. + exact phomotopy_pconst_contr. Defined. (** The constant map is definitionally equal to the zero_morphism of a pointed category *) diff --git a/theories/Pointed/pFiber.v b/theories/Pointed/pFiber.v index c503e10cace..b9517ceea02 100644 --- a/theories/Pointed/pFiber.v +++ b/theories/Pointed/pFiber.v @@ -73,9 +73,13 @@ Definition functor_pfiber {A B C D} Proof. srapply Build_pMap. + cbn. exact (functor_hfiber2 p (point_eq k)). - + srapply path_hfiber. - - apply point_eq. - - refine (concat_pp_p _ _ _ @ _). apply moveR_Vp. exact (point_htpy p)^. + + snapply path_sigma'. + - exact (point_eq h). + - lhs napply transport_paths_Fl. + lhs napply (whiskerL _ (concat_pp_p _ _ _)). + lhs napply (whiskerL _ (whiskerL _ (point_htpy p)^)). + lhs napply (whiskerL _ (concat_V_pp _ _)). + napply concat_V_pp. Defined. Definition pequiv_pfiber {A B C D} @@ -92,7 +96,10 @@ Proof. srapply Build_pHomotopy. - intros x; reflexivity. - apply moveL_pV. cbn; unfold functor_sigma; cbn. - abstract (rewrite ap_pr1_path_sigma, concat_p1; reflexivity). + refine (ap (concat 1) (concat_p1 _ @ _)). + exact (ap_pr1_path_sigma + (u := functor_hfiber2 p (point_eq k) (ispointed_fiber f)) + (v := ispointed_fiber g) (point_eq h) _). Defined. Definition square_pequiv_pfiber {A B C D} @@ -122,3 +129,62 @@ Proof. apply concat_p1. - reflexivity. Qed. + +(** The value of [pfiber2_loops] on a general element of the double fiber. *) +Definition pfiber2_loops_beta {C D : Type} {c0 : C} {d0 : D} + (g : C -> D) (de : g c0 = d0) (c : C) (w : g c = d0) (v : c = c0) + : pfiber2_loops (Build_pMap (A:=[C, c0]) (B:=[D, d0]) g de) + (((c; w); v)) + = de^ @ ((ap g v)^ @ w). +Proof. + destruct v; destruct de. + exact ((concat_1p w)^ @ ap (concat 1) (concat_1p w)^). +Defined. + +(** The path algebra underlying the pointwise part of [pfiber2_loops_natural], with all endpoints free. *) +Local Definition pfiber2_loops_natural_core {D : Type} {y x : D} + (X : y = x) (l : x = x) + : X^ @ (1 @ (((1 @ (1 @ X)^)^ @ l) @ 1)) = 1 @ (l @ 1). +Proof. + destruct X. + exact (ap (concat 1) (concat_1p _ @ whiskerR (concat_1p l) 1)). +Defined. + +(** [pfiber2_loops] commutes with the fiber functor of a square, for an arbitrary square of pointed maps. *) +Definition pfiber2_loops_natural_functor {A B C D : pType} + {f : A ->* B} {g : C ->* D} {h : A ->* C} {k : B ->* D} + (p : k o* f ==* g o* h) + : pfiber2_loops g o* functor_pfiber (square_functor_pfiber p) + ==* fmap loops k o* pfiber2_loops f. +Proof. + pointed_reduce. + snapply Build_pHomotopy. + - intros [[c w] v]. + cbn in v. + revert w; revert v; revert c. + napply paths_ind_r. + intro w. + refine (pfiber2_loops_beta _ _ _ _ _ @ _). + refine (ap (fun q => dpoint_eq1^ @ (1 @ ((q^ @ ap k w) @ 1))) H @ _). + exact (pfiber2_loops_natural_core dpoint_eq1 (ap k w)). + - cbn; cbv beta iota delta + [point_htpy square_functor_pfiber + HFiber.functor_hfiber2 ispointed_fiber functor_sigma + functor_pfiber pmap_compose pointed_htpy point_eq]; + cbn. + generalize dependent (p point2). + napply paths_ind_r. + cbn. + generalize dependent (k (f point2)). + intros x dpe; destruct dpe. + reflexivity. +Defined. + +(** The same for an equivalence square; the underlying double-fiber map is [functor_pfiber] of the same square. *) +Definition pfiber2_loops_natural {A B C D : pType} + {f : A ->* B} {g : C ->* D} (h : A <~>* C) (k : B <~>* D) + (p : k o* f ==* g o* h) + : pfiber2_loops g + o* pequiv_pfiber (pequiv_pfiber h k p) h (square_pequiv_pfiber h k p) + ==* fmap loops k o* pfiber2_loops f + := pfiber2_loops_natural_functor p. diff --git a/theories/Pointed/pMap.v b/theories/Pointed/pMap.v index 80312bbb620..afc4aa23a82 100644 --- a/theories/Pointed/pMap.v +++ b/theories/Pointed/pMap.v @@ -44,7 +44,7 @@ Proof. refine (_ @* precompose_pconst f). apply pmap_postwhisker. symmetry. - apply pmap_punit_pconst. + apply phomotopy_pconst_contr. Defined. (* We note that the inverse of [path_pmap] computes definitionally on reflexivity, and hence [path_pmap] itself computes typally so. *)