Library HoTT.Homotopy.ClassifyingSpace.Core
From HoTT Require Import Basics Types.
From HoTT.WildCat Require Import Core Universe Equiv NatTrans Yoneda.
Require Import Pointed.
Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
Require Import Algebra.AbGroups.AbelianGroup.
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_mult_scope.
Local Open Scope path_scope.
From HoTT.WildCat Require Import Core Universe Equiv NatTrans Yoneda.
Require Import Pointed.
Require Import Cubical.DPath Cubical.PathSquare Cubical.DPathSquare.
Require Import Algebra.AbGroups.AbelianGroup.
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_mult_scope.
Local Open Scope path_scope.
Classifying spaces of groups
HIT ClassifyingSpace (G : Group) : 1-Type | bbase : ClassifyingSpace | bloop : X -> bbase = bbase | bloop_pp : forall x y, bloop (x * y) = bloop x @ bloop y.
ClassifyingSpace is a cumulative inductive, so that WildCat machinery (e.g. fmap B) relates groups in different universes.
Local Set Polymorphic Inductive Cumulativity.
Private Inductive ClassifyingSpace@{u} (G : Group@{u}) : Type@{u} :=
| 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.
#[export] Instance istrunc_ClassifyingSpace
: IsTrunc 1 (ClassifyingSpace G).
Proof. Admitted.
End ClassifyingSpace.
Arguments bloop {G} _%_mc_mult_scope.
Private Inductive ClassifyingSpace@{u} (G : Group@{u}) : Type@{u} :=
| 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.
#[export] Instance istrunc_ClassifyingSpace
: IsTrunc 1 (ClassifyingSpace G).
Proof. Admitted.
End ClassifyingSpace.
Arguments bloop {G} _%_mc_mult_scope.
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.
lhs_V napply dp_apD_const'.
apply moveR_equiv_V.
napply ClassifyingSpace_ind_beta_bloop.
Defined.
(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.
lhs_V napply dp_apD_const'.
apply moveR_equiv_V.
napply ClassifyingSpace_ind_beta_bloop.
Defined.
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 x y.
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 x y.
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.
`{∀ b, IsTrunc (-1) (P b)} (bbase' : P bbase)
: ∀ b, P b.
Proof.
refine (ClassifyingSpace_ind_hset P bbase' _).
intros; rapply dp_ishprop.
Defined.
To eliminate into a Pi-type ∀ x, P x, you might expect to need Funext twice, once to show that the Pi-type is 1-truncated, and once to provide the path bbase' = bbase'. But by using the usual intro-revert trick, one can completely avoid Funext. This computes definitionally on bbase: ClassifyingSpace_rec_forall P bbase' bloop' bloop_pp' bbase = bbase'.
Definition ClassifyingSpace_rec_forall
{X : Type} (P : X → Type) `{∀ x, IsTrunc 1 (P x)}
(bbase' : ∀ x, P x)
(bloop' : G → bbase' == bbase')
(bloop_pp' : ∀ x : X, ∀ g h : G, bloop' (g × h) x = bloop' g x @ bloop' h x)
: ClassifyingSpace G → (∀ x, P x).
Proof.
intros bg x; revert bg.
exact (ClassifyingSpace_rec (P x) (bbase' x) (fun g ⇒ bloop' g x) (bloop_pp' x)).
Defined.
{X : Type} (P : X → Type) `{∀ x, IsTrunc 1 (P x)}
(bbase' : ∀ x, P x)
(bloop' : G → bbase' == bbase')
(bloop_pp' : ∀ x : X, ∀ g h : G, bloop' (g × h) x = bloop' g x @ bloop' h x)
: ClassifyingSpace G → (∀ x, P x).
Proof.
intros bg x; revert bg.
exact (ClassifyingSpace_rec (P x) (bbase' x) (fun g ⇒ bloop' g x) (bloop_pp' x)).
Defined.
To give a homotopy between two functions defined using induction we need to provide p and bloop_comm below; note that bloop1_pp and bloop2_pp are not involved.
Definition ClassifyingSpace_ind_homotopy
(P : ClassifyingSpace G → Type) `{∀ b, IsTrunc 1 (P b)}
(bbase1 : P bbase) (bloop1 : ∀ x, DPath P (bloop x) bbase1 bbase1)
(bloop1_pp : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop1 (x × y)) ((bloop1 x) @Dp (bloop1 y)) 1 1)
(bbase2 : P bbase) (bloop2 : ∀ x, DPath P (bloop x) bbase2 bbase2)
(bloop2_pp : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop2 (x × y)) ((bloop2 x) @Dp (bloop2 y)) 1 1)
(p : bbase1 = bbase2)
(bloop_comm : ∀ g, bloop1 g @ p = ap (transport P (bloop g)) p @ bloop2 g)
: ClassifyingSpace_ind P bbase1 bloop1 bloop1_pp
== ClassifyingSpace_ind P bbase2 bloop2 bloop2_pp.
Proof.
srapply ClassifyingSpace_ind_hset; cbn beta.
- exact p.
- intro g.
unfold DPath.
transport_paths FlFr_D.
rewrite 2 ClassifyingSpace_ind_beta_bloop.
apply bloop_comm.
Defined.
(P : ClassifyingSpace G → Type) `{∀ b, IsTrunc 1 (P b)}
(bbase1 : P bbase) (bloop1 : ∀ x, DPath P (bloop x) bbase1 bbase1)
(bloop1_pp : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop1 (x × y)) ((bloop1 x) @Dp (bloop1 y)) 1 1)
(bbase2 : P bbase) (bloop2 : ∀ x, DPath P (bloop x) bbase2 bbase2)
(bloop2_pp : ∀ x y, DPathSquare P (sq_G1 (bloop_pp x y))
(bloop2 (x × y)) ((bloop2 x) @Dp (bloop2 y)) 1 1)
(p : bbase1 = bbase2)
(bloop_comm : ∀ g, bloop1 g @ p = ap (transport P (bloop g)) p @ bloop2 g)
: ClassifyingSpace_ind P bbase1 bloop1 bloop1_pp
== ClassifyingSpace_ind P bbase2 bloop2 bloop2_pp.
Proof.
srapply ClassifyingSpace_ind_hset; cbn beta.
- exact p.
- intro g.
unfold DPath.
transport_paths FlFr_D.
rewrite 2 ClassifyingSpace_ind_beta_bloop.
apply bloop_comm.
Defined.
And here is the same result for functions defined using the recursion principle.
Definition ClassifyingSpace_rec_homotopy
(P : Type) `{IsTrunc 1 P}
(bbase1 : P) (bloop1 : G → bbase1 = bbase1)
(bloop1_pp : ∀ x y : G, bloop1 (x × y) = bloop1 x @ bloop1 y)
(bbase2 : P) (bloop2 : G → bbase2 = bbase2)
(bloop2_pp : ∀ x y : G, bloop2 (x × y) = bloop2 x @ bloop2 y)
(p : bbase1 = bbase2)
(bloop_comm : ∀ g, p @ bloop2 g = bloop1 g @ p)
: ClassifyingSpace_rec P bbase1 bloop1 bloop1_pp
== ClassifyingSpace_rec P bbase2 bloop2 bloop2_pp.
Proof.
(* It's just as easy to prove this directly as it is to use the dependent version. *)
srapply ClassifyingSpace_ind_hset; cbn beta.
- exact p.
- intro g.
transport_paths FlFr.
rewrite 2 ClassifyingSpace_rec_beta_bloop.
symmetry; apply bloop_comm.
Defined.
End Eliminators.
(P : Type) `{IsTrunc 1 P}
(bbase1 : P) (bloop1 : G → bbase1 = bbase1)
(bloop1_pp : ∀ x y : G, bloop1 (x × y) = bloop1 x @ bloop1 y)
(bbase2 : P) (bloop2 : G → bbase2 = bbase2)
(bloop2_pp : ∀ x y : G, bloop2 (x × y) = bloop2 x @ bloop2 y)
(p : bbase1 = bbase2)
(bloop_comm : ∀ g, p @ bloop2 g = bloop1 g @ p)
: ClassifyingSpace_rec P bbase1 bloop1 bloop1_pp
== ClassifyingSpace_rec P bbase2 bloop2 bloop2_pp.
Proof.
(* It's just as easy to prove this directly as it is to use the dependent version. *)
srapply ClassifyingSpace_ind_hset; cbn beta.
- exact p.
- intro g.
transport_paths FlFr.
rewrite 2 ClassifyingSpace_rec_beta_bloop.
symmetry; apply bloop_comm.
Defined.
End Eliminators.
We close the section, so we can use the above eliminators for different groups.
A two-variable version of the non-dependent eliminator. We could also have a dependent version, but since it is harder to state, we'll omit it for now. This definitionally computes to the expected recursors *as functions* when either variable is fixed to bbase: ClassifyingSpace_rec2 P bbase' bloop1 bloop1_pp bloop2 bloop2_pp bloop_comm bbase = ClassifyingSpace_rec P bbase' bloop2 bloop2_pp and (fun bg ⇒ ClassifyingSpace_rec2 P bbase' bloop1 bloop1_pp bloop2 bloop2_pp bloop_comm bg bbase) = ClassifyingSpace_rec P bbase' bloop1 bloop1_pp.
Definition ClassifyingSpace_rec2 {G H : Group}
(P : Type) `{IsTrunc 1 P} (bbase' : P)
(bloop1 : G → bbase' = bbase')
(bloop1_pp : ∀ x y : G, bloop1 (x × y) = bloop1 x @ bloop1 y)
(bloop2 : H → bbase' = bbase')
(bloop2_pp : ∀ x y : H, bloop2 (x × y) = bloop2 x @ bloop2 y)
(bloop_comm : ∀ g h, bloop1 g @ bloop2 h = bloop2 h @ bloop1 g)
: ClassifyingSpace G → ClassifyingSpace H → P.
Proof.
srapply ClassifyingSpace_rec_forall.
- exact (ClassifyingSpace_rec P bbase' bloop2 bloop2_pp).
- intro g.
snapply ClassifyingSpace_rec_homotopy.
+ exact (bloop1 g).
+ exact (bloop_comm g).
- intros x g h; revert x.
srapply ClassifyingSpace_ind_hprop; simpl.
apply bloop1_pp.
Defined.
(P : Type) `{IsTrunc 1 P} (bbase' : P)
(bloop1 : G → bbase' = bbase')
(bloop1_pp : ∀ x y : G, bloop1 (x × y) = bloop1 x @ bloop1 y)
(bloop2 : H → bbase' = bbase')
(bloop2_pp : ∀ x y : H, bloop2 (x × y) = bloop2 x @ bloop2 y)
(bloop_comm : ∀ g h, bloop1 g @ bloop2 h = bloop2 h @ bloop1 g)
: ClassifyingSpace G → ClassifyingSpace H → P.
Proof.
srapply ClassifyingSpace_rec_forall.
- exact (ClassifyingSpace_rec P bbase' bloop2 bloop2_pp).
- intro g.
snapply ClassifyingSpace_rec_homotopy.
+ exact (bloop1 g).
+ exact (bloop_comm g).
- intros x g h; revert x.
srapply ClassifyingSpace_ind_hprop; simpl.
apply bloop1_pp.
Defined.
Computation rule for ClassifyingSpace_rec2.
Definition ClassifyingSpace_rec2_beta_bloop1_bbase {G H : Group}
(P : Type) `{IsTrunc 1 P} (bbase' : P)
(bloop1 : G → bbase' = bbase')
(bloop1_pp : ∀ x y : G, bloop1 (x × y) = bloop1 x @ bloop1 y)
(bloop2 : H → bbase' = bbase')
(bloop2_pp : ∀ x y : H, bloop2 (x × y) = bloop2 x @ bloop2 y)
(bloop_comm : ∀ g h, bloop1 g @ bloop2 h = bloop2 h @ bloop1 g)
(g : G)
: ap10 (ap (ClassifyingSpace_rec2 P bbase' bloop1 bloop1_pp bloop2 bloop2_pp bloop_comm)
(bloop g))
bbase = bloop1 g.
Proof.
lhs_V napply ap_apply_Fl.
unfold ClassifyingSpace_rec2, ClassifyingSpace_rec_forall; cbn.
rapply ClassifyingSpace_rec_beta_bloop.
Defined.
(P : Type) `{IsTrunc 1 P} (bbase' : P)
(bloop1 : G → bbase' = bbase')
(bloop1_pp : ∀ x y : G, bloop1 (x × y) = bloop1 x @ bloop1 y)
(bloop2 : H → bbase' = bbase')
(bloop2_pp : ∀ x y : H, bloop2 (x × y) = bloop2 x @ bloop2 y)
(bloop_comm : ∀ g h, bloop1 g @ bloop2 h = bloop2 h @ bloop1 g)
(g : G)
: ap10 (ap (ClassifyingSpace_rec2 P bbase' bloop1 bloop1_pp bloop2 bloop2_pp bloop_comm)
(bloop g))
bbase = bloop1 g.
Proof.
lhs_V napply ap_apply_Fl.
unfold ClassifyingSpace_rec2, ClassifyingSpace_rec_forall; cbn.
rapply ClassifyingSpace_rec_beta_bloop.
Defined.
The classifying space is 0-connected.
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.
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.
refine (_ @ concat_p1 _).
apply moveL_Vp.
refine (_ @ bloop_id).
refine ((bloop_pp _ _)^ @ _).
apply ap, right_inverse.
Defined.
Proof.
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.
exact bloop_id.
Defined.
Proof.
srapply Build_pMap.
1: exact bloop.
exact bloop_id.
Defined.
The pointed version of the recursion principle. We will see in equiv_pmap_bg_loopgroup that this is an equivalence between group homomorphisms G $-> LoopGroup P and pointed maps BG ->* P, giving an adjunction.
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 (ClassifyingSpace_rec P (point P) bloop' bloop_pp') idpath.
(bloop' : G → loops P)
(bloop_pp' : ∀ x y : G, bloop' (x × y) = bloop' x @ bloop' y)
: B G ->* P
:= Build_pMap (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.
`{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.
+ exact (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.
lhs napply (transport_idmap_ap _ (bloop x)).
rhs_V rapply (transport_path_universe (.* x)).
napply (transport2 idmap).
lhs napply (ap_compose _ trunctype_type (bloop x)).
rhs_V napply ap_trunctype; apply ap.
napply ClassifyingSpace_rec_beta_bloop.
Defined.
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.
exact bloop_id.
Defined.
#[export] 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.
+ exact (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.
lhs napply (transport_idmap_ap _ (bloop x)).
rhs_V rapply (transport_path_universe (.* x)).
napply (transport2 idmap).
lhs napply (ap_compose _ trunctype_type (bloop x)).
rhs_V napply ap_trunctype; apply ap.
napply ClassifyingSpace_rec_beta_bloop.
Defined.
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.
exact bloop_id.
Defined.
#[export] 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).
:= Build_Group (loops X) concat idpath inverse
(Build_IsGroup _ _ _ _
(Build_IsMonoid _ _ _
(Build_IsSemiGroup _ _ _ concat_p_pp) concat_1p concat_p1)
concat_Vp concat_pV).
For a pointed 1-type, the loop group and the fundamental group agree.
Definition grp_iso_loopgroup_pi1 (P : pType) `{IsTrunc 1 P}
: LoopGroup P $<~> Pi1 P.
Proof.
snapply Build_GroupIsomorphism'.
- rapply equiv_tr.
- intros x y; reflexivity.
Defined.
Definition grp_iso_g_loopgroup_bg : GroupIsomorphism G (LoopGroup (B G)).
Proof.
snapply 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))
:= grp_iso_loopgroup_pi1 (B G) $oE grp_iso_g_loopgroup_bg.
(* 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.
snapply Build_pMap.
- intro f.
snapply Build_GroupHomomorphism.
+ exact (fmap loops f).
+ napply fmap_loops_pp.
- cbn beta.
apply equiv_path_grouphomomorphism.
exact (pointed_htpy fmap_loops_pconst).
Defined.
End EncodeDecode.
: LoopGroup P $<~> Pi1 P.
Proof.
snapply Build_GroupIsomorphism'.
- rapply equiv_tr.
- intros x y; reflexivity.
Defined.
Definition grp_iso_g_loopgroup_bg : GroupIsomorphism G (LoopGroup (B G)).
Proof.
snapply 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))
:= grp_iso_loopgroup_pi1 (B G) $oE grp_iso_g_loopgroup_bg.
(* 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.
snapply Build_pMap.
- intro f.
snapply Build_GroupHomomorphism.
+ exact (fmap loops f).
+ napply fmap_loops_pp.
- cbn beta.
apply equiv_path_grouphomomorphism.
exact (pointed_htpy fmap_loops_pconst).
Defined.
End EncodeDecode.
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.
: 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.
Instance is0functor_pclassifyingspace : Is0Functor B.
Proof.
apply Build_Is0Functor.
intros G H f.
snapply pClassifyingSpace_rec.
- exact _.
- exact (bloop o f).
- intros x y.
refine (ap bloop (grp_homo_op f x y) @ _).
apply bloop_pp.
Defined.
Definition ap_fmap_b_beta_bloop {G H : Group} (u : G $-> H) (g : G)
: ap (fmap B u) (bloop g) = bloop (u g)
:= ClassifyingSpace_rec_beta_bloop _ _ _ _ _.
Definition bloop_natural (G H : Group) (f : G $-> H)
: fmap loops (fmap B f) o bloop == bloop o f.
Proof.
napply 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.
snapply Build_NatEquiv.
1: intros G; exact pequiv_g_loops_bg.
snapply Build_Is1Natural.
intros X Y f.
symmetry.
apply pbloop_natural.
Defined.
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 aps 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.
(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 aps 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.
Action on 2-cells
- intros G H f g p.
snapply Build_pHomotopy.
{ snapply 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.
snapply Build_pHomotopy.
{ snapply 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 map
- intros G.
snapply Build_pHomotopy.
{ snapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro g; cbn.
transport_paths (transport_paths_Flr (f:=ClassifyingSpace_rec _ _ _ _) (bloop g) _).
apply equiv_p1_1q.
apply ClassifyingSpace_rec_beta_bloop. }
reflexivity.
snapply Build_pHomotopy.
{ snapply ClassifyingSpace_ind_hset.
1: exact _.
1: reflexivity.
intro g; cbn.
transport_paths (transport_paths_Flr (f:=ClassifyingSpace_rec _ _ _ _) (bloop g) _).
apply equiv_p1_1q.
apply ClassifyingSpace_rec_beta_bloop. }
reflexivity.
Preservation of composition
- intros G H K g f.
snapply Build_pHomotopy.
{ snapply 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: napply ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
reflexivity. }
reflexivity.
Defined.
snapply Build_pHomotopy.
{ snapply 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: napply ClassifyingSpace_rec_beta_bloop.
apply sq_1G.
reflexivity. }
reflexivity.
Defined.
The adjunction between B and the loop group
- Dropping the connectivity of the target, but keeping the source a classifying space, gives B as a left adjoint to the loop group functor on pointed 1-types. This is equiv_pmap_bg_loopgroup just below, and equiv_pmap_bg_pi1 is the same statement with Pi1 in place of LoopGroup, the two agreeing by grp_iso_loopgroup_pi1.
- Dropping the truncatedness of the source, but keeping the target a classifying space, gives B as a right adjoint to Pi1 on 0-connected pointed types. That is equiv_bg_pi1_adjoint, further below.
Definition equiv_pmap_bg_loopgroup `{Univalence} (G : Group) (P : pType) `{IsTrunc 1 P}
: (B G $-> P) <~> (G $-> LoopGroup P).
Proof.
snapply equiv_adjointify.
- intro f.
exact (grp_homo_compose (grp_homo_loops f) grp_iso_g_loopgroup_bg).
- intro phi.
exact (pClassifyingSpace_rec P phi (grp_homo_op phi)).
- intro phi.
rapply equiv_path_grouphomomorphism.
napply pClassifyingSpace_rec_beta_bloop.
- intro f.
rapply path_pforall.
snapply Build_pHomotopy.
+ srapply ClassifyingSpace_ind_hset.
× cbn; symmetry; apply (point_eq f).
× intro g.
unfold DPath.
transport_paths FlFr.
lhs napply (whiskerR (ClassifyingSpace_rec_beta_bloop _ _ _ _ _)); cbn.
apply moveR_pV, concat_p_pp.
+ cbn.
symmetry; napply concat_1p.
Defined.
: (B G $-> P) <~> (G $-> LoopGroup P).
Proof.
snapply equiv_adjointify.
- intro f.
exact (grp_homo_compose (grp_homo_loops f) grp_iso_g_loopgroup_bg).
- intro phi.
exact (pClassifyingSpace_rec P phi (grp_homo_op phi)).
- intro phi.
rapply equiv_path_grouphomomorphism.
napply pClassifyingSpace_rec_beta_bloop.
- intro f.
rapply path_pforall.
snapply Build_pHomotopy.
+ srapply ClassifyingSpace_ind_hset.
× cbn; symmetry; apply (point_eq f).
× intro g.
unfold DPath.
transport_paths FlFr.
lhs napply (whiskerR (ClassifyingSpace_rec_beta_bloop _ _ _ _ _)); cbn.
apply moveR_pV, concat_p_pp.
+ cbn.
symmetry; napply concat_1p.
Defined.
The same adjunction, phrased using the fundamental group.
Definition equiv_pmap_bg_pi1 `{Univalence} (G : Group) (P : pType) `{IsTrunc 1 P}
: (B G $-> P) <~> (G $-> Pi1 P)
:= equiv_postcompose_cat_equiv (grp_iso_loopgroup_pi1 P)
oE equiv_pmap_bg_loopgroup G P.
: (B G $-> P) <~> (G $-> Pi1 P)
:= equiv_postcompose_cat_equiv (grp_iso_loopgroup_pi1 P)
oE equiv_pmap_bg_loopgroup G P.
Definition equiv_pmap_bg_pi1_beta `{Univalence} (G : Group) (P : pType)
`{IsTrunc 1 P} (f : B G $-> P)
: equiv_pmap_bg_pi1 G P f = fmap Pi1 f $o grp_iso_g_pi1_bg.
Proof.
(* The underlying functions are definitionally equal. *)
rapply equiv_path_map_grouphomomorphism.
reflexivity.
Defined.
`{IsTrunc 1 P} (f : B G $-> P)
: equiv_pmap_bg_pi1 G P f = fmap Pi1 f $o grp_iso_g_pi1_bg.
Proof.
(* The underlying functions are definitionally equal. *)
rapply equiv_path_map_grouphomomorphism.
reflexivity.
Defined.
Interestingly, fmap B is an equivalence. This is a corollary of the adjunction: transposing fmap B u gives bloop o u by bloop_natural, so fmap B is the inverse of the adjunction composed with an isomorphism.
Instance isequiv_fmap_pclassifyingspace `{U : Univalence} (G H : Group)
: IsEquiv (fmap B (a := G) (b := H)).
Proof.
pose (e := equiv_postcompose_cat_equiv (x:=G) (grp_iso_g_loopgroup_bg (G:=H))).
rapply (isequiv_homotopic ((equiv_pmap_bg_loopgroup G (B H))^-1 oE e)).
intro phi.
apply moveR_equiv_V.
rapply equiv_path_grouphomomorphism.
change (bloop o phi == fmap loops (fmap B phi) o bloop). (* For the reader. *)
symmetry; apply bloop_natural.
Defined.
: IsEquiv (fmap B (a := G) (b := H)).
Proof.
pose (e := equiv_postcompose_cat_equiv (x:=G) (grp_iso_g_loopgroup_bg (G:=H))).
rapply (isequiv_homotopic ((equiv_pmap_bg_loopgroup G (B H))^-1 oE e)).
intro phi.
apply moveR_equiv_V.
rapply equiv_path_grouphomomorphism.
change (bloop o phi == fmap loops (fmap B phi) o bloop). (* For the reader. *)
symmetry; apply bloop_natural.
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.
snapply Build_Equiv.
2: apply isequiv_fmap_pclassifyingspace.
Defined.
: (G $-> H) <~> (B G $-> B H).
Proof.
snapply Build_Equiv.
2: apply isequiv_fmap_pclassifyingspace.
Defined.
This equivalence is natural in H.
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.
snapply 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.
: Is1Natural (opyon G) (opyon (B G) o B) (equiv_grp_homo_pmap_bg G).
Proof.
snapply 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.
B (Pi1 X) <~>* X for a 0-connected 1-truncated X. The equivalence is the adjunct of the identity map Pi1 X $-> Pi1 X.
Theorem pequiv_pclassifyingspace_pi1 `{Univalence}
(X : pType) `{IsConnected 0 X} `{IsTrunc 1 X}
: B (Pi1 X) <~>* X.
Proof.
snapply (Build_pEquiv ((equiv_pmap_bg_pi1 _ X)^-1 grp_homo_id)).
1, 2: exact _.
(* Calling the map f, it is an equivalence since fmap loops f o bloop == tr^-1, and the other two maps are equivalences. *)
apply isequiv_is0connected_isequiv_loops.
snapply (cancelR_isequiv bloop).
1: exact _.
rapply (isequiv_homotopic' (equiv_tr 0 _)^-1%equiv); symmetry.
intro g; napply pClassifyingSpace_rec_beta_bloop.
Defined.
(X : pType) `{IsConnected 0 X} `{IsTrunc 1 X}
: B (Pi1 X) <~>* X.
Proof.
snapply (Build_pEquiv ((equiv_pmap_bg_pi1 _ X)^-1 grp_homo_id)).
1, 2: exact _.
(* Calling the map f, it is an equivalence since fmap loops f o bloop == tr^-1, and the other two maps are equivalences. *)
apply isequiv_is0connected_isequiv_loops.
snapply (cancelR_isequiv bloop).
1: exact _.
rapply (isequiv_homotopic' (equiv_tr 0 _)^-1%equiv); symmetry.
intro g; napply pClassifyingSpace_rec_beta_bloop.
Defined.
The classifying space functor and the fundamental group functor form an adjunction (pType needs to be restricted to the subcategory of 0-connected pointed types). Note that the full adjunction should also be natural in X, but this was not needed yet.
Lemma natequiv_bg_pi1_adjoint `{Univalence} (X : pType) `{IsConnected 0 X}
: NatEquiv (opyon (Pi1 X)) (opyon X o B).
Proof.
refine (natequiv_compose _ (natequiv_grp_homo_pmap_bg _)).
refine (natequiv_compose (G := opyon (pTr 1 X) o B) _ _).
{ snapply Build_NatEquiv.
1: intro; exact pequiv_ptr_rec.
exact (is1natural_prewhisker (G:=opyon X) B (opyoneda _ _ _)). }
{ refine (natequiv_prewhisker _ _).
refine (natequiv_opyon_equiv _^-1$).
refine (pequiv_pclassifyingspace_pi1 (pTr 1 X) o×E (emap B _)).
exact (grp_iso_pi_Tr 0 X). }
Defined.
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)).
: NatEquiv (opyon (Pi1 X)) (opyon X o B).
Proof.
refine (natequiv_compose _ (natequiv_grp_homo_pmap_bg _)).
refine (natequiv_compose (G := opyon (pTr 1 X) o B) _ _).
{ snapply Build_NatEquiv.
1: intro; exact pequiv_ptr_rec.
exact (is1natural_prewhisker (G:=opyon X) B (opyoneda _ _ _)). }
{ refine (natequiv_prewhisker _ _).
refine (natequiv_opyon_equiv _^-1$).
refine (pequiv_pclassifyingspace_pi1 (pTr 1 X) o×E (emap B _)).
exact (grp_iso_pi_Tr 0 X). }
Defined.
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)).
Why so slow? Fixed by making this opaque.
There is also a natural equivalence for unpointed function types, which computes to the map defined above on pointed functions: equiv_bg_pi1_adjoint X G f is definitionally equal to equiv_map_bg X G (fmap B f)
Definition natequiv_map_bg `{Univalence}
(X : pType) `{IsConnected 0 X}
: NatEquiv (opyon (A:=Type) (B (Pi 1 X)) o B) (opyon (A:=Type) X o B).
Proof.
unfold opyon.
refine (natequiv_compose (G := opyon (Tr 1 X) o B) _ _).
{ snapply Build_NatEquiv.
1: intro; rapply (equiv_o_to_O (Tr 1) X).
by srapply Build_Is1Natural. }
{ refine (natequiv_prewhisker _ _).
refine (natequiv_opyon_equiv _^-1$).
refine (pequiv_pclassifyingspace_pi1 (pTr 1 X) o×E (emap B _)).
exact (grp_iso_pi_Tr 0 X). }
Defined.
Definition equiv_map_bg `{Univalence}
(X : pType) `{IsConnected 0 X} (G : Group)
: (B (Pi 1 X) → B G) <~> (X → B G).
Proof.
rapply natequiv_map_bg.
Defined.
(X : pType) `{IsConnected 0 X}
: NatEquiv (opyon (A:=Type) (B (Pi 1 X)) o B) (opyon (A:=Type) X o B).
Proof.
unfold opyon.
refine (natequiv_compose (G := opyon (Tr 1 X) o B) _ _).
{ snapply Build_NatEquiv.
1: intro; rapply (equiv_o_to_O (Tr 1) X).
by srapply Build_Is1Natural. }
{ refine (natequiv_prewhisker _ _).
refine (natequiv_opyon_equiv _^-1$).
refine (pequiv_pclassifyingspace_pi1 (pTr 1 X) o×E (emap B _)).
exact (grp_iso_pi_Tr 0 X). }
Defined.
Definition equiv_map_bg `{Univalence}
(X : pType) `{IsConnected 0 X} (G : Group)
: (B (Pi 1 X) → B G) <~> (X → B G).
Proof.
rapply natequiv_map_bg.
Defined.
Pi1 induces an equivalence on certain mapping types
Definition isequiv_fmap_pi1_pmap_dom_trunc `{Univalence} (X Y : pType)
`{IsConnected 0 X} `{IsTrunc 1 X} `{IsTrunc 1 Y}
: IsEquiv (fmap Pi1 (a:=X) (b:=Y)).
Proof.
pose (e := pequiv_pclassifyingspace_pi1 X).
tapply (isequiv_homotopic (equiv_pmap_bg_pi1 _ Y oE equiv_precompose_cat_equiv (z:=Y) e)).
intro f.
lhs napply equiv_pmap_bg_pi1_beta.
apply path_hom.
intro x.
lhs exact (fmap_comp Pi1 e f (grp_iso_g_pi1_bg x)).
(* fmap Pi1 e $o grp_iso_g_pi1_bg is the identity, since e is the adjunct of the identity map. *)
exact (ap (fmap Pi1 f) (equiv_path_grouphomomorphism^-1
((equiv_pmap_bg_pi1_beta _ X e)^ @ eisretr (equiv_pmap_bg_pi1 _ X) grp_homo_id) x)).
Defined.
`{IsConnected 0 X} `{IsTrunc 1 X} `{IsTrunc 1 Y}
: IsEquiv (fmap Pi1 (a:=X) (b:=Y)).
Proof.
pose (e := pequiv_pclassifyingspace_pi1 X).
tapply (isequiv_homotopic (equiv_pmap_bg_pi1 _ Y oE equiv_precompose_cat_equiv (z:=Y) e)).
intro f.
lhs napply equiv_pmap_bg_pi1_beta.
apply path_hom.
intro x.
lhs exact (fmap_comp Pi1 e f (grp_iso_g_pi1_bg x)).
(* fmap Pi1 e $o grp_iso_g_pi1_bg is the identity, since e is the adjunct of the identity map. *)
exact (ap (fmap Pi1 f) (equiv_path_grouphomomorphism^-1
((equiv_pmap_bg_pi1_beta _ X e)^ @ eisretr (equiv_pmap_bg_pi1 _ X) grp_homo_id) x)).
Defined.
For X 0-connected and Y a pointed 1-type, fmap Pi1 is an equivalence from pointed maps X ->* Y to group homomorphisms. Note that Y is not assumed to be connected.
Definition isequiv_fmap_pi1_pmap `{Univalence} (X Y : pType)
`{IsConnected 0 X} `{IsTrunc 1 Y}
: IsEquiv (fmap Pi1 (a:=X) (b:=Y)).
Proof.
(* Since Y is a 1-type, we can replace X by pTr 1 X, which has the same Pi1 and is a 0-connected 1-type. The square commutes by functoriality of Pi1. *)
refine (isequiv_commsq (fmap Pi1 (a:=pTr 1 X) (b:=Y)) _
(fun g : pTr 1 X $-> Y ⇒ g $o ptr)
(equiv_precompose_cat_equiv (z:=Pi1 Y) (grp_iso_pi_Tr 0 X)) _).
- intro phi; symmetry.
apply path_hom; exact (fmap_comp Pi1 ptr phi).
- rapply isequiv_fmap_pi1_pmap_dom_trunc.
- exact (equiv_isequiv pequiv_ptr_rec).
Defined.
`{IsConnected 0 X} `{IsTrunc 1 Y}
: IsEquiv (fmap Pi1 (a:=X) (b:=Y)).
Proof.
(* Since Y is a 1-type, we can replace X by pTr 1 X, which has the same Pi1 and is a 0-connected 1-type. The square commutes by functoriality of Pi1. *)
refine (isequiv_commsq (fmap Pi1 (a:=pTr 1 X) (b:=Y)) _
(fun g : pTr 1 X $-> Y ⇒ g $o ptr)
(equiv_precompose_cat_equiv (z:=Pi1 Y) (grp_iso_pi_Tr 0 X)) _).
- intro phi; symmetry.
apply path_hom; exact (fmap_comp Pi1 ptr phi).
- rapply isequiv_fmap_pi1_pmap_dom_trunc.
- exact (equiv_isequiv pequiv_ptr_rec).
Defined.
H-space structure on B G when G is abelian
Definition fmap11_B {G H K : Group}
(f1 : G $-> K) (f2 : H $-> K)
(comm: ∀ g h, f1 g × f2 h = f2 h × f1 g)
: B G → B H → B K.
Proof.
srapply ClassifyingSpace_rec2.
- exact bbase.
- exact (bloop o f1).
- intros g1 g2.
rhs_V napply bloop_pp.
apply ap, grp_homo_op.
- exact (bloop o f2).
- intros h1 h2.
rhs_V napply bloop_pp.
apply ap, grp_homo_op.
- intros g h.
refine ((bloop_pp _ _)^ @ _ @ bloop_pp _ _).
apply ap, comm.
Defined.
Definition fmap11_B_bbase {G H K : Group}
(f1 : G $-> K) (f2 : H $-> K)
(comm: ∀ g h, f1 g × f2 h = f2 h × f1 g)
: fmap11_B f1 f2 comm bbase = fmap B f2
:= idpath.
Definition fmap11_B_bbase' `{funext : Funext} {G H K : Group}
(f1 : G $-> K) (f2 : H $-> K)
(comm: ∀ g h, f1 g × f2 h = f2 h × f1 g)
: (fun x ⇒ fmap11_B f1 f2 comm x bbase) == fmap B f1.
Proof.
srapply ClassifyingSpace_ind_homotopy.
1: reflexivity.
intro x.
cbn; apply concat_p1_1p.
Defined.
(f1 : G $-> K) (f2 : H $-> K)
(comm: ∀ g h, f1 g × f2 h = f2 h × f1 g)
: B G → B H → B K.
Proof.
srapply ClassifyingSpace_rec2.
- exact bbase.
- exact (bloop o f1).
- intros g1 g2.
rhs_V napply bloop_pp.
apply ap, grp_homo_op.
- exact (bloop o f2).
- intros h1 h2.
rhs_V napply bloop_pp.
apply ap, grp_homo_op.
- intros g h.
refine ((bloop_pp _ _)^ @ _ @ bloop_pp _ _).
apply ap, comm.
Defined.
Definition fmap11_B_bbase {G H K : Group}
(f1 : G $-> K) (f2 : H $-> K)
(comm: ∀ g h, f1 g × f2 h = f2 h × f1 g)
: fmap11_B f1 f2 comm bbase = fmap B f2
:= idpath.
Definition fmap11_B_bbase' `{funext : Funext} {G H K : Group}
(f1 : G $-> K) (f2 : H $-> K)
(comm: ∀ g h, f1 g × f2 h = f2 h × f1 g)
: (fun x ⇒ fmap11_B f1 f2 comm x bbase) == fmap B f1.
Proof.
srapply ClassifyingSpace_ind_homotopy.
1: reflexivity.
intro x.
cbn; apply concat_p1_1p.
Defined.
When G is an abelian group, BG is an H-space.
The multiplication follows from fmap11_B. One can also construct it directly, which replaces some subterms that are essentially fmap B pmap_idmap with idmap. The approach using fmap11_B actually makes the proof of bg_mul_symm simpler, but bg_mul_right_id no longer holds definitionally.
Definition bg_mul : B G → B G → B G
:= fmap11_B grp_homo_id grp_homo_id commutativity.
Definition bg_mul_symm : ∀ x y, bg_mul x y = bg_mul y x.
Proof.
intros x.
srapply ClassifyingSpace_ind_hset; cbn beta.
1: reflexivity. (* bg_mul x bbase and bg_mul bbase x are definitionally equal! *)
intros g; revert x.
srapply ClassifyingSpace_ind_hprop; cbn beta.
unfold DPath.
(* Rocq rewrites the output of this step using the above definitional equality again: *)
transport_paths FlFr.
apply concat_p1_1p.
Defined.
:= fmap11_B grp_homo_id grp_homo_id commutativity.
Definition bg_mul_symm : ∀ x y, bg_mul x y = bg_mul y x.
Proof.
intros x.
srapply ClassifyingSpace_ind_hset; cbn beta.
1: reflexivity. (* bg_mul x bbase and bg_mul bbase x are definitionally equal! *)
intros g; revert x.
srapply ClassifyingSpace_ind_hprop; cbn beta.
unfold DPath.
(* Rocq rewrites the output of this step using the above definitional equality again: *)
transport_paths FlFr.
apply concat_p1_1p.
Defined.
This is not definitionally true, but bg_mul b bbase is definitionally equal to fmap B grp_homo_id, so we can use fmap_id to prove this.
Definition bg_mul_left_id : ∀ b : B G, bg_mul bbase b = b
:= fmap_id B G.
#[export] Instance ishspace_bg : IsHSpace (B G)
:= Build_IsHSpace _
bg_mul
bg_mul_left_id
bg_mul_right_id.
End HSpace_bg.
:= fmap_id B G.
#[export] Instance ishspace_bg : IsHSpace (B G)
:= Build_IsHSpace _
bg_mul
bg_mul_left_id
bg_mul_right_id.
End HSpace_bg.