module Homotopy.Space.Suspension.Pi2 {} (grp : ConcreteGroup ) (hg : HSpace (grp .B)) where

π₂ of a suspension🔗

We will prove that the second homotopy group of the suspension of a pointed connected groupoid with an H-space structure (hence an abelian concrete group) is

We start by defining a type family Hopf over which is on both poles and sends the meridian to the H-space multiplication on the right, which is an equivalence by assumption. We will show, by an encode-decode argument, that the groupoid truncation is equivalent to the fibre of Hopf over

As the name implies, the Hopf type family is the synthetic equivalent of the classic Hopf fibration, though here we have evidently generalised it beyond a map Below we prove that the total space of the Hopf fibration is the join

Hopf : ΣG  Type _
Hopf north       = G
Hopf south       = G
Hopf (merid x i) = ua (μr x) i

To encode, we use truncation recursion, since Hopf is a family of groupoids by construction, and since we have we can transport it along a to get a point in an arbitrary fibre.

encode' :  x   north  x ∥₁  Hopf x
encode' x = n-Tr-rec (tr x) λ p  subst Hopf p G₀ where
  tr :  x  is-groupoid (Hopf x)
  tr = Susp-elim-prop  s  hlevel 1) (grp .has-is-groupoid) (grp .has-is-groupoid)

To decode an element of Hopf we use suspension recursion. On the north pole we can use the suspension map on the south pole this is just a meridian; and on the meridians we must prove that these agree. Through a short calculation we can reduce this to a coherence lemma relating the composition of meridians and the H-space multiplication.

decode' :  x  Hopf x   north  x ∥₁
decode' = Susp-elim _ (n-Tr.inc  suspend BG) (n-Tr.inc  merid) λ x  ua→ λ a  to-pathp $
  inc (subst (north ≡_) (merid x) (suspend BG a)) ≡⟨ ap n-Tr.inc (subst-path-right (suspend BG a) (merid x)) 
  inc ((merid a  sym (merid G₀))  merid x)      ≡˘⟨ ap n-Tr.inc (∙-assoc _ _ _) ≡˘
  inc (merid a  sym (merid G₀)  merid x)        ≡⟨ merid-μ a x 
  inc (merid (μ a x))                             
  where

To show this coherence, we can use the wedge connectivity lemma. It will suffice to do so, in turn, when when and then to show that these agree. In either case we must show something like which is easy to do with the pre-existing coherence lemmas ∙∙-introl and ∙∙-intror, and the H-space unit laws.

  merid-μ :  a b  inc (merid a  sym (merid G₀)  merid b)  inc (merid (μ a b))
  merid-μ =
    let
      α = merid G₀

      P : (a b :  G )  Type 
      P a b = Path  north  south ∥₁ (inc (merid a  sym α  merid b)) (inc (merid (μ a b)))

      p1 :  a  P a G₀
      p1 a = ap n-Tr.inc $
           sym (double-composite _ _ _)
        ∙∙ sym (∙∙-intror (merid a) (sym α))
        ∙∙ ap merid (sym (idr a))

      p2 :  b  P G₀ b
      p2 b = ap n-Tr.inc $
           sym (double-composite _ _ _)
        ∙∙ sym (∙∙-introl (merid b) α)
        ∙∙ ap merid (sym (idl b))

Moreover, it is easy to show that these agree: by construction we’re left with showing that ∙∙-introl and ∙∙-intror agree when all three paths are the same, and by path induction we may assume that this one path is refl; In that case, they agree definitionally.

      coh : p1 G₀  p2 G₀
      coh = ap (ap n-Tr.inc) $ ap₂ (_∙∙_∙∙_ (sym (double-composite α (sym α) α)))
        (ap sym (J  y p  ∙∙-intror p (sym p)  ∙∙-introl p p) refl α))
        (ap (ap merid  sym) (sym id-coh))

      c = is-connected∙→is-connected (grp .has-is-connected)
    in Wedge.elim {A∙ = BG} {BG} 0 0 c c  _ _  hlevel 2) p1 p2 coh

We have thus constructed maps between and the truncation of the based path space We must then show that these are inverses, which, in both directions, are simple calculations.

opaque
  ΩΣG≃G :  north {A = fst BG}  north ∥₁  G
  ΩΣG≃G .fst = encode' north
  ΩΣG≃G .snd = is-iso→is-equiv (iso (decode' north) invl (invr north)) where abstract
    invl :  a  encode' north (decode' north a)  a
    invl a = Regularity.fast! (
      Equiv.from (flip μ G₀ , μ-invr G₀) (μ G₀ a) ≡⟨ ap  e  Equiv.from e (μ G₀ a)) {x = _ , μ-invr G₀} {y = id≃} (ext idr) 
      μ G₀ a                                      ≡⟨ idl a 
      a                                           )

To show that decoding inverts encoding, we use the extra generality afforded by the parameter to apply path induction.

    invr : (x : ΣG) (p :  north  x ∥₁)  decode' x (encode' x p)  p
    invr x = n-Tr-elim! _ $ J
       x p  decode' x (encode' x (inc p))  inc p)
      (ap n-Tr.inc
        ( ap₂ _∙_ (ap merid (transport-refl _)) refl
         ∙-invr (merid G₀)))

This equivalence is pointed, almost by definition.

  ΩΣG≃∙G : n-Tr∙ (Ω¹ (Σ¹ BG)) 3 ≃∙ BG
  ΩΣG≃∙G = ΩΣG≃G , transport-refl _

Furthermore, note that, by construction, the inverse pointed map of this equivalence is none other than suspend∙ followed by the inclusion into the groupoid truncation.

  ΩΣG≃∙G-inv : Equiv∙.from∙ ΩΣG≃∙G  inc∙ ∘∙ suspend∙ BG
  ΩΣG≃∙G-inv = homogeneous-funext∙ λ _  refl

Finally, we can apply to the equivalence above and use some pre-existing lemmas to show that the set truncation of the double loop space is equivalent to A couple more short calculations which we omit show that this equivalence preserves path composition, i.e. is an isomorphism of homotopy groups and that the inverse map is the expected suspension map up to truncation.

Ω²ΣG≃ΩG :   Ωⁿ 2 (Σ¹ BG)  ∥₀   Ω¹ BG 
Ω²ΣG≃ΩG =
   πₙ₊₁ 1 (Σ¹ BG)             ≃⟨ n-Tr-set 
   n-Tr∙ (Ωⁿ 2 (Σ¹ BG)) 2     ≃⟨ n-Tr-Ω¹ (Ω¹ (Σ¹ BG)) 1 .fst 
   Ω¹ (n-Tr∙ (Ω¹ (Σ¹ BG)) 3)  ≃⟨ Ω¹-ap ΩΣG≃∙G .fst 
   Ω¹ BG                      ≃∎

opaque
  unfolding Ω¹-ap

  Ω²ΣG≃ΩG-pres : is-group-hom
    (πₙ₊₁ 1 (Σ¹ BG) .snd)
    (π₁Groupoid.π₁ BG (grp .has-is-groupoid) .snd)
    (Ω²ΣG≃ΩG .fst)

  Ω²ΣG≃ΩG-inv
    :  (l :  Ω¹ BG )
     Equiv.from Ω²ΣG≃ΩG l  inc (Ω¹-map (suspend∙ BG) .fst l)
  Ω²ΣG≃ΩG-pres = record { pres-⋆ = elim! λ p q  trace p q .snd } where
    open Σ Ω²ΣG≃ΩG renaming (fst to f0) using ()
    instance
      _ :  {n}  H-Level  G  (3 + n)
      _ = basic-instance 3 (grp .has-is-groupoid)

    trace : (p q : refl  refl)  (  Ωⁿ 2 (Σ¹ BG)  ∥₀ , inc (p  q)) ≃∙ ( Ω¹ BG  , f0 (inc p)  f0 (inc q))
    trace p q =
       πₙ₊₁ 1 (Σ¹ BG)  , inc (p  q)         ≃∙⟨ n-Tr-set , refl ≃∙
       n-Tr∙ (Ωⁿ 2 (Σ¹ BG)) 2  , inc (p  q) ≃∙⟨ n-Tr-Ω¹ _ 1 .fst , n-Tr-Ω¹-∙ _ 1 p q ≃∙
       Ω¹ (n-Tr∙ (Ω¹ (Σ¹ BG)) 3)  , _        ≃∙⟨ Ω¹-ap ΩΣG≃∙G .fst , Ω¹-map-∙ (Equiv∙.to∙ ΩΣG≃∙G) (n-Tr-Ω¹ _ 1 · inc p) (n-Tr-Ω¹ _ 1 · inc q) ≃∙
       Ω¹ BG  , f0 (inc p)  f0 (inc q)      ≃∙∎

  Ω²ΣG≃ΩG-inv l = trace .snd where
    trace : ( Ω¹ BG  , l) ≃∙ ( πₙ₊₁ 1 (Σ¹ BG)  , inc (Ω¹-map (suspend∙ BG) · l))
    trace =
       Ω¹ BG                      , l                                ≃∙⟨ Ω¹-ap ΩΣG≃∙G .fst e⁻¹ , (Ω¹-ap-inv ΩΣG≃∙G ·ₚ l)  ap  x  Ω¹-map x · l) ΩΣG≃∙G-inv ≃∙
       Ω¹ (n-Tr∙ (Ω¹ (Σ¹ BG)) 3)  , Ω¹-map (inc∙ ∘∙ suspend∙ BG) · l ≃∙˘⟨ n-Tr-Ω¹ _ 1 .fst , (n-Tr-Ω¹-inc _ 1 ·ₚ _)  (Ω¹-map-∘ inc∙ (suspend∙ BG) ·ₚ l) ≃∙˘
       n-Tr∙ (Ωⁿ 2 (Σ¹ BG)) 2     , inc (Ω¹-map (suspend∙ BG) · l)   ≃∙˘⟨ n-Tr-set , refl ≃∙˘
       πₙ₊₁ 1 (Σ¹ BG)             , inc (Ω¹-map (suspend∙ BG) · l)   ≃∙∎
π₂ΣG≅ΩG : πₙ₊₁ 1 (Σ¹ BG) Groups.≅ π₁Groupoid.π₁ BG (grp .has-is-groupoid)
π₂ΣG≅ΩG = total-iso Ω²ΣG≃ΩG Ω²ΣG≃ΩG-pres

The Hopf fibration🔗

We can now prove that the total space of the Hopf fibration defined above is the join of with itself.

join→hopf : (G  G)  Σ _ Hopf
join→hopf (inl x) = north , x
join→hopf (inr x) = south , x
join→hopf (join a b i) = record
  { fst = merid (a \\ b) i
  ; snd = attach ( i)  { (i = i0)  a ; (i = i1)  b })
    (inS (μ-\\-l a b i))
  }
join→hopf-split :  x p  fibre join→hopf (x , p)
join→hopf-split = Susp-elim _
   p  inl p , refl)
   p  inr p , refl)
   x i  filler x i i1)

  module surj where module _ (x : fst BG) where
    coh :  a  PathP
       i  fibre join→hopf (merid x i , ua-inc (μr x) a i))
      (inl a , refl) (inr (μ a x) , refl)
    coh a i .fst = join a (μ a x) i
    coh a i .snd j .fst = merid (μ-\\-r a x j) i
    coh a i .snd j .snd = attach ( i)
       { (i = i0)  a ; (i = i1)  μ a x })
      (inS (∨-square (μ-zig a x) j i))

    open ua→ {e = μr x} {B = λ i z  fibre join→hopf (merid x i , z)} {f₀ = λ p  inl p , refl} {f₁ = λ p  inr p , refl} coh public

hopf→join : (Σ _ Hopf)  G  G
hopf→join a = uncurry join→hopf-split a .fst

hopf→join→hopf : is-right-inverse hopf→join join→hopf
hopf→join→hopf a = uncurry join→hopf-split a .snd

join→hopf→join : is-left-inverse hopf→join join→hopf
join→hopf→join (inl x) = refl
join→hopf→join (inr x) = refl
join→hopf→join (join a b i) =
  let it = attach ( i)  { (i = i0)  a ; (i = i1)  b }) (inS (μ-\\-l a b i)) in
  comp  l  surj.filler (a \\ b) i l it .fst  join a b i) ( i) λ where
    j (j = i0)  λ k  join a (μ-\\-l a b (i  k)) (~ k  i)
    j (i = i0)  λ k  join a (μ-\\-l a b k) (~ j  ~ k)
    j (i = i1)  λ k  inr b

∫Hopf≃join : Σ _ Hopf  ( G    G )
∫Hopf≃join .fst = hopf→join
∫Hopf≃join .snd = is-iso→is-equiv (iso join→hopf join→hopf→join hopf→join→hopf)