ClassifyingSpace.v

Require Import Basics Types.

Require Import Pointed Cubical WildCat.

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:

  HIT ClassifyingSpace (G : Group) : 1-Type
   | bbase : ClassifyingSpace
   | bloop : X -> bbase = bbase
   | bloop_pp : forall x y, bloop (x * y) = bloop x @ bloop y.

  We implement this is a private inductive type.
*)

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 : forall 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. *)

Section ClassifyingSpace_ind.


    Local Open Scope dpath_scope.


    Context {G : Group}.


    (** 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)
      `{forall b, IsTrunc 1 (P b)}
      (bbase' : P bbase)
      (bloop' : forall x, DPath P (bloop x) bbase' bbase')
      (bloop_pp' : forall 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)
     `{forall b, IsTrunc 1 (P b)}
      (bbase' : P bbase) (bloop' : forall x, DPath P (bloop x) bbase' bbase')
      (bloop_pp' : forall 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 *)

Section Eliminators.


  Context {G : Group}.


  (** The non-dependent eliminator *)

Definition ClassifyingSpace_rec
    (P : Type) `{IsTrunc 1 P} (bbase' : P) (bloop' : G -> bbase' = bbase')
    (bloop_pp' : forall 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' : forall 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)
    `{forall b, IsTrunc 0 (P b)}
    (bbase' : P bbase) (bloop' : forall x, DPath P (bloop x) bbase' bbase')
    : forall 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)
    `{forall b, IsTrunc (-1) (P b)} (bbase' : P bbase)
    : forall 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.


(** 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].


(** To use the [B G] notation for [pClassifyingSpace] import this module. *)

Module Import 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.


(** [bloop] "preserves inverses" by taking inverses in [G] to inverses of paths in [BG]. *)

Definition bloop_inv {G : Group} : forall 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.


(** 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' : forall 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' : forall 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.


(** Here we prove that [BG] is a delooping of [G], i.e. that [loops BG <~> G]. *)

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 : forall b, bbase = b -> codes b.

  Proof.

    intros b p.

    exact (transport codes p mon_unit).

  Defined.


  Local Definition codes_transport
    : forall 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 : forall (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 : forall 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. *)

Definition equiv_g_loops_bg : G <~> loops (B G)
    := Build_Equiv _ _ bloop _.


  (** 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.


  (** 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.


(** 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 : forall 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
    : forall b : B G, bg_mul bbase b = b.

  Proof.

    apply bg_mul_symm.

  Defined.


  Definition bg_mul_right_id
    : forall 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.

  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.

  (** 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.

  (** 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.


(** Interestingly, [fmap B] is an equivalence *)

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.


(** 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.

  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(Pi 1 X) <~>* X] for a 0-connected 1-truncated [X]. *)

Theorem pequiv_pclassifyingspace_pi1 `{Univalence}
  (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).

  (** [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.


(** 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)).

  (** Why so slow? Fixed by making this opaque. *)

Opaque equiv_bg_pi1_adjoint.

Defined.

Transparent equiv_bg_pi1_adjoint.

Timings for ClassifyingSpace.v