This file defines the notion of a representable element of the symmetric group. Representable elements should (and do) correspond to elements of the symmetric group in the image of the inclusion ⟨ 𝓖 ⟩ → SymGroup ⟨ 𝓖 ⟩. However they must be defined in a different way to preserve the strict associativity and unitality.
Module header
{-# OPTIONS --safe --cubical #-} open import Cubical.Algebra.Group module Groups.Symmetric.Representable {ℓ} (𝓖 : Group ℓ) where open import Cubical.Algebra.Group.GroupPath open import Cubical.Algebra.Group.Morphisms open import Cubical.Data.Sigma open import Cubical.Data.Vec open import Cubical.Foundations.Equiv open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Prelude open import Cubical.Foundations.SIP open import Cubical.Functions.FunExtEquiv open import Groups.Function.Inverse open import Groups.Symmetric open import Groups.Symmetric.Inclusion 𝓖 open GroupStr (𝓖 .snd) using (_·_;1g;inv;is-set) open GroupStr (SymGroup .snd) using () renaming (_·_ to _·′_; 1g to 1gs; inv to _⁻¹; is-set to is-set-sym) open GroupStr hiding (_·_;1g;inv;is-set)
We define Representable as follows. A similar trick to the one used for inverses is used to ensure strict associativity and unitality is maintained. Without this trick the definition says that a function f is representable if f (g + h) ≡ f g + h for all g h ∈ ⟨ 𝓖 ⟩.
Representable : (f : ⟨ 𝓖 ⟩ → ⟨ 𝓖 ⟩) → Type ℓ Representable f = ∀ x g h → x ≡ g · h → f x ≡ f g · h Repr : Type ℓ Repr = Σ[ f ∈ ⟨ SymGroup ⟩ ] Representable (fst f) × Representable (fst (snd f))
Representable is a Prop and so Repr is a set.
rep-prop : (f : ⟨ 𝓖 ⟩ → ⟨ 𝓖 ⟩) → isProp (Representable f) rep-prop f = isPropΠ2 (λ x y → isPropΠ2 λ w z → (is-set (f x) (f y · w))) repΣ-set : isSet Repr repΣ-set = isSetΣ is-set-sym λ f → isProp→isSet (isProp× (rep-prop (fst f)) (rep-prop (fst (snd f))))
As Representable f is a prop we can prove that Reprs are equal if the underlying permutations are.
repr-equality : (f g : Repr) → fst f ≡ fst g → f ≡ g repr-equality (f , fr) (g , gr) p = ΣPathP (p , (isProp→PathP (λ i → isProp× (rep-prop (fst (p i))) (rep-prop (fst (snd (p i))))) fr gr))
Representable elements are closed under group operations
repr-comp : ∀ (f g : ⟨ 𝓖 ⟩ → ⟨ 𝓖 ⟩) → Representable f → Representable g → Representable (λ x → f (g x)) repr-comp f g rf rg x f′ g′ p = rf (g x) (g f′) g′ (rg x f′ g′ p) repr-id : Representable (λ x → x) repr-id x g h p = p repr-inv : ∀ (f : ⟨ SymGroup ⟩) → Representable (fst f) → Representable (fst (snd f)) repr-inv (f , finv , ε , η) rf x g h p = η (finv g · h) x ( x ≡⟨ p ⟩ g · h ≡⟨ cong (_· h) (sym (ε g (finv g) refl)) ⟩ f (finv g) · h ≡⟨ sym (rf (finv g · h) (finv g) h refl) ⟩ f (finv g · h) ∎) Repr-comp : ∀ (f f′ : Repr) → Repr Repr-comp (f , rf , rf′) (g , rg , rg′) = f ·′ g , repr-comp (fst f) (fst g) rf rg , repr-comp (fst (snd g)) (fst (snd f)) rg′ rf′ Repr-id : Repr Repr-id = 1gs , repr-id , repr-id Repr-inv : (f : Repr) → Repr Repr-inv (a@(f , finv , ε , η) , rf , rf′) = a ⁻¹ , rf′ , rf
Associativity and Unitality still hold by definition
Repr-assoc : (f g h : Repr) → Repr-comp f (Repr-comp g h) ≡ Repr-comp (Repr-comp f g) h Repr-assoc f g h = refl Repr-lid : (f : Repr) → Repr-comp Repr-id f ≡ f Repr-lid f = refl Repr-rid : (f : Repr) → Repr-comp f Repr-id ≡ f Repr-rid f = refl
We can prove the invertibility properties
Repr-inv-left : (f : Repr) → Repr-comp (Repr-inv f) f ≡ Repr-id Repr-inv-left f = repr-equality (Repr-comp (Repr-inv f) f) Repr-id (·InvL (SymGroup .snd) (fst f)) Repr-inv-right : (f : Repr) → Repr-comp f (Repr-inv f) ≡ Repr-id Repr-inv-right f = repr-equality (Repr-comp f (Repr-inv f)) Repr-id (·InvR (SymGroup .snd) (fst f))
and the following invertibility property holds definitionally
Repr-inv-comp : (f g : Repr) → Repr-inv (Repr-comp f g) ≡ Repr-comp (Repr-inv g) (Repr-inv f) Repr-inv-comp f g = refl
and hence representable elements of the symmetric group themselves form a group.
RSymGroup : Group ℓ RSymGroup = makeGroup Repr-id Repr-comp Repr-inv repΣ-set Repr-assoc Repr-lid Repr-rid Repr-inv-right Repr-inv-left open GroupStr (RSymGroup .snd) using () renaming (_·_ to _*_; 1g to 1gr; inv to invᵣ)
As stated above, an element is representable if and only if it is in the image of the inclusion homomorphism.
We first have that every included element is representable.
inc-rep : ∀ (a : ⟨ 𝓖 ⟩) → Representable (fst (inc a)) inc-rep a x g h p = a · x ≡⟨ cong (a ·_) p ⟩ a · (g · h) ≡⟨ ·Assoc (𝓖 .snd) a g h ⟩ (a · g) · h ∎and that any representable element is the image of an included element
Repr-inc : ∀ (f : Repr) → Σ[ g ∈ ⟨ 𝓖 ⟩ ] inc g ≡ fst f Repr-inc (a@(f , rest) , rf , rf′) = (f 1g) , inverse-equality-lemma (inc (f 1g)) a is-set is-set λ x → sym (rf x 1g x (sym (·IdL (𝓖 .snd) x)))This allows us to define
incᵣ
incᵣ : ⟨ 𝓖 ⟩ → Repr incᵣ g = inc g , inc-rep g , repr-inv (inc g) (inc-rep g)
and show that it is an equivalence.
open Iso incᵣ-iso : Iso ⟨ 𝓖 ⟩ Repr incᵣ-iso .fun = incᵣ incᵣ-iso .inv f = fst (Repr-inc f) incᵣ-iso .leftInv g = inc-injective (fst (Repr-inc (incᵣ g))) g (snd (Repr-inc (incᵣ g))) incᵣ-iso .rightInv f = repr-equality (incᵣ (fst (Repr-inc f))) f (snd (Repr-inc f)) incᵣ-equiv : ⟨ 𝓖 ⟩ ≃ Repr incᵣ-equiv = isoToEquiv incᵣ-iso
Further it is also a group homomorphism.
incᵣ-homo : ∀ g h → incᵣ (g · h) ≡ incᵣ g * incᵣ h incᵣ-homo g h = repr-equality (incᵣ (g · h)) (incᵣ g * incᵣ h) (inc-homo g h) incᵣ-pres1 : incᵣ-equiv .fst 1g ≡ 1gr incᵣ-pres1 = repr-equality (incᵣ-equiv .fst 1g) 1gr inc-pres1 incᵣ-presinv : (x : ⟨ 𝓖 ⟩) → incᵣ-equiv .fst (GroupStr.inv (snd 𝓖) x) ≡ invᵣ (incᵣ-equiv .fst x) incᵣ-presinv x = repr-equality (incᵣ-equiv .fst (GroupStr.inv (snd 𝓖) x)) (invᵣ (incᵣ-equiv .fst x)) (inc-pres-inv x) incᵣ-group-iso : GroupEquiv 𝓖 RSymGroup incᵣ-group-iso = incᵣ-equiv , record { pres· = incᵣ-homo ; pres1 = incᵣ-pres1 ; presinv = incᵣ-presinv }
Using the structure identity principle, ⟨ 𝓖 ⟩ and RSymgroup ⟨ 𝓖 ⟩ are actually equal.
inc≡ : 𝓖 ≡ RSymGroup inc≡ = equivFun (GroupPath 𝓖 RSymGroup) incᵣ-group-iso