Theory of Symmetric Groups

Cubical/Algebra/SymmetricGroup.agda

@@ -4,23 +4,87 @@ module Cubical.Algebra.SymmetricGroup where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Structure
 open import Cubical.Data.Sigma
-open import Cubical.Data.Nat using (ℕ ; suc ; zero)
-open import Cubical.Data.Fin using (Fin ; isSetFin)
-open import Cubical.Data.Empty
-open import Cubical.Relation.Nullary using (¬_)
+open import Cubical.Data.Nat
+open import Cubical.Data.SumFin
+open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Bool
+open import Cubical.Data.Unit
 
 open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Bool
+open import Cubical.Algebra.Group.Instances.Unit
 
-private
-  variable
-    ℓ : Level
+private variable
+  ℓ ℓ' : Level
+  X Y : Type ℓ
 
-Symmetric-Group : (X : Type ℓ) → isSet X → Group ℓ
-Symmetric-Group X isSetX = makeGroup (idEquiv X) compEquiv invEquiv (isOfHLevel≃ 2 isSetX isSetX)
-  compEquiv-assoc compEquivEquivId compEquivIdEquiv invEquiv-is-rinv invEquiv-is-linv
+SymGroup : (X : Type ℓ) → isSet X → Group ℓ
+SymGroup X isSetX = makeGroup {G = X ≃ X} (idEquiv X) compEquiv invEquiv
+  (isOfHLevel≃ 2 isSetX isSetX)
+  compEquiv-assoc
+  compEquivEquivId
+  compEquivIdEquiv
+  invEquiv-is-rinv
+  invEquiv-is-linv
 
--- Finite symmetrics groups
+FinSymGroup : ℕ → Group₀
+FinSymGroup n = SymGroup (Fin n) isSetFin
 
-Sym : ℕ → Group _
-Sym n = Symmetric-Group (Fin n) isSetFin
+Sym0≃1 : GroupEquiv (FinSymGroup 0) UnitGroup₀
+Sym0≃1 = contrGroupEquivUnit $ inhProp→isContr (idEquiv _) $ isOfHLevel≃ 1 isProp⊥ isProp⊥
+
+Sym0≡1 : FinSymGroup 0 ≡ UnitGroup₀
+Sym0≡1 = uaGroup Sym0≃1
+
+Sym1≃1 : GroupEquiv (FinSymGroup 1) UnitGroup₀
+Sym1≃1 = contrGroupEquivUnit $ isOfHLevel≃ 0 isContrSumFin1 isContrSumFin1
+
+Sym1≡1 : FinSymGroup 1 ≡ UnitGroup₀
+Sym1≡1 = uaGroup Sym1≃1
+
+Sym2≃Bool : GroupEquiv (FinSymGroup 2) BoolGroup
+Sym2≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
+  Fin 2 ≃ Fin 2 Iso⟨ equivCompIso SumFin2≃Bool SumFin2≃Bool ⟩
+  Bool ≃ Bool   Iso⟨ invIso univalenceIso ⟩
+  Bool ≡ Bool   Iso⟨ invIso reflectIso ⟩
+  Bool          ∎Iso
+  where open BoolReflection
+
+Sym2≡Bool : FinSymGroup 2 ≡ BoolGroup
+Sym2≡Bool = uaGroup Sym2≃Bool
+
+SymUnit≃Unit : GroupEquiv (SymGroup Unit isSetUnit) UnitGroup₀
+SymUnit≃Unit = contrGroupEquivUnit $ isOfHLevel≃ 0 isContrUnit isContrUnit
+
+SymUnit≡Unit : SymGroup Unit isSetUnit ≡ UnitGroup₀
+SymUnit≡Unit = uaGroup SymUnit≃Unit
+
+SymBool≃Bool : GroupEquiv (SymGroup Bool isSetBool) BoolGroup
+SymBool≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
+  Bool ≃ Bool Iso⟨ invIso univalenceIso ⟩
+  Bool ≡ Bool Iso⟨ invIso reflectIso ⟩
+  Bool        ∎Iso
+  where open BoolReflection
+
+SymBool≡Bool : SymGroup Bool isSetBool ≡ BoolGroup
+SymBool≡Bool = uaGroup SymBool≃Bool
+
+module _ (n : ℕ) where
+
+  ⟨Sym⟩≃factorial : ⟨ FinSymGroup n ⟩ ≃ Fin (n !)
+  ⟨Sym⟩≃factorial = SumFin≃≃ n
+
+  ⟨Sym⟩≡factorial : ⟨ FinSymGroup n ⟩ ≡ Fin (n !)
+  ⟨Sym⟩≡factorial = ua ⟨Sym⟩≃factorial
+
+Sym-cong-≃ : ∀ isSetX isSetY → X ≃ Y → GroupEquiv (SymGroup X isSetX) (SymGroup Y isSetY)
+Sym-cong-≃ isSetX isSetY e .fst = equivComp e e
+Sym-cong-≃ isSetX isSetY e .snd = makeIsGroupHom λ g h → sym $ equivEq $ funExt λ x → cong (e .fst ∘ h .fst) (retEq e _)