module Group where

{-
This file contains the definitions of group and group action
along with some examples.
-}

open import Basics 
open import Atoms
open import Perms

--------------------------------------------------------------------------------------------------------------------------------
--Definition of Group
--------------------------------------------------------------------------------------------------------------------------------

record Group : Set₁ where
  field
    Gₛ : Set
    _≈ₛ_ : Rel Gₛ
    eq≈ₛ : isEquivalence Gₛ _≈ₛ_
    _∙_ : Op₂ Gₛ
    e     : Gₛ
    _⁻¹  : Op₁ Gₛ
    asso : assoc {Gₛ}{_∙_}{_≈ₛ_}
    id      : idax {Gₛ}{_∙_}{_⁻¹}{_≈ₛ_} e 
    cong∙ : _∙_ Preserves₂ _≈ₛ_ ⟶ _≈ₛ_ ⟶ _≈ₛ_
    cong⁻¹ : _⁻¹ Preserves _≈ₛ_ ⟶ _≈ₛ_

open Group public

-------------------------------------------------------------------------------------------------------------------------------
--Definition of group action
-------------------------------------------------------------------------------------------------------------------------------

record GAct (G : Group) : Set₁ where
 field
    AₛP : Set
    ≈ₐP : Rel AₛP
    eq≈ₐP : isEquivalence AₛP ≈ₐP
    ActP : (Gₛ G) → AₛP → AₛP
    resP : ActP Preserves₂ (_≈ₛ_ G) ⟶ ≈ₐP ⟶ ≈ₐP
    p₁p₂↠P : p₁p₂Act {Gₛ G}{AₛP}{_∙_ G}{≈ₐP}{ActP}
    ι↠P : ιAct {Gₛ G}{AₛP}{≈ₐP}{ActP} (e G)

open GAct public

-----------------------------------------------------------------------------------------------------------------------------
--Perm is a group
-----------------------------------------------------------------------------------------------------------------------------

PermG : Group
PermG = record { Gₛ = Perm
                                   ; _≈ₛ_ = pEquiv
                                   ; eq≈ₛ = pEquiv≡
                                   ; _∙_ = _++_
                                   ; e = ι
                                   ; _⁻¹ = invPerm
                                   ; asso = PermAssoc≈
                                   ; id = λ p → (p⁻¹p≡ι p) , (pp⁻¹≡ι p)
                                   ; cong∙ = λ {p₁ p₂ q₁ q₂} →  cong++ {p₁} {p₂} {q₁} {q₂} 
                                   ; cong⁻¹ = λ {p q} → ( λ p≈q → p≈q⇒p⁻¹≈q⁻¹ p q p≈q)
                                  }

-----------------------------------------------------------------------------------------------------------------------------
--Permutation action on atoms is a group action
----------------------------------------------------------------------------------------------------------------------------

PermGA : GAct PermG
PermGA = record { AₛP = Atom
                              ; ≈ₐP = _≡_
                              ; eq≈ₐP = aEquiv≡ Atom
                              ; ActP = PermAct
                              ; resP = λ {p₁ p₂ a₁ a₂} p₁≈p₂ a₁≡a₂ → PermAct p₁ a₁ ≡< cong (λ w → PermAct p₁ w) a₁≡a₂ > (PermAct p₁ a₂ ≡< p₁≈p₂ {a₂} > ((PermAct p₂ a₂) ▪)) 
                              ; p₁p₂↠P = λ p₁ p₂ → (λ {x} → sym (p₁++p₂≡p₂p₁ {x} p₂ p₁))
                              ; ι↠P = λ {x} → refl
                              }

--------------------------------------------------------------------------------------------------------------------------
--Permutation action on itself (composition) is a group action
--------------------------------------------------------------------------------------------------------------------------

Perms : GAct PermG
Perms = record {AₛP = Perm
                           ; ≈ₐP = pEquiv
                           ; eq≈ₐP = pEquiv≡ 
                           ; ActP = λ π → λ σ → σ ++ π
                           ; resP = λ {p₁}{p₂}{q₁}{q₂} p₁≈p₂ q₁≈q₂ → cong++ {q₁}{q₂}{p₁}{p₂} q₁≈q₂ p₁≈p₂
                           ; p₁p₂↠P = λ p₁ p₂ {p₃} {x} → sym (cong (λ w → PermAct w x) (PermAssoc p₃ p₂ p₁))
                           ; ι↠P = λ {p} → ιp p
                           }

-----------------------------------------------------------------------------------------------------------------------------------
--Permutation action on itself (conjugation) is a group action
-----------------------------------------------------------------------------------------------------------------------------------

PermGP : GAct PermG
PermGP = record { AₛP = Perm
                              ; ≈ₐP = pEquiv
                              ; eq≈ₐP = pEquiv≡
                              ; ActP = PPAct
                              ; resP = λ {π₁ π₂ p₁ p₂} π₁≈π₂ p₁≈p₂ → resPP π₁ π₂ p₁ p₂ π₁≈π₂ p₁≈p₂
                              ; p₁p₂↠P = λ p₁ p₂ → (λ {p} → sym (p₁++p₂≡p₂p₁p p₂ p₁ p))
                              ; ι↠P = λ {p} → ιp p
                              }
----------------------------------------------------------------------------------------------