Library HoTT.Homotopy.ClassifyingSpace
Require Import Basics Types.
Require Import Pointed WildCat.
Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
Require Import Algebra.AbGroups.
Require Import Homotopy.HSpace.Core.
Require Import TruncType.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.WhiteheadsPrinciple.
Local Open Scope pointed_scope.
Local Open Scope mc_scope.
Local Open Scope trunc_scope.
Local Open Scope mc_mult_scope.
Require Import Pointed WildCat.
Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
Require Import Algebra.AbGroups.
Require Import Homotopy.HSpace.Core.
Require Import TruncType.
Require Import Truncations.Core Truncations.Connectedness.
Require Import Homotopy.HomotopyGroup.
Require Import Homotopy.WhiteheadsPrinciple.
Local Open Scope pointed_scope.
Local Open Scope mc_scope.
Local Open Scope trunc_scope.
Local Open Scope mc_mult_scope.
We define the Classifying space of a group to be the following HIT:
Module Export ClassifyingSpace.
Section ClassifyingSpace.
Private Inductive ClassifyingSpace (G : Group) :=
| bbase : ClassifyingSpace G.
Context {G : Group}.
Axiom bloop : G → bbase G = bbase G.
Global Arguments bbase {_}.
Axiom bloop_pp : ∀ x y, bloop (x × y) = bloop x @ bloop y.
Global Instance istrunc_ClassifyingSpace
: IsTrunc 1 (ClassifyingSpace G).
Proof. Admitted.
End ClassifyingSpace.
Section ClassifyingSpace.
Private Inductive ClassifyingSpace (G : Group) :=
| bbase : ClassifyingSpace G.
Context {G : Group}.
Axiom bloop : G → bbase G = bbase G.
Global Arguments bbase {_}.
Axiom bloop_pp : ∀ x y, bloop (x × y) = bloop x @ bloop y.
Global Instance istrunc_ClassifyingSpace
: IsTrunc 1 (ClassifyingSpace G).
Proof. Admitted.
End ClassifyingSpace.
Now we can state the expected dependent elimination principle, and derive other versions of the elimination principle from it.
Note that since our classifying space is 1-truncated, we can only eliminate into 1-truncated type families.
Definition ClassifyingSpace_ind
(P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc 1 (P b)}
(bbase' : P bbase)
(bloop' : ∀ x, DPath P (bloop x) bbase' bbase')
(bloop_pp' : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop' (x × y)) ((bloop' x) @Dp (bloop' y)) 1 1)
(b : ClassifyingSpace G)
: P b
:= match b with
bbase ⇒ (fun _ _ ⇒ bbase')
end bloop' bloop_pp'.
(P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc 1 (P b)}
(bbase' : P bbase)
(bloop' : ∀ x, DPath P (bloop x) bbase' bbase')
(bloop_pp' : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop' (x × y)) ((bloop' x) @Dp (bloop' y)) 1 1)
(b : ClassifyingSpace G)
: P b
:= match b with
bbase ⇒ (fun _ _ ⇒ bbase')
end bloop' bloop_pp'.
Here we state the computation rule for ClassifyingSpace_ind over bloop as an axiom. We don't need one for bloop_pp since we have a 1-type. We leave this as admitted since the computation rule is an axiom.
Definition ClassifyingSpace_ind_beta_bloop
(P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc 1 (P b)}
(bbase' : P bbase) (bloop' : ∀ x, DPath P (bloop x) bbase' bbase')
(bloop_pp' : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop' (x × y)) ((bloop' x) @Dp (bloop' y)) 1 1)
(x : G)
: apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp') (bloop x) = bloop' x.
Proof. Admitted.
End ClassifyingSpace_ind.
End ClassifyingSpace.
(P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc 1 (P b)}
(bbase' : P bbase) (bloop' : ∀ x, DPath P (bloop x) bbase' bbase')
(bloop_pp' : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop' (x × y)) ((bloop' x) @Dp (bloop' y)) 1 1)
(x : G)
: apD (ClassifyingSpace_ind P bbase' bloop' bloop_pp') (bloop x) = bloop' x.
Proof. Admitted.
End ClassifyingSpace_ind.
End ClassifyingSpace.
Other eliminators
The non-dependent eliminator
Definition ClassifyingSpace_rec
(P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G → bbase' = bbase')
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: ClassifyingSpace G → P.
Proof.
srefine (ClassifyingSpace_ind (fun _ ⇒ P) bbase' _ _).
1: intro x; apply dp_const, bloop', x.
intros x y.
apply ds_const'.
rapply sq_GGcc.
2: refine (_ @ ap _ (dp_const_pp _ _)).
1,2: symmetry; apply eissect.
by apply sq_G1.
Defined.
(P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G → bbase' = bbase')
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: ClassifyingSpace G → P.
Proof.
srefine (ClassifyingSpace_ind (fun _ ⇒ P) bbase' _ _).
1: intro x; apply dp_const, bloop', x.
intros x y.
apply ds_const'.
rapply sq_GGcc.
2: refine (_ @ ap _ (dp_const_pp _ _)).
1,2: symmetry; apply eissect.
by apply sq_G1.
Defined.
Computation rule for non-dependent eliminator
Definition ClassifyingSpace_rec_beta_bloop
(P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G → bbase' = bbase')
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y) (x : G)
: ap (ClassifyingSpace_rec P bbase' bloop' bloop_pp') (bloop x) = bloop' x.
Proof.
rewrite <- dp_apD_const'.
unfold ClassifyingSpace_rec.
rewrite ClassifyingSpace_ind_beta_bloop.
apply eissect.
Qed.
(P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G → bbase' = bbase')
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y) (x : G)
: ap (ClassifyingSpace_rec P bbase' bloop' bloop_pp') (bloop x) = bloop' x.
Proof.
rewrite <- dp_apD_const'.
unfold ClassifyingSpace_rec.
rewrite ClassifyingSpace_ind_beta_bloop.
apply eissect.
Qed.
Sometimes we want to induct into a set which means we can ignore the bloop_pp arguments. Since this is a routine argument, we turn it into a special case of our induction principle.
Definition ClassifyingSpace_ind_hset
(P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc 0 (P b)}
(bbase' : P bbase) (bloop' : ∀ x, DPath P (bloop x) bbase' bbase')
: ∀ b, P b.
Proof.
refine (ClassifyingSpace_ind P bbase' bloop' _).
intros.
apply ds_G1.
apply path_ishprop.
Defined.
Definition ClassifyingSpace_rec_hset
(P : Type) `{IsTrunc 0 P} (bbase' : P) (bloop' : G → bbase' = bbase')
: ClassifyingSpace G → P.
Proof.
srapply (ClassifyingSpace_rec P bbase' bloop' _).
intros; apply path_ishprop.
Defined.
(P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc 0 (P b)}
(bbase' : P bbase) (bloop' : ∀ x, DPath P (bloop x) bbase' bbase')
: ∀ b, P b.
Proof.
refine (ClassifyingSpace_ind P bbase' bloop' _).
intros.
apply ds_G1.
apply path_ishprop.
Defined.
Definition ClassifyingSpace_rec_hset
(P : Type) `{IsTrunc 0 P} (bbase' : P) (bloop' : G → bbase' = bbase')
: ClassifyingSpace G → P.
Proof.
srapply (ClassifyingSpace_rec P bbase' bloop' _).
intros; apply path_ishprop.
Defined.
Similarly, when eliminating into an hprop, we only have to handle the basepoint.
Definition ClassifyingSpace_ind_hprop (P : ClassifyingSpace G → Type)
`{∀ b, IsTrunc (-1) (P b)} (bbase' : P bbase)
: ∀ b, P b.
Proof.
refine (ClassifyingSpace_ind_hset P bbase' _).
intros; rapply dp_ishprop.
Defined.
End Eliminators.
`{∀ b, IsTrunc (-1) (P b)} (bbase' : P bbase)
: ∀ b, P b.
Proof.
refine (ClassifyingSpace_ind_hset P bbase' _).
intros; rapply dp_ishprop.
Defined.
End Eliminators.
The classifying space is 0-connected.
Global Instance isconnected_classifyingspace {G : Group}
: IsConnected 0 (ClassifyingSpace G).
Proof.
apply (Build_Contr _ (tr bbase)).
srapply Trunc_ind.
srapply ClassifyingSpace_ind_hprop; reflexivity.
Defined.
: IsConnected 0 (ClassifyingSpace G).
Proof.
apply (Build_Contr _ (tr bbase)).
srapply Trunc_ind.
srapply ClassifyingSpace_ind_hprop; reflexivity.
Defined.
The classifying space of a group is pointed.
Global Instance ispointed_classifyingspace (G : Group)
: IsPointed (ClassifyingSpace G)
:= bbase.
Definition pClassifyingSpace (G : Group) := [ClassifyingSpace G, bbase].
: IsPointed (ClassifyingSpace G)
:= bbase.
Definition pClassifyingSpace (G : Group) := [ClassifyingSpace G, bbase].
Module Import ClassifyingSpaceNotation.
Definition B G := pClassifyingSpace G.
End ClassifyingSpaceNotation.
Definition B G := pClassifyingSpace G.
End ClassifyingSpaceNotation.
bloop takes the unit of the group to reflexivity.
Definition bloop_id {G : Group} : bloop (mon_unit : G) = idpath.
Proof.
symmetry.
apply (cancelL (bloop mon_unit)).
refine (_ @ bloop_pp _ _).
refine (_ @ ap _ (left_identity _)^).
apply concat_p1.
Defined.
Proof.
symmetry.
apply (cancelL (bloop mon_unit)).
refine (_ @ bloop_pp _ _).
refine (_ @ ap _ (left_identity _)^).
apply concat_p1.
Defined.
Definition bloop_inv {G : Group} : ∀ x : G, bloop (-x) = (bloop x)^.
Proof.
intro x.
refine (_ @ concat_p1 _).
apply moveL_Vp.
refine (_ @ bloop_id).
refine ((bloop_pp _ _)^ @ _).
apply ap, right_inverse.
Defined.
Proof.
intro x.
refine (_ @ concat_p1 _).
apply moveL_Vp.
refine (_ @ bloop_id).
refine ((bloop_pp _ _)^ @ _).
apply ap, right_inverse.
Defined.
The underlying pointed map of pequiv_g_loops_bg.
Definition pbloop {G : Group} : G ->* loops (B G).
Proof.
srapply Build_pMap.
1: exact bloop.
apply bloop_id.
Defined.
(* This says that B is left adjoint to the loop space functor from pointed 1-types to groups. *)
Definition pClassifyingSpace_rec {G : Group} (P : pType) `{IsTrunc 1 P}
(bloop' : G → loops P)
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: B G ->* P
:= Build_pMap (B G) P (ClassifyingSpace_rec P (point P) bloop' bloop_pp') idpath.
(* And this is one of the standard facts about adjoint functors: (R h') o eta = h, where h : G -> R P, h' : L G -> P is the adjunct, and eta (bloop) is the unit. *)
Definition pClassifyingSpace_rec_beta_bloop {G : Group} (P : pType) `{IsTrunc 1 P}
(bloop' : G → loops P)
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: fmap loops (pClassifyingSpace_rec P bloop' bloop_pp') o bloop == bloop'.
Proof.
intro x; simpl.
refine (concat_1p _ @ concat_p1 _ @ _).
apply ClassifyingSpace_rec_beta_bloop.
Defined.
Proof.
srapply Build_pMap.
1: exact bloop.
apply bloop_id.
Defined.
(* This says that B is left adjoint to the loop space functor from pointed 1-types to groups. *)
Definition pClassifyingSpace_rec {G : Group} (P : pType) `{IsTrunc 1 P}
(bloop' : G → loops P)
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: B G ->* P
:= Build_pMap (B G) P (ClassifyingSpace_rec P (point P) bloop' bloop_pp') idpath.
(* And this is one of the standard facts about adjoint functors: (R h') o eta = h, where h : G -> R P, h' : L G -> P is the adjunct, and eta (bloop) is the unit. *)
Definition pClassifyingSpace_rec_beta_bloop {G : Group} (P : pType) `{IsTrunc 1 P}
(bloop' : G → loops P)
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: fmap loops (pClassifyingSpace_rec P bloop' bloop_pp') o bloop == bloop'.
Proof.
intro x; simpl.
refine (concat_1p _ @ concat_p1 _ @ _).
apply ClassifyingSpace_rec_beta_bloop.
Defined.
Section EncodeDecode.
Context `{Univalence} {G : Group}.
Local Definition codes : B G → HSet.
Proof.
srapply ClassifyingSpace_rec.
+ srapply (Build_HSet G).
+ intro x.
apply path_trunctype.
exact (Build_Equiv _ _ (fun t ⇒ t × x) _).
+ intros x y; cbn beta.
refine (_ @ path_trunctype_pp _ _).
apply ap, path_equiv, path_forall.
intro; cbn.
apply associativity.
Defined.
Local Definition encode : ∀ b, bbase = b → codes b.
Proof.
intros b p.
exact (transport codes p mon_unit).
Defined.
Local Definition codes_transport
: ∀ x y : G, transport codes (bloop x) y = y × x.
Proof.
intros x y.
rewrite transport_idmap_ap.
rewrite ap_compose.
rewrite ClassifyingSpace_rec_beta_bloop.
rewrite ap_trunctype.
by rewrite transport_path_universe_uncurried.
Qed.
Local Definition decode : ∀ (b : B G), codes b → bbase = b.
Proof.
srapply ClassifyingSpace_ind_hset.
+ exact bloop.
+ intro x.
apply dp_arrow.
intro y; cbn in ×.
apply dp_paths_r.
refine ((bloop_pp _ _)^ @ _).
symmetry.
apply ap, codes_transport.
Defined.
Local Lemma decode_encode : ∀ b p, decode b (encode b p) = p.
Proof.
intros b p.
destruct p.
apply bloop_id.
Defined.
Global Instance isequiv_bloop : IsEquiv (@bloop G).
Proof.
srapply isequiv_adjointify.
+ exact (encode _).
+ rapply decode_encode.
+ intro x.
refine (codes_transport _ _ @ _).
apply left_identity.
Defined.
Context `{Univalence} {G : Group}.
Local Definition codes : B G → HSet.
Proof.
srapply ClassifyingSpace_rec.
+ srapply (Build_HSet G).
+ intro x.
apply path_trunctype.
exact (Build_Equiv _ _ (fun t ⇒ t × x) _).
+ intros x y; cbn beta.
refine (_ @ path_trunctype_pp _ _).
apply ap, path_equiv, path_forall.
intro; cbn.
apply associativity.
Defined.
Local Definition encode : ∀ b, bbase = b → codes b.
Proof.
intros b p.
exact (transport codes p mon_unit).
Defined.
Local Definition codes_transport
: ∀ x y : G, transport codes (bloop x) y = y × x.
Proof.
intros x y.
rewrite transport_idmap_ap.
rewrite ap_compose.
rewrite ClassifyingSpace_rec_beta_bloop.
rewrite ap_trunctype.
by rewrite transport_path_universe_uncurried.
Qed.
Local Definition decode : ∀ (b : B G), codes b → bbase = b.
Proof.
srapply ClassifyingSpace_ind_hset.
+ exact bloop.
+ intro x.
apply dp_arrow.
intro y; cbn in ×.
apply dp_paths_r.
refine ((bloop_pp _ _)^ @ _).
symmetry.
apply ap, codes_transport.
Defined.
Local Lemma decode_encode : ∀ b p, decode b (encode b p) = p.
Proof.
intros b p.
destruct p.
apply bloop_id.
Defined.
Global Instance isequiv_bloop : IsEquiv (@bloop G).
Proof.
srapply isequiv_adjointify.
+ exact (encode _).
+ rapply decode_encode.
+ intro x.
refine (codes_transport _ _ @ _).
apply left_identity.
Defined.
The defining property of BG.
Pointed version of the defining property.
Definition pequiv_g_loops_bg : G <~>* loops (B G)
:= Build_pEquiv _ _ pbloop _.
Definition pequiv_loops_bg_g := pequiv_g_loops_bg^-1*%equiv.
:= Build_pEquiv _ _ pbloop _.
Definition pequiv_loops_bg_g := pequiv_g_loops_bg^-1*%equiv.
We also have that the equivalence is a group isomorphism.
First we show that the loop space of a pointed 1-type is a group.
Definition LoopGroup (X : pType) `{IsTrunc 1 X} : Group
:= Build_Group (loops X) concat idpath inverse
(Build_IsGroup _ _ _ _
(Build_IsMonoid _ _ _
(Build_IsSemiGroup _ _ _ concat_p_pp) concat_1p concat_p1)
concat_Vp concat_pV).
Definition grp_iso_g_loopgroup_bg : GroupIsomorphism G (LoopGroup (B G)).
Proof.
snrapply Build_GroupIsomorphism'.
1: exact equiv_g_loops_bg.
intros x y.
apply bloop_pp.
Defined.
Definition grp_iso_g_pi1_bg : GroupIsomorphism G (Pi1 (B G)).
Proof.
snrapply (transitive_groupisomorphism _ _ _ grp_iso_g_loopgroup_bg).
snrapply Build_GroupIsomorphism'.
- rapply equiv_tr.
- intros x y; reflexivity.
Defined.
(* We also record this fact. *)
Definition grp_homo_loops {X Y : pType} `{IsTrunc 1 X} `{IsTrunc 1 Y}
: (X ->** Y) ->* [LoopGroup X $-> LoopGroup Y, grp_homo_const].
Proof.
snrapply Build_pMap.
- intro f.
snrapply Build_GroupHomomorphism.
+ exact (fmap loops f).
+ nrapply fmap_loops_pp.
- cbn beta.
apply equiv_path_grouphomomorphism.
exact (pointed_htpy fmap_loops_pconst).
Defined.
End EncodeDecode.
:= Build_Group (loops X) concat idpath inverse
(Build_IsGroup _ _ _ _
(Build_IsMonoid _ _ _
(Build_IsSemiGroup _ _ _ concat_p_pp) concat_1p concat_p1)
concat_Vp concat_pV).
Definition grp_iso_g_loopgroup_bg : GroupIsomorphism G (LoopGroup (B G)).
Proof.
snrapply Build_GroupIsomorphism'.
1: exact equiv_g_loops_bg.
intros x y.
apply bloop_pp.
Defined.
Definition grp_iso_g_pi1_bg : GroupIsomorphism G (Pi1 (B G)).
Proof.
snrapply (transitive_groupisomorphism _ _ _ grp_iso_g_loopgroup_bg).
snrapply Build_GroupIsomorphism'.
- rapply equiv_tr.
- intros x y; reflexivity.
Defined.
(* We also record this fact. *)
Definition grp_homo_loops {X Y : pType} `{IsTrunc 1 X} `{IsTrunc 1 Y}
: (X ->** Y) ->* [LoopGroup X $-> LoopGroup Y, grp_homo_const].
Proof.
snrapply Build_pMap.
- intro f.
snrapply Build_GroupHomomorphism.
+ exact (fmap loops f).
+ nrapply fmap_loops_pp.
- cbn beta.
apply equiv_path_grouphomomorphism.
exact (pointed_htpy fmap_loops_pconst).
Defined.
End EncodeDecode.
When G is an abelian group, BG is an H-space.
Section HSpace_bg.
Context {G : AbGroup}.
Definition bg_mul : B G → B G → B G.
Proof.
intro b.
snrapply ClassifyingSpace_rec.
1: exact _.
1: exact b.
{ intro x.
revert b.
snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: exact (bloop x).
cbn; intro y.
apply dp_paths_lr.
refine (concat_pp_p _ _ _ @ _).
apply moveR_Vp.
refine ((bloop_pp _ _)^ @ _ @ bloop_pp _ _).
apply ap, commutativity. }
intros x y.
revert b.
srapply ClassifyingSpace_ind_hprop.
exact (bloop_pp x y).
Defined.
Definition bg_mul_symm : ∀ x y, bg_mul x y = bg_mul y x.
Proof.
intros x.
srapply ClassifyingSpace_ind_hset.
{ simpl.
revert x.
srapply ClassifyingSpace_ind_hset.
1: reflexivity.
intros x.
apply sq_dp^-1, sq_1G.
refine (ap_idmap _ @ _^).
nrapply ClassifyingSpace_rec_beta_bloop. }
intros y; revert x.
simpl.
snrapply ClassifyingSpace_ind_hprop.
1: exact _.
simpl.
nrapply (transport_paths_FFlr' (g := idmap)).
apply equiv_p1_1q.
lhs nrapply ap_idmap.
nrapply ClassifyingSpace_rec_beta_bloop.
Defined.
Definition bg_mul_left_id
: ∀ b : B G, bg_mul bbase b = b.
Proof.
apply bg_mul_symm.
Defined.
Definition bg_mul_right_id
: ∀ b : B G, bg_mul b bbase = b.
Proof.
reflexivity.
Defined.
Global Instance ishspace_bg : IsHSpace (B G)
:= Build_IsHSpace _
bg_mul
bg_mul_left_id
bg_mul_right_id.
End HSpace_bg.
Context {G : AbGroup}.
Definition bg_mul : B G → B G → B G.
Proof.
intro b.
snrapply ClassifyingSpace_rec.
1: exact _.
1: exact b.
{ intro x.
revert b.
snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: exact (bloop x).
cbn; intro y.
apply dp_paths_lr.
refine (concat_pp_p _ _ _ @ _).
apply moveR_Vp.
refine ((bloop_pp _ _)^ @ _ @ bloop_pp _ _).
apply ap, commutativity. }
intros x y.
revert b.
srapply ClassifyingSpace_ind_hprop.
exact (bloop_pp x y).
Defined.
Definition bg_mul_symm : ∀ x y, bg_mul x y = bg_mul y x.
Proof.
intros x.
srapply ClassifyingSpace_ind_hset.
{ simpl.
revert x.
srapply ClassifyingSpace_ind_hset.
1: reflexivity.
intros x.
apply sq_dp^-1, sq_1G.
refine (ap_idmap _ @ _^).
nrapply ClassifyingSpace_rec_beta_bloop. }
intros y; revert x.
simpl.
snrapply ClassifyingSpace_ind_hprop.
1: exact _.
simpl.
nrapply (transport_paths_FFlr' (g := idmap)).
apply equiv_p1_1q.
lhs nrapply ap_idmap.
nrapply ClassifyingSpace_rec_beta_bloop.
Defined.
Definition bg_mul_left_id
: ∀ b : B G, bg_mul bbase b = b.
Proof.
apply bg_mul_symm.
Defined.
Definition bg_mul_right_id
: ∀ b : B G, bg_mul b bbase = b.
Proof.
reflexivity.
Defined.
Global Instance ishspace_bg : IsHSpace (B G)
:= Build_IsHSpace _
bg_mul
bg_mul_left_id
bg_mul_right_id.
End HSpace_bg.
Functoriality of B(-)
Global Instance is0functor_pclassifyingspace : Is0Functor B.
Proof.
apply Build_Is0Functor.
intros G H f.
snrapply pClassifyingSpace_rec.
- exact _.
- exact (bloop o f).
- intros x y.
refine (ap bloop (grp_homo_op f x y) @ _).
apply bloop_pp.
Defined.
Definition bloop_natural (G H : Group) (f : G $-> H)
: fmap loops (fmap B f) o bloop == bloop o f.
Proof.
nrapply pClassifyingSpace_rec_beta_bloop.
Defined.
Lemma pbloop_natural (G K : Group) (f : G $-> K)
: fmap loops (fmap B f) o× pbloop ==* pbloop o× f.
Proof.
srapply phomotopy_homotopy_hset.
apply bloop_natural.
Defined.
Definition natequiv_g_loops_bg `{Univalence}
: NatEquiv ptype_group (loops o B).
Proof.
snrapply Build_NatEquiv.
1: intros G; rapply pequiv_g_loops_bg.
snrapply Build_Is1Natural.
intros X Y f.
symmetry.
apply pbloop_natural.
Defined.
Global Instance is1functor_pclassifyingspace : Is1Functor B.
Proof.
apply Build_Is1Functor.
Action on 2-cells
- intros G H f g p.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro x.
rapply equiv_sq_dp^-1.
simpl.
rewrite 2 ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
apply ap.
exact (p x). }
reflexivity.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro x.
rapply equiv_sq_dp^-1.
simpl.
rewrite 2 ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
apply ap.
exact (p x). }
reflexivity.
Preservation of identity
- intros G.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro x.
rapply equiv_sq_dp^-1.
simpl.
rewrite ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
symmetry.
apply ap_idmap. }
reflexivity.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro x.
rapply equiv_sq_dp^-1.
simpl.
rewrite ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
symmetry.
apply ap_idmap. }
reflexivity.
Preservation of composition
- intros G H K g f.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro x.
rapply equiv_sq_dp^-1.
simpl.
rapply sq_ccGG.
1,2: symmetry.
2: refine (ap_compose (ClassifyingSpace_rec _ _ _ (fun x y ⇒
ap bloop (grp_homo_op g x y) @ bloop_pp (g x) (g y))) _ (bloop x)
@ ap _ _ @ _).
1-3: nrapply ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
reflexivity. }
reflexivity.
Defined.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro x.
rapply equiv_sq_dp^-1.
simpl.
rapply sq_ccGG.
1,2: symmetry.
2: refine (ap_compose (ClassifyingSpace_rec _ _ _ (fun x y ⇒
ap bloop (grp_homo_op g x y) @ bloop_pp (g x) (g y))) _ (bloop x)
@ ap _ _ @ _).
1-3: nrapply ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
reflexivity. }
reflexivity.
Defined.
Global Instance isequiv_fmap_pclassifyingspace `{U : Univalence} (G H : Group)
: IsEquiv (fmap B (a := G) (b := H)).
Proof.
snrapply isequiv_adjointify.
{ intros f.
refine (grp_homo_compose (grp_iso_inverse _) (grp_homo_compose _ _)).
1,3: rapply grp_iso_g_loopgroup_bg.
exact (grp_homo_loops f). }
{ intros f.
rapply equiv_path_pforall.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
{ cbn; symmetry.
rapply (point_eq f). }
{ intro g.
rapply equiv_sq_dp^-1.
rewrite ClassifyingSpace_rec_beta_bloop.
simpl.
rapply sq_ccGc.
1: symmetry; rapply decode_encode.
apply equiv_sq_path.
rewrite concat_pp_p.
rewrite concat_pp_V.
reflexivity. } }
symmetry; apply concat_1p. }
intros f.
rapply equiv_path_grouphomomorphism.
intro x.
rapply (moveR_equiv_V' equiv_g_loops_bg).
nrapply pClassifyingSpace_rec_beta_bloop.
Defined.
: IsEquiv (fmap B (a := G) (b := H)).
Proof.
snrapply isequiv_adjointify.
{ intros f.
refine (grp_homo_compose (grp_iso_inverse _) (grp_homo_compose _ _)).
1,3: rapply grp_iso_g_loopgroup_bg.
exact (grp_homo_loops f). }
{ intros f.
rapply equiv_path_pforall.
snrapply Build_pHomotopy.
{ snrapply ClassifyingSpace_ind_hset.
1: exact _.
{ cbn; symmetry.
rapply (point_eq f). }
{ intro g.
rapply equiv_sq_dp^-1.
rewrite ClassifyingSpace_rec_beta_bloop.
simpl.
rapply sq_ccGc.
1: symmetry; rapply decode_encode.
apply equiv_sq_path.
rewrite concat_pp_p.
rewrite concat_pp_V.
reflexivity. } }
symmetry; apply concat_1p. }
intros f.
rapply equiv_path_grouphomomorphism.
intro x.
rapply (moveR_equiv_V' equiv_g_loops_bg).
nrapply pClassifyingSpace_rec_beta_bloop.
Defined.
Hence we have that group homomorphisms are equivalent to pointed maps between their deloopings.
Theorem equiv_grp_homo_pmap_bg `{U : Univalence} (G H : Group)
: (G $-> H) <~> (B G $-> B H).
Proof.
snrapply Build_Equiv.
2: apply isequiv_fmap_pclassifyingspace.
Defined.
Global Instance is1natural_grp_homo_pmap_bg_r {U : Univalence} (G : Group)
: Is1Natural (opyon G) (opyon (B G) o B) (equiv_grp_homo_pmap_bg G).
Proof.
snrapply Build_Is1Natural.
intros K H f h.
apply path_hom.
rapply (fmap_comp B h f).
Defined.
Theorem natequiv_grp_homo_pmap_bg `{U : Univalence} (G : Group)
: NatEquiv (opyon G) (opyon (B G) o B).
Proof.
rapply Build_NatEquiv.
Defined.
: (G $-> H) <~> (B G $-> B H).
Proof.
snrapply Build_Equiv.
2: apply isequiv_fmap_pclassifyingspace.
Defined.
Global Instance is1natural_grp_homo_pmap_bg_r {U : Univalence} (G : Group)
: Is1Natural (opyon G) (opyon (B G) o B) (equiv_grp_homo_pmap_bg G).
Proof.
snrapply Build_Is1Natural.
intros K H f h.
apply path_hom.
rapply (fmap_comp B h f).
Defined.
Theorem natequiv_grp_homo_pmap_bg `{U : Univalence} (G : Group)
: NatEquiv (opyon G) (opyon (B G) o B).
Proof.
rapply Build_NatEquiv.
Defined.
Theorem pequiv_pclassifyingspace_pi1 `{Univalence}
(X : pType) `{IsConnected 0 X} `{IsTrunc 1 X}
: B (Pi1 X) <~>* X.
Proof.
(X : pType) `{IsConnected 0 X} `{IsTrunc 1 X}
: B (Pi1 X) <~>* X.
Proof.
The pointed map f is the adjunct to the inverse of the natural map loops X → Pi1 X. We define it first, to make the later goals easier to read.
transparent assert (f : (B (Pi1 X) ->* X)).
{ snrapply pClassifyingSpace_rec.
1: exact _.
1: exact (equiv_tr 0 _)^-1%equiv.
intros x y.
strip_truncations.
reflexivity. }
snrapply (Build_pEquiv _ _ f).
{ snrapply pClassifyingSpace_rec.
1: exact _.
1: exact (equiv_tr 0 _)^-1%equiv.
intros x y.
strip_truncations.
reflexivity. }
snrapply (Build_pEquiv _ _ f).
f is an equivalence since loops_functor f o bloop == tr^-1, and the other two maps are equivalences.
apply isequiv_is0connected_isequiv_loops.
snrapply (cancelR_isequiv bloop).
1: exact _.
rapply isequiv_homotopic'; symmetry.
nrapply pClassifyingSpace_rec_beta_bloop.
Defined.
Lemma natequiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X}
: NatEquiv (opyon (Pi1 X)) (opyon X o B).
Proof.
nrefine (natequiv_compose (G := opyon (Pi1 (pTr 1 X))) _ _).
2: exact (natequiv_opyon_equiv (A:=Group) (grp_iso_inverse (grp_iso_pi_Tr 0 X))).
refine (natequiv_compose _ (natequiv_grp_homo_pmap_bg _)).
refine (natequiv_compose (G := opyon (pTr 1 X) o B) _ _); revgoals.
{ refine (natequiv_prewhisker _ _).
refine (natequiv_opyon_equiv _^-1$).
rapply pequiv_pclassifyingspace_pi1. }
snrapply Build_NatEquiv.
1: intro; exact pequiv_ptr_rec.
rapply is1natural_prewhisker.
Defined.
snrapply (cancelR_isequiv bloop).
1: exact _.
rapply isequiv_homotopic'; symmetry.
nrapply pClassifyingSpace_rec_beta_bloop.
Defined.
Lemma natequiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X}
: NatEquiv (opyon (Pi1 X)) (opyon X o B).
Proof.
nrefine (natequiv_compose (G := opyon (Pi1 (pTr 1 X))) _ _).
2: exact (natequiv_opyon_equiv (A:=Group) (grp_iso_inverse (grp_iso_pi_Tr 0 X))).
refine (natequiv_compose _ (natequiv_grp_homo_pmap_bg _)).
refine (natequiv_compose (G := opyon (pTr 1 X) o B) _ _); revgoals.
{ refine (natequiv_prewhisker _ _).
refine (natequiv_opyon_equiv _^-1$).
rapply pequiv_pclassifyingspace_pi1. }
snrapply Build_NatEquiv.
1: intro; exact pequiv_ptr_rec.
rapply is1natural_prewhisker.
Defined.
The classifying space functor and the fundamental group functor form an adjunction (pType needs to be restricted to the subcategory of 0-connected pTypes). Note that the full adjunction should also be natural in X, but this was not needed yet.
Theorem equiv_bg_pi1_adjoint `{Univalence} (X : pType)
`{IsConnected 0 X} (G : Group)
: (Pi 1 X $-> G) <~> (X $-> B G).
Proof.
rapply natequiv_bg_pi1_adjoint.
Defined.
Lemma is1natural_equiv_bg_pi1_adjoint_r `{Univalence}
(X : pType) `{IsConnected 0 X}
: Is1Natural (opyon (Pi1 X)) (opyon X o B)
(equiv_bg_pi1_adjoint X).
Proof.
rapply (is1natural_natequiv (natequiv_bg_pi1_adjoint X)).
`{IsConnected 0 X} (G : Group)
: (Pi 1 X $-> G) <~> (X $-> B G).
Proof.
rapply natequiv_bg_pi1_adjoint.
Defined.
Lemma is1natural_equiv_bg_pi1_adjoint_r `{Univalence}
(X : pType) `{IsConnected 0 X}
: Is1Natural (opyon (Pi1 X)) (opyon X o B)
(equiv_bg_pi1_adjoint X).
Proof.
rapply (is1natural_natequiv (natequiv_bg_pi1_adjoint X)).
Why so slow? Fixed by making this opaque.