{-# OPTIONS --safe --lossy-unification #-}
{-
This file contains:
1. The iso π₃S²≅ℤ
2. A proof that π₃S² is generated by the Hopf map
-}
module Cubical.Homotopy.Group.Pi3S2 where

open import Cubical.Homotopy.Loopspace

open import Cubical.Homotopy.Group.LES
open import Cubical.Homotopy.Group.PinSn
open import Cubical.Homotopy.Group.Base
open import Cubical.Homotopy.HopfInvariant.HopfMap
open import Cubical.Homotopy.HopfInvariant.Base
open import Cubical.Homotopy.HopfInvariant.Homomorphism

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.GroupoidLaws
open import Cubical.Foundations.Isomorphism
open Iso
open import Cubical.Foundations.Equiv

open import Cubical.HITs.SetTruncation renaming (elim to sElim)
open import Cubical.HITs.Sn
open import Cubical.HITs.Sn.Multiplication
open import Cubical.HITs.Susp
open import Cubical.HITs.S1

open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Int

open import Cubical.Algebra.Group
open import Cubical.Algebra.Group.ZAction
open import Cubical.Algebra.Group.Exact
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Instances.Unit
open import Cubical.Algebra.Group.Instances.Int

TotalHopf→∙S² : (Σ (S₊ 2) S¹Hopf , north , base) →∙ S₊∙ 2
fst TotalHopf→∙S² = fst
snd TotalHopf→∙S² = refl

IsoTotalSpaceJoin' : Iso (Σ (S₊ 2) S¹Hopf) (S₊ 3)
IsoTotalSpaceJoin' = compIso hopfS¹.IsoTotalSpaceJoin (IsoSphereJoin 1 1)

IsoFiberTotalHopfS¹ : Iso (fiber (fst TotalHopf→∙S²) north) S¹
fun IsoFiberTotalHopfS¹ ((x , y) , z) = subst S¹Hopf z y
inv IsoFiberTotalHopfS¹ x = (north , x) , refl
rightInv IsoFiberTotalHopfS¹ x = refl
leftInv IsoFiberTotalHopfS¹ ((x , y) , z) =
  ΣPathP
    ((ΣPathP
      (sym z , (λ i → transp (λ j → S¹Hopf (z (~ i ∧ j))) i y)))
         , (λ j i → z (i ∨ ~ j)))

IsoFiberTotalHopfS¹∙≡ :
  (fiber (fst TotalHopf→∙S²) north , (north , base) , refl) ≡ S₊∙ 1
IsoFiberTotalHopfS¹∙≡ = ua∙ (isoToEquiv IsoFiberTotalHopfS¹) refl

private
  transportGroupEquiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'}
      (n : ℕ) (f : A →∙ B)
    → isEquiv (fst (πLES.A→B f n))
    → isEquiv (fst (π'∘∙Hom n f))
  transportGroupEquiv n f iseq =
    transport (λ i → isEquiv (fst (π∘∙A→B-PathP n f i))) iseq

π₃S²≅π₃TotalHopf : GroupEquiv (πGr 2 (Σ (S₊ 2) S¹Hopf , north , base))
                              (πGr 2 (S₊∙ 2))
fst (fst π₃S²≅π₃TotalHopf) = fst (πLES.A→B TotalHopf→∙S² 2)
snd (fst π₃S²≅π₃TotalHopf) =
  SES→isEquiv
    (isContr→≡UnitGroup
      (subst isContr (cong (π 3) (sym IsoFiberTotalHopfS¹∙≡))
        (∣ refl ∣₂ , (sElim (λ _ → isSetPathImplicit)
          (λ p → cong ∣_∣₂
            (isOfHLevelSuc 3 isGroupoidS¹ _ _ _ _ _ _ refl p))))))
    (isContr→≡UnitGroup
      (subst isContr (cong (π 2) (sym IsoFiberTotalHopfS¹∙≡))
        (∣ refl ∣₂ , (sElim (λ _ → isSetPathImplicit) (λ p
                    → cong ∣_∣₂ (isGroupoidS¹ _ _ _ _ refl p))))))
    (πLES.fib→A TotalHopf→∙S² 2)
    (πLES.A→B TotalHopf→∙S² 2)
    (πLES.B→fib TotalHopf→∙S² 1)
    (πLES.Ker-A→B⊂Im-fib→A TotalHopf→∙S² 2)
    (πLES.Ker-B→fib⊂Im-A→B TotalHopf→∙S² 1)
snd π₃S²≅π₃TotalHopf = snd (πLES.A→B TotalHopf→∙S² 2)

π'₃S²≅π'₃TotalHopf : GroupEquiv (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base))
                                (π'Gr 2 (S₊∙ 2))
fst (fst π'₃S²≅π'₃TotalHopf) = fst (π'∘∙Hom 2 TotalHopf→∙S²)
snd (fst π'₃S²≅π'₃TotalHopf) =
  transportGroupEquiv 2 TotalHopf→∙S² (π₃S²≅π₃TotalHopf .fst .snd)
snd π'₃S²≅π'₃TotalHopf = snd (π'∘∙Hom 2 TotalHopf→∙S²)

πS³≅πTotalHopf : (n : ℕ)
  → GroupEquiv (π'Gr n (S₊∙ 3)) (π'Gr n (Σ (S₊ 2) S¹Hopf , north , base))
πS³≅πTotalHopf n =
  π'Iso n
   ((isoToEquiv
     (invIso
      (compIso
       (hopfS¹.IsoTotalSpaceJoin)
       (IsoSphereJoin 1 1))))
  , refl)

π₃S²≅ℤ : GroupEquiv (π'Gr 2 (S₊∙ 2)) ℤGroup
π₃S²≅ℤ =
  compGroupEquiv
    (invGroupEquiv
      (compGroupEquiv (πS³≅πTotalHopf 2) π'₃S²≅π'₃TotalHopf))
    (GroupIso→GroupEquiv (πₙ'Sⁿ≅ℤ 2))

-- We prove that the generator is the Hopf map
π₃TotalHopf-gen' : π' 3 (Σ (Susp S¹) S¹Hopf , north , base)
π₃TotalHopf-gen' =
  ∣ inv (compIso (hopfS¹.IsoTotalSpaceJoin) (IsoSphereJoin 1 1)) , refl ∣₂

πS³≅πTotalHopf-gen :
  fst (fst (πS³≅πTotalHopf 2)) ∣ idfun∙ _ ∣₂ ≡ π₃TotalHopf-gen'
πS³≅πTotalHopf-gen =
  cong ∣_∣₂
    (∘∙-idʳ (inv (compIso (hopfS¹.IsoTotalSpaceJoin)
                 (IsoSphereJoin 1 1)) , refl))

πTotalHopf-gen :
  gen₁-by (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base))
    ∣ inv (compIso (hopfS¹.IsoTotalSpaceJoin) (IsoSphereJoin 1 1)) , refl ∣₂
πTotalHopf-gen =
  subst (gen₁-by (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base)))
        πS³≅πTotalHopf-gen
        (Iso-pres-gen₁ (π'Gr 2 (S₊∙ 3))
                       (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base))
                       ∣ idfun∙ _ ∣₂
                       (πₙ'Sⁿ-gen-by-idfun 2)
                       (GroupEquiv→GroupIso (πS³≅πTotalHopf 2)))

πTotalHopf≅πS²-gen :
    fst (fst π'₃S²≅π'₃TotalHopf)
      π₃TotalHopf-gen'
  ≡ ∣ HopfMap' , refl ∣₂
πTotalHopf≅πS²-gen =
  cong ∣_∣₂ (ΣPathP (refl , (sym (rUnit refl))))

π₂S³-gen-by-HopfMap' : gen₁-by (π'Gr 2 (S₊∙ 2)) ∣ HopfMap' , refl ∣₂
π₂S³-gen-by-HopfMap' =
  subst (gen₁-by (π'Gr 2 (S₊∙ 2)))  πTotalHopf≅πS²-gen
    (Iso-pres-gen₁ (π'Gr 2 (Σ (S₊ 2) S¹Hopf , north , base)) (π'Gr 2 (S₊∙ 2))
      ∣ inv (compIso (hopfS¹.IsoTotalSpaceJoin) (IsoSphereJoin 1 1)) , refl ∣₂
      πTotalHopf-gen
      (GroupEquiv→GroupIso π'₃S²≅π'₃TotalHopf))

π₂S³-gen-by-HopfMap : gen₁-by (π'Gr 2 (S₊∙ 2)) ∣ HopfMap ∣₂
π₂S³-gen-by-HopfMap =
  subst (gen₁-by (π'Gr 2 (S₊∙ 2)))
        (cong ∣_∣₂ (sym hopfMap≡HopfMap'))
        π₂S³-gen-by-HopfMap'

-- As a consequence, we also get that the Hopf invariant determines
-- an iso π₃S²≅ℤ
hopfInvariantEquiv : GroupEquiv (π'Gr 2 (S₊∙ 2)) ℤGroup
fst (fst hopfInvariantEquiv) = HopfInvariant-π' 0
snd (fst hopfInvariantEquiv) =
  GroupEquivℤ-isEquiv (invGroupEquiv π₃S²≅ℤ) ∣ HopfMap ∣₂
                      π₂S³-gen-by-HopfMap (GroupHom-HopfInvariant-π' 0)
                      (abs→⊎ _ _ HopfInvariant-HopfMap)
snd hopfInvariantEquiv = snd (GroupHom-HopfInvariant-π' 0)