homotopy.EilenbergMacLane

{-# OPTIONS --without-K --rewriting --overlapping-instances --confluence-check --instance-search-depth=3 #-}

open import HoTT
open import homotopy.HSpace renaming (HSpaceStructure to HSS)
open import homotopy.Freudenthal
open import homotopy.IterSuspensionStable
import homotopy.Pi2HSusp as Pi2HSusp
open import homotopy.EM1HSpace
open import homotopy.EilenbergMacLane1
open import lib.types.Torsor
open import torsors.Delooping

module homotopy.EilenbergMacLane where

-- EM(G,n) when G is π₁(A,a₀)
module EMImplicit {i} {X : Ptd i} {{_ : is-connected 0 (de⊙ X)}}
  {{X-level : has-level 1 (de⊙ X)}} (H-X : HSS X) where

  private
    A = de⊙ X
    a₀ = pt X

  ⊙EM : (n : ℕ) → Ptd i
  ⊙EM O = ⊙Ω X
  ⊙EM (S n) = ⊙Trunc ⟨ S n ⟩ (⊙Susp^ n X)

  module _ (n : ℕ) where
    EM = de⊙ (⊙EM n)
    ptEM = pt (⊙EM n)

  EM-level : (n : ℕ) → has-level ⟨ n ⟩ (EM n)
  EM-level O = has-level-apply X-level _ _
  EM-level (S n) = Trunc-level

  instance
    EM-conn : {n : ℕ} → is-connected ⟨ n ⟩ (EM (S n))
    EM-conn {n} = Trunc-preserves-conn (⊙Susp^-conn' n)

  {-
  π (S k) (EM (S n)) (embase (S n)) == π k (EM n) (embase n)
  where k > 0 and n = S (S n')
  -}
  module Stable (k n : ℕ) (indexing : S k ≤ S (S n))
    where

    private
      SSn : ℕ
      SSn = S (S n)

      lte : ⟨ S k ⟩ ≤T ⟨ SSn ⟩
      lte = ⟨⟩-monotone-≤ $ indexing

      Skle : S k ≤ (S n) *2
      Skle = ≤-trans indexing (lemma n)
        where lemma : (n' : ℕ) → S (S n') ≤ (S n') *2
              lemma O = inl idp
              lemma (S n') = ≤-trans (≤-ap-S (lemma n')) (inr ltS)

    private
      module SS = Susp^StableSucc k (S n) Skle (⊙Susp^ (S n) X) {{⊙Susp^-conn' (S n)}}

    abstract
      stable : πS (S k) (⊙EM (S SSn)) ≃ᴳ πS k (⊙EM SSn)
      stable =
        πS (S k) (⊙EM (S SSn))
          ≃ᴳ⟨ πS-Trunc-fuse-≤-iso _ _ _ (≤T-ap-S lte) ⟩
        πS (S k) (⊙Susp^ SSn X)
          ≃ᴳ⟨ SS.stable ⟩
        πS k (⊙Susp^ (S n) X)
          ≃ᴳ⟨ πS-Trunc-fuse-≤-iso _ _ _ lte ⁻¹ᴳ ⟩
        πS k (⊙EM SSn)
          ≃ᴳ∎

  module BelowDiagonal where

    π₁ : (n : ℕ) → πS 0 (⊙EM (S (S n))) ≃ᴳ 0ᴳ
    π₁ n =
      contr-iso-0ᴳ (πS 0 (⊙EM (S (S n))))
        (connected-at-level-is-contr
          {{raise-level-≤T (≤T-ap-S (≤T-ap-S (-2≤T ⟨ n ⟩₋₂)))
                          (Trunc-level {n = 0})}})

    -- some clutter here arises from the definition of <;
    -- any simple way to avoid this?
    πS-below : (k n : ℕ) → (S k < n)
      → πS k (⊙EM n) ≃ᴳ 0ᴳ
    πS-below 0 .2 ltS = π₁ 0
    πS-below 0 .3 (ltSR ltS) = π₁ 1
    πS-below 0 (S (S n)) (ltSR (ltSR _)) = π₁ n
    πS-below (S k) ._ ltS =
      πS-below k _ ltS
      ∘eᴳ Stable.stable k k (inr ltS)
    πS-below (S k) ._ (ltSR ltS) =
      πS-below k _ (ltSR ltS)
      ∘eᴳ Stable.stable k (S k) (inr (ltSR ltS))
    πS-below (S k) ._ (ltSR (ltSR ltS)) =
      πS-below k _ (ltSR (ltSR ltS))
      ∘eᴳ Stable.stable k (S (S k)) (inr (ltSR (ltSR ltS)))
    πS-below (S k) (S (S (S n))) (ltSR (ltSR (ltSR lt))) =
      πS-below k _ (<-cancel-S (ltSR (ltSR (ltSR lt))))
      ∘eᴳ Stable.stable k n (inr (<-cancel-S (ltSR (ltSR (ltSR lt)))))


  module OnDiagonal where

    π₁ : πS 0 (⊙EM 1) ≃ᴳ πS 0 X
    π₁ = πS-Trunc-fuse-≤-iso 0 1 X ≤T-refl

    private
      module Π₂ = Pi2HSusp H-X

    π₂ : πS 1 (⊙EM 2) ≃ᴳ πS 0 X
    π₂ = Π₂.π₂-Susp
     ∘eᴳ πS-Trunc-fuse-≤-iso 1 2 (⊙Susp X) ≤T-refl

    πS-diag : (n : ℕ) → πS n (⊙EM (S n)) ≃ᴳ πS 0 X
    πS-diag 0 = π₁
    πS-diag 1 = π₂
    πS-diag (S (S n)) = πS-diag (S n)
                    ∘eᴳ Stable.stable (S n) n ≤-refl

  module AboveDiagonal where

    πS-above : ∀ (k n : ℕ) → (n < S k)
      → πS k (⊙EM n) ≃ᴳ 0ᴳ
    πS-above k n lt =
      contr-iso-0ᴳ (πS k (⊙EM n))
        (inhab-prop-is-contr
          [ idp^ (S k) ]
          {{Trunc-preserves-level 0 (Ω^-level -1 (S k) _
            (raise-level-≤T (lemma lt) (EM-level n)))}})
      where lemma : {k n : ℕ} → n < k → ⟨ n ⟩ ≤T (⟨ k ⟩₋₂ +2+ -1)
            lemma ltS = inl (! (+2+-comm _ -1))
            lemma (ltSR lt) = ≤T-trans (lemma lt) (inr ltS)

  module Spectrum where

    private
      module Π₂ = Pi2HSusp H-X

    spectrum0 : ⊙Ω (⊙EM 1) ⊙≃ ⊙EM 0
    spectrum0 = ⊙unTrunc-equiv (⊙Ω X) ⊙∘e ⊙Ω-Trunc-[_]-≃ X

    spectrum0-pres-comp : preserves-comp Ω-∙ Ω-∙ (fst (⊙–> spectrum0))
    spectrum0-pres-comp = =ₜ-equiv-ind (Trunc-elim {{Π-level λ _ → ⟨⟩}} λ p →
      =ₜ-equiv-ind (Trunc-elim λ q →
        ! (ap2 (λ t₁ t₂ → Trunc-elim (λ x → x) t₁ ∙ Trunc-elim (λ x → x) t₂)
            (<–-inv-r (=ₜ-equiv [ pt X ] [ pt X ]) [ p ]) (<–-inv-r (=ₜ-equiv [ pt X ] [ pt X ]) [ q ]) ∙
        ! (ap (Trunc-elim (λ x → x))
            (ap (=ₜ-maps.to [ pt X ] [ pt X ] [ pt X ] [ pt X ]) (∙-ap [_] p q) ∙ <–-inv-r (=ₜ-equiv _ _) [ p ∙ q ])))))
    
    spectrum1 : ⊙Ω (⊙EM 2) ⊙≃ ⊙EM 1
    spectrum1 = Π₂.⊙eq ⊙∘e ⊙Ω-Trunc-[ ⊙Susp X ]-≃

    private
      instance
        sconn : {n : ℕ} → is-connected ⟨ S n ⟩ (de⊙ (⊙Susp^ (S n) X))
        sconn {n} = ⊙Susp^-conn' (S n)

      kle : (n : ℕ) → ⟨ S (S n) ⟩ ≤T ⟨ n ⟩ +2+ ⟨ n ⟩
      kle O = inl idp
      kle (S n) = ≤T-trans (≤T-ap-S (kle n))
                   (≤T-trans (inl (! (+2+-βr ⟨ n ⟩ ⟨ n ⟩)))
                               (inr ltS))

    module FS (n : ℕ) =
      FreudenthalEquiv ⟨ n ⟩₋₁ ⟨ S (S n) ⟩ (kle n)
        (⊙Susp^ (S n) X)

    spectrumSS : (n : ℕ)
      → ⊙Ω (⊙EM (S (S (S n)))) ⊙≃ ⊙EM (S (S n))
    spectrumSS n = FS.⊙eq n ⊙⁻¹ ⊙∘e ⊙Ω-Trunc-[_]-≃ (⊙Susp^ (S (S n)) X)

    spectrum : (n : ℕ) → ⊙Ω (⊙EM (S n)) ⊙≃ ⊙EM n
    spectrum 0 = spectrum0
    spectrum 1 = spectrum1
    spectrum (S (S n)) = spectrumSS n

module EMExplicit {i} (G : AbGroup i) where
  module HSpace = EM₁HSpace G
  
  open EMImplicit {{⟨⟩}} {{EM₁-level₁ (fst G)}} HSpace.H-⊙EM₁ public
  open AbGroup G

  open BelowDiagonal public using (πS-below)

  πS-diag : (n : ℕ) → πS n (⊙EM (S n)) ≃ᴳ grp
  πS-diag n = π₁-EM₁ grp ∘eᴳ OnDiagonal.πS-diag n

  open AboveDiagonal public using (πS-above)
  open Spectrum public using (spectrum)

  deloop'-fold : (n : ℕ) → ⊙Ω^' n (⊙EM n) ⊙≃ ⊙El
  deloop'-fold O = ⊙f-equiv where open GroupIso (Ω¹-EM₁ grp)
  deloop'-fold (S n) = deloop'-fold n ⊙∘e ⊙Ω^'-emap n (spectrum n)

  deloop'-fold-pres-comp : (n : ℕ) → preserves-comp (Ω^'S-∙ n) comp (fst (⊙–> (deloop'-fold (S n))))
  deloop'-fold-pres-comp O g₁ g₂ = ap f (Spectrum.spectrum0-pres-comp g₁ g₂) ∙ pres-comp _ _ where open GroupIso (Ω¹-EM₁ grp)
  deloop'-fold-pres-comp (S n) g₁ g₂ =
    ap (fst (⊙–> (deloop'-fold (S n)))) (Ω^'S-fmap-∙ n (⊙–> (spectrum (S n))) g₁ g₂) ∙ deloop'-fold-pres-comp n _ _

  instance
    EM-SS-+2+ : {n : ℕ} → has-level (S (S (⟨ n ⟩₋₂ +2+ S (S ⟨ n ⟩₋₂)))) (EM (S (S n)))
    EM-SS-+2+ {n} =
      transport! (λ l → has-level l (EM (S (S n)))) (+2+-βr (S (S (⟨ n ⟩₋₂))) (S ⟨ n ⟩₋₂) ∙ +2+-βr (S (S (S (⟨ n ⟩₋₂)))) ⟨ n ⟩₋₂) aux
      where abstract
        aux : ∀ {n} → has-level (S (S (S (S (⟨ n ⟩₋₂ +2+ ⟨ n ⟩₋₂))))) (EM (S (S n)))
        aux {n} = raise-level-≤T aux2 (EM-level (S (S n))) where
          aux2 : ∀ {n} → ⟨ S (S n) ⟩ ≤T S (S (S (S (⟨ n ⟩₋₂ +2+ ⟨ n ⟩₋₂))))
          aux2 {O} = inl idp
          aux2 {S n} = transport! (λ l → ⟨ S (S (S n)) ⟩ ≤T l) (+2+-βr (S (S (S (S (S (⟨ n ⟩₋₂)))))) ⟨ n ⟩₋₂)
            (≤T-trans (≤T-ap-S (aux2 {n})) (inr ltS))

  -- If n > 1, then K(G , (S n)) is equivalent to the type of torsors over K(G , n).
  ⊙EM-Torsors-≃ : {n : ℕ} → ⊙EM (S (S (S n))) ⊙≃ ⊙Torsors {j = i} (⊙EM (S (S n)))
  ⊙EM-Torsors-≃ {n} = ⊙tors-uniq-map-≃ (⊙EM (S (S n)))
    {{PtdTorsors-contr {{EM-conn}}}}
    {{connected-≤T (inr (<T-ap-S (<T-ap-S (-2<T _)))) {{EM-conn}}}}
    (spectrum (S (S n)) ⊙⁻¹)

  EM-Torsors-≃ : {n : ℕ} → EM (S (S (S n))) ≃ Torsors i (⊙EM (S (S n)))
  EM-Torsors-≃ = ⊙≃-to-≃ ⊙EM-Torsors-≃

-- making instance argument available for instance search
module _ {i} {G : AbGroup i} where

  open EMExplicit G renaming (EM-SS-+2+ to EM-SS-+2+-exp)
  
  instance
    EM-SS-+2+ : {n : ℕ} → has-level (S (S (⟨ n ⟩₋₂ +2+ S (S ⟨ n ⟩₋₂)))) (EM (S (S n)))
    EM-SS-+2+ = EM-SS-+2+-exp 

module _ {i j} {G : Group i} {H : Group j} (φ : G →ᴳ H) where

  private
    module φ = GroupHom φ

    EM₁-fmap-hom : G →ᴳ Ω^S-group 0 (⊙EM₁ H) {{EM₁-level₁ H}}
    EM₁-fmap-hom = group-hom f f-preserves-comp
      where
        f : Group.El G → embase' H == embase
        f g = emloop (φ.f g)
        f-preserves-comp : ∀ g₁ g₂ → f (Group.comp G g₁ g₂) == f g₁ ∙ f g₂
        f-preserves-comp g₁ g₂ =
          emloop (φ.f (Group.comp G g₁ g₂))
            =⟨ ap emloop (φ.pres-comp g₁ g₂) ⟩
          emloop (Group.comp H (φ.f g₁) (φ.f g₂))
            =⟨ emloop-comp' H (φ.f g₁) (φ.f g₂) ⟩
          emloop (φ.f g₁) ∙ emloop (φ.f g₂) =∎

    module EM₁FmapRec =
      EM₁Level₁Rec {G = G} {C = EM₁ H}
                  {{EM₁-level₁ H {⟨-2⟩}}}
                  embase
                  EM₁-fmap-hom

  abstract
    EM₁-fmap : EM₁ G → EM₁ H
    EM₁-fmap = EM₁FmapRec.f

    EM₁-fmap-embase-β : EM₁-fmap embase ↦ embase
    EM₁-fmap-embase-β = EM₁FmapRec.embase-β
    {-# REWRITE EM₁-fmap-embase-β #-}

    EM₁-fmap-emloop-β : ∀ g → ap EM₁-fmap (emloop g) == emloop (φ.f g)
    EM₁-fmap-emloop-β = EM₁FmapRec.emloop-β

  ⊙EM₁-fmap : ⊙EM₁ G ⊙→ ⊙EM₁ H
  ⊙EM₁-fmap = EM₁-fmap , idp

module _ {i j} {G : AbGroup i} {H : AbGroup j} (φ : AbGroup.grp G →ᴳ AbGroup.grp H) where

  ⊙EM-fmap : ∀ n → EMExplicit.⊙EM G n ⊙→ EMExplicit.⊙EM H n
  ⊙EM-fmap O = ⊙Ω-fmap (⊙EM₁-fmap φ)
  ⊙EM-fmap (S n) = ⊙Trunc-fmap (⊙Susp^-fmap n (⊙EM₁-fmap φ))

  EM-fmap : ∀ n → EMExplicit.EM G n → EMExplicit.EM H n
  EM-fmap n = fst (⊙EM-fmap n)