{-

This file contains:
    - the abelianization of groups as a HIT as proposed in https://arxiv.org/abs/2007.05833

The definition of the abelianization is not as a set-quotient, since the relation of
abelianization is cumbersome to work with.

-}
module Cubical.Algebra.Group.Abelianization.Properties where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Equiv

open import Cubical.Data.Sigma

open import Cubical.Algebra.Group.Base
open import Cubical.Algebra.Group.Properties
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
  using (isPropIsGroupHom; compGroupHom; idGroupHom
       ; makeIsGroupHom ; GroupEquiv→GroupHom ; invGroupEquiv)
open import Cubical.Algebra.Monoid.Base
open import Cubical.Algebra.Semigroup
open import Cubical.Algebra.AbGroup.Base

open import Cubical.Algebra.Group.Abelianization.Base

private
  variable
    ℓ ℓ' : Level

module _ (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  private
    instance
      _ = snd G

  -- Some helpful lemmas, similar to those in Cubical/HITs/SetQuotients/Properties.agda
  elimProp : {B : Abelianization G → Type ℓ'}
        → (Bprop : (x : Abelianization G) → isProp (B x))
        → (f : (g : fst G) → B (η g))
        → (x : Abelianization G)
        → B x
  elimProp Bprop f (η g) = f g
  elimProp {B = B} Bprop f (comm a b c i) =
    isProp→PathP (λ i → Bprop (comm a b c i)) (f (a · (b · c))) (f (a · (c · b))) i
  elimProp Bprop f (isset x y p q i j) =
    isOfHLevel→isOfHLevelDep
       (λ x → isProp→isSet (Bprop x)) (g x) (g y) (cong g p) (cong g q) (isset x y p q) i j
    where
    g = elimProp Bprop f

  elimProp2 : {C : Abelianization G → Abelianization G → Type ℓ'}
        → (Cprop : (x y : Abelianization G) → isProp (C x y))
        → (f : (a b : fst G) → C (η a) (η b))
        → (x y : Abelianization G)
        → C x y
  elimProp2 Cprop f = elimProp (λ x → isPropΠ (λ y → Cprop x y))
                               (λ x → elimProp (λ y → Cprop (η x) y) (f x))

  elimProp3 : {D : Abelianization G → Abelianization G → Abelianization G → Type ℓ'}
        → (Dprop : (x y z : Abelianization G) → isProp (D x y z))
        → ((a b c : fst G) → D (η a) (η b) (η c))
        → (x y z : Abelianization G)
        → D x y z
  elimProp3 Dprop f = elimProp (λ x → isPropΠ2 (λ y z → Dprop x y z))
                               (λ x → elimProp2 (λ y z → Dprop (η x) y z) (f x))

  elimContr : {B : Abelianization G → Type ℓ'}
        → (Bcontr : ∀ (a : fst G) → isContr (B (η a)))
        → (x : Abelianization G)
        → B x
  elimContr Bcontr = elimProp (elimProp (λ _ → isPropIsProp) λ _ → isContr→isProp (Bcontr _))
                              λ _ → Bcontr _ .fst

  elimContr2 : {C : Abelianization G → Abelianization G → Type ℓ'}
        → (Ccontr : ∀ (a b : fst G) → isContr (C (η a) (η b)))
        → (x y : Abelianization G)
        → C x y
  elimContr2 Ccontr = elimContr λ _ → isOfHLevelΠ 
                     (elimContr λ _ → inhProp→isContr (Ccontr _ _) isPropIsContr)

  rec : {M : Type ℓ'}
        (Mset : isSet M)
        (f : fst G → M)
        (fcomm : (a b c : fst G) → f (a · (b · c)) ≡ f (a · (c · b)))
      → Abelianization G → M
  rec Mset f fcomm (η g) = f g
  rec Mset f fcomm (comm a b c i) = fcomm a b c i
  rec Mset f fcomm (isset a b p q i j) = Mset (g a) (g b) (cong g p) (cong g q) i j
    where
    g = rec Mset f fcomm

  rec2 : {M : Type ℓ'}
        (Mset : isSet M)
        (f : fst G → fst G → M)
        (fcomml : (a b c d : fst G) → f (a · (b · c)) d ≡ f (a · (c · b)) d)
        (fcommr : (a b c d : fst G) → f a (b · (c · d)) ≡ f a (b · (d · c)))
      → Abelianization G → Abelianization G → M
  rec2 Mset f fcomml fcommr =
    rec
      (isSetΠ (λ _ → Mset))
      (λ g → rec Mset (λ h → f g h) (fcommr g))
      (λ a b c → funExt (elimProp (λ _ → Mset _ _) (λ d → fcomml a b c d)))

module AbelianizationGroupStructure (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  private
    instance
      _ = snd G

  {-
    Definition of the group structure on the abelianization. Here the generality of the comm
    relation is used.
  -}
  _·Ab_ : Abelianization G → Abelianization G → Abelianization G
  _·Ab_ =
    (rec2 G)
      isset
      (λ x y → η (x · y))
      (λ a b c d → η ((a · (b · c)) · d) ≡⟨ cong η (cong (λ x → (x · d)) (·Assoc _ _ _)) ⟩
                   η (((a · b) · c) · d) ≡⟨ cong η (sym (·Assoc (a · b) c d)) ⟩
                   η ((a · b) · (c · d)) ≡⟨ comm (a · b) c d ⟩
                   η ((a · b) · (d · c)) ≡⟨ cong η (sym (·Assoc _ _ _)) ⟩
                   η (a · (b · (d · c))) ≡⟨ cong η (cong (λ x → (a · x)) (·Assoc _ _ _)) ⟩
                   η (a · ((b · d) · c)) ≡⟨ comm a (b · d) c ⟩
                   η (a · (c · (b · d))) ≡⟨ cong η (cong (λ x → (a · x)) (·Assoc _ _ _)) ⟩
                   η (a · ((c · b) · d)) ≡⟨ cong η (·Assoc a (c · b) d) ⟩
                   η ((a · (c · b)) · d) ∎)
      (λ a b c d → η (a · (b · (c · d))) ≡⟨ cong η (·Assoc _ _ _) ⟩
                   η ((a · b) · (c · d)) ≡⟨ comm (a · b) c d ⟩
                   η ((a · b) · (d · c)) ≡⟨ cong η (sym (·Assoc _ _ _)) ⟩
                   η (a · (b · (d · c))) ∎)

  1Ab : Abelianization G
  1Ab = η 1g

  invAb : Abelianization G → Abelianization G
  invAb =
    (rec G)
      isset
      ((λ x → η (inv x)))
      (λ a b c → η (inv (a · (b · c)))         ≡⟨ cong η (invDistr a (b · c)) ⟩
      η ((inv (b · c)) · (inv a))              ≡⟨ cong (λ x → η (x · (inv a))) (invDistr b c) ⟩
      η (((inv c) · (inv b)) · (inv a))        ≡⟨ cong
                                                    η
                                                    ((sym (·IdL (((inv c) · (inv b)) · (inv a))))) ⟩
      η (1g · (((inv c) · (inv b)) · (inv a))) ≡⟨ comm 1g ((inv c) · (inv b)) (inv a) ⟩
      η (1g · ((inv a) · ((inv c) · (inv b)))) ≡⟨ cong η (·IdL ((inv a) · ((inv c) · (inv b)))) ⟩
      η ((inv a) · ((inv c) · (inv b)))        ≡⟨ comm (inv a) (inv c) (inv b) ⟩
      η ((inv a) · ((inv b) · (inv c)))        ≡⟨ cong
                                                    η
                                                    ((sym (·IdL ((inv a) · ((inv b) · (inv c)))))) ⟩
      η (1g · ((inv a) · ((inv b) · (inv c)))) ≡⟨ comm 1g (inv a) ((inv b) · (inv c)) ⟩
      η (1g · (((inv b) · (inv c)) · (inv a))) ≡⟨ cong η (·IdL (((inv b) · (inv c)) · (inv a))) ⟩
      η (((inv b) · (inv c)) · (inv a))        ≡⟨ cong
                                                    (λ x → η (x · (inv a)))
                                                    (sym (invDistr c b)) ⟩
      η ((inv (c · b)) · (inv a))              ≡⟨ cong η (sym (invDistr a (c · b))) ⟩
      η (inv (a · (c · b))) ∎)

  assocAb : (x y z : Abelianization G) → x ·Ab (y ·Ab z) ≡ (x ·Ab y) ·Ab z
  assocAb =
    (elimProp3 G)
      (λ x y z → isset (x ·Ab (y ·Ab z)) ((x ·Ab y) ·Ab z))
      (λ x y z → cong η (·Assoc x y z))

  ridAb : (x : Abelianization G) → x ·Ab 1Ab ≡ x
  ridAb =
    (elimProp G)
      (λ x → isset (x ·Ab 1Ab) x)
      (λ x → cong η (·IdR x))

  rinvAb : (x : Abelianization G) → x ·Ab (invAb x) ≡ 1Ab
  rinvAb =
    (elimProp G)
      (λ x → isset (x ·Ab (invAb x)) 1Ab)
      (λ x → (η x) ·Ab (invAb (η x)) ≡⟨ refl ⟩
             (η x) ·Ab (η (inv x))   ≡⟨ refl ⟩
             η (x · (inv x))         ≡⟨ cong η (·InvR x) ⟩
             η 1g                    ≡⟨ refl ⟩
             1Ab ∎)

  commAb : (x y : Abelianization G) → x ·Ab y ≡ y ·Ab x
  commAb =
    (elimProp2 G)
      (λ x y → isset (x ·Ab y) (y ·Ab x))
      (λ x y → (η x) ·Ab (η y)  ≡⟨ refl ⟩
               η (x · y)        ≡⟨ cong η (sym (·IdL (x · y))) ⟩
               η (1g · (x · y)) ≡⟨ comm 1g x y ⟩
               η (1g · (y · x)) ≡⟨ cong η (·IdL (y · x)) ⟩
               η (y · x)        ≡⟨ refl ⟩
               (η y) ·Ab (η x) ∎)

  open AbGroupStr
  open IsAbGroup
  open IsGroup
  open IsSemigroup
  open IsMonoid
  -- The proof that the abelianization is in fact an abelian group.
  asAbelianGroup : AbGroup ℓ
  fst asAbelianGroup = Abelianization G
  0g (snd asAbelianGroup) = 1Ab
  _+_ (snd asAbelianGroup) = _·Ab_
  - snd asAbelianGroup = invAb
  is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd asAbelianGroup))))) = isset
  ·Assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd asAbelianGroup))))) = assocAb
  ·IdR (isMonoid (isGroup (isAbGroup (snd asAbelianGroup)))) = ridAb
  ·IdL (isMonoid (isGroup (isAbGroup (snd asAbelianGroup)))) x = commAb 1Ab x ∙ ridAb x
  ·InvR (isGroup (isAbGroup (snd asAbelianGroup))) = rinvAb
  ·InvL (isGroup (isAbGroup (snd asAbelianGroup))) x = commAb (invAb x) x ∙ rinvAb x
  +Comm (isAbGroup (snd asAbelianGroup)) = commAb

  -- The proof that η can be seen as a group homomorphism
  ηAsGroupHom : GroupHom G (AbGroup→Group asAbelianGroup)
  ηAsGroupHom = f , fIsHom
    where
    f = λ x → η x
    fIsHom : IsGroupHom (snd G) f (snd (AbGroup→Group asAbelianGroup))
    IsGroupHom.pres· fIsHom = λ x y → refl
    IsGroupHom.pres1 fIsHom = refl
    IsGroupHom.presinv fIsHom = λ x → refl

AbelianizationAbGroup : (G : Group ℓ) → AbGroup ℓ
AbelianizationAbGroup G = AbelianizationGroupStructure.asAbelianGroup G

AbelianizationGroup : (G : Group ℓ) → Group ℓ
AbelianizationGroup G = AbGroup→Group (AbelianizationAbGroup G)

AbelianizationHom : (G : Group ℓ) → GroupHom G (AbGroup→Group (AbelianizationAbGroup G))
AbelianizationHom G = AbelianizationGroupStructure.ηAsGroupHom G

module UniversalProperty (G : Group ℓ) where
  open GroupStr {{...}}
  open GroupTheory G
  open AbelianizationGroupStructure G
  private
    instance
      _ = snd G

  {- The proof of the universal property of the abelianization.

  G --η--> abelianization
  \         .
    \       .
      f   ∃! inducedHom
        \   .
          \ .
            H
  commuting diagram
  -}
  inducedHom : (H : AbGroup ℓ)
             → (f : GroupHom G (AbGroup→Group H))
             → AbGroupHom asAbelianGroup H
  inducedHom H f = g , gIsHom
    where open IsGroupHom
          instance
            _ : GroupStr (fst H)
            _ = snd (AbGroup→Group H)
          f' : fst G → fst H
          f' = fst f
          g : Abelianization G → fst H
          g = (rec G)
                is-set
                (λ x → (f') x)
                (λ a b c → f' (a · b · c)           ≡⟨ (snd f).pres· a (b · c) ⟩
                           (f' a) · (f' (b · c))    ≡⟨ cong
                                                         (λ x → (f' a) · x)
                                                         ((snd f).pres· b c) ⟩
                           (f' a) · (f' b) · (f' c) ≡⟨ cong
                                                         (λ x → (f' a) · x)
                                                         ((snd H).AbGroupStr.+Comm (f' b) (f' c)) ⟩
                           (f' a) · (f' c) · (f' b) ≡⟨ cong
                                                         (λ x → (f' a) · x)
                                                         (sym ((snd f).pres· c b)) ⟩
                           (f' a) · (f' (c · b))    ≡⟨ sym ((snd f).pres· a (c · b)) ⟩
                           f' (a · c · b) ∎)
          gIsHom : IsGroupHom (snd (AbGroup→Group asAbelianGroup)) g (snd (AbGroup→Group H))
          pres· gIsHom =
            (elimProp2 G)
              (λ x y → is-set _ _)
              ((snd f).pres·)
          pres1 gIsHom = (snd f).pres1
          presinv gIsHom =
            (elimProp G)
              (λ x → is-set _ _)
              ((snd f).presinv)

  commutativity : (H : AbGroup ℓ)
                → (f : GroupHom G (AbGroup→Group H))
                → (compGroupHom ηAsGroupHom (inducedHom H f) ≡ f)
  commutativity H f =
      Σ≡Prop
        (λ _ → isPropIsGroupHom _ _)
        (λ i x → q x i)
    where q : (x : fst  G)
            → fst (compGroupHom ηAsGroupHom (inducedHom H f)) x ≡ fst f x
          q = (λ x → refl)

  uniqueness : (H : AbGroup ℓ)
             → (f : GroupHom G (AbGroup→Group H))
             → (g : AbGroupHom asAbelianGroup H)
             → (p : compGroupHom ηAsGroupHom g ≡ f)
             → (g ≡ inducedHom H f)
  uniqueness H f g p =
      Σ≡Prop
        (λ _ → isPropIsGroupHom _ _)
        (λ i x →  q x i)
    where
    module H = AbGroupStr (str H)
    q : (x : Abelianization G) → fst g x ≡ fst (inducedHom H f) x
    q = (elimProp G)
          (λ _ → H.is-set _ _)
          (λ x → fst g (η x) ≡⟨ cong (λ f → f x) (cong fst p) ⟩
                 (fst f) x   ≡⟨ refl ⟩
                 fst (inducedHom H f) (η x)∎)


module _ {ℓ} {G : Group ℓ} (H : AbGroup ℓ) (ϕ : GroupHom G (AbGroup→Group H)) where
  fromAbelianization : AbGroupHom (AbelianizationAbGroup G) H
  fst fromAbelianization = rec G (AbGroupStr.is-set (snd H)) (fst ϕ)
    λ x y z → IsGroupHom.pres· (snd ϕ) _ _
            ∙ cong₂ (AbGroupStr._+_ (snd H)) refl
                (IsGroupHom.pres· (snd ϕ) _ _
                ∙ AbGroupStr.+Comm (snd H) _ _
                ∙ sym (IsGroupHom.pres· (snd ϕ) _ _))
            ∙ sym (IsGroupHom.pres· (snd ϕ) _ _)
  snd fromAbelianization =
    makeIsGroupHom (elimProp2 _
      (λ _ _ → AbGroupStr.is-set (snd H) _ _)
      λ x y → IsGroupHom.pres· (snd ϕ) x y)

AbelianizationFun : ∀ {ℓ} {G : Group ℓ} {H : Group ℓ}
  → GroupHom G H → AbGroupHom (AbelianizationAbGroup G) (AbelianizationAbGroup H)
fst (AbelianizationFun {G = G} {H} ϕ) = rec _ isset (λ x → η (fst ϕ x)) λ a b c
  → cong η (IsGroupHom.pres· (snd ϕ) a _
         ∙ cong₂ (GroupStr._·_ (snd H)) refl (IsGroupHom.pres· (snd ϕ) b c))
  ∙ comm _ _ _
  ∙ sym (cong η (IsGroupHom.pres· (snd ϕ) a _
         ∙ cong₂ (GroupStr._·_ (snd H)) refl (IsGroupHom.pres· (snd ϕ) c b)))
snd (AbelianizationFun {G = G} {H} ϕ) = makeIsGroupHom
  (elimProp2 _ (λ _ _ → isset _ _)
    λ a b → cong η (IsGroupHom.pres· (snd ϕ) a b))

AbelianizationEquiv : ∀ {ℓ} {G : Group ℓ} {H : Group ℓ}
  → GroupEquiv G H
  → AbGroupEquiv (AbelianizationAbGroup G) (AbelianizationAbGroup H)
fst (AbelianizationEquiv {G = G} {H} ϕ) = isoToEquiv main
  where
  main : Iso _ _
  Iso.fun main = fst (AbelianizationFun (GroupEquiv→GroupHom ϕ))
  Iso.inv main = fst (AbelianizationFun (GroupEquiv→GroupHom (invGroupEquiv ϕ)))
  Iso.rightInv main =
    elimProp _ (λ _ → isset _ _) λ g → cong η (secEq (fst ϕ) g)
  Iso.leftInv main =
    elimProp _ (λ _ → isset _ _) λ g → cong η (retEq (fst ϕ) g)
snd (AbelianizationEquiv {G = G} {H} ϕ) =
  snd (AbelianizationFun (fst (fst ϕ) , snd ϕ))

AbelianizationIdempotent : ∀ {ℓ} (G : AbGroup ℓ)
  → AbGroupIso G (AbelianizationAbGroup (AbGroup→Group G))
Iso.fun (fst (AbelianizationIdempotent G)) = η
Iso.inv (fst (AbelianizationIdempotent G)) =
  rec _ (AbGroupStr.is-set (snd G))
  (λ x → x)
  λ a b c → cong (AbGroupStr._+_ (snd G) a) (AbGroupStr.+Comm (snd G) _ _)
Iso.rightInv (fst (AbelianizationIdempotent G)) =
  elimProp _ (λ _ → isset _ _) (λ _ → refl)
Iso.leftInv (fst (AbelianizationIdempotent G)) x = refl
snd (AbelianizationIdempotent G) =
  snd (AbelianizationGroupStructure.ηAsGroupHom _)