Library HoTT.Homotopy.Bouquet

Require Import Basics Types.
Require Import Pointed WildCat.
Require Import Algebra.Groups.
Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
Require Import Homotopy.Suspension.
Require Import Homotopy.ClassifyingSpace.
Require Import Homotopy.HomotopyGroup.

Local Open Scope trunc_scope.
Local Open Scope pointed_scope.
Import ClassifyingSpaceNotation.

In this file we show that the fundamental group of a bouquet of circles indexed by a type S is the free group on that type S. We begin by defining S-indexed wedges of circles as the suspension of the pointification of S.

Section AssumeUnivalence.

  Context `{Univalence}.

An S-indexed wedge of circles a.k.a a bouquet can be defined as the suspension of the pointification of S.
  Definition Bouquet (S : Type) : pType := psusp (pointify S).

  Global Instance isconnected_bouquet (S : Type)
    : IsConnected 0 (Bouquet S).
  Proof.
    rapply isconnected_susp.
  Defined.

We can directly prove that it satisfies the desired equivalence together with naturality in the second argument.
  Lemma natequiv_pi1bouquet_rec (S : Type)
    : NatEquiv
        (opyon (Pi 1 (Bouquet S)))
        (opyon S o group_type).
  Proof.
Pointify
    nrefine (natequiv_compose _ _).
    1: refine (natequiv_prewhisker (natequiv_pointify_r S) ptype_group).
Post-compose with pequiv_loops_bg_g
    nrefine (natequiv_compose _ _).
1: rapply (natequiv_postwhisker _ (natequiv_inverse natequiv_g_loops_bg)).
Loop-susp adjoint
    nrefine (natequiv_compose _ _).
    1: refine (natequiv_prewhisker
      (natequiv_loop_susp_adjoint_r (pointify S)) B).
Pi1-BG adjunction
    rapply natequiv_bg_pi1_adjoint.
  Defined.

For the rest of this file, we don't need to unfold this.
  Local Opaque natequiv_pi1bouquet_rec.

  Theorem equiv_pi1bouquet_rec (S : Type) (G : Group)
    : (Pi 1 (Bouquet S) $-> G) <~> (S → G).
  Proof.
    apply natequiv_pi1bouquet_rec.
  Defined.

  Global Instance is1natural_equiv_pi1bouquet_rec (S : Type)
    : Is1Natural
        (opyon (Pi 1 (Bouquet S)))
        (opyon S o group_type)
        (fun G ⇒ equiv_pi1bouquet_rec S G).
  Proof.
    rapply (is1natural_natequiv (natequiv_pi1bouquet_rec _)).
  Defined.

We can define the inclusion map by using the previous equivalence on the identity group homomorphism.
  Definition pi1bouquet_incl (S : Type)
    : S → Pi 1 (Bouquet S).
  Proof.
    rapply equiv_pi1bouquet_rec.
    apply grp_homo_id.
  Defined.

The fundemental group of an S-bouquet is the free group on S.
  Global Instance isfreegroupon_pi1bouquet (S : Type)
    : IsFreeGroupOn S (Pi 1 (Bouquet S)) (pi1bouquet_incl S).
  Proof.
    apply equiv_isfreegroupon_isequiv_precomp.
    intro G.
    snrapply isequiv_homotopic'.
    1: apply equiv_pi1bouquet_rec.
    intros f.
    refine (_ @ @is1natural_equiv_pi1bouquet_rec S _ _ f grp_homo_id).
    simpl; f_ap; symmetry.
    rapply (cat_idr_strong f).
  Defined.

End AssumeUnivalence.