Permutations

Content created by Egbert Rijke, Fredrik Bakke, Eléonore Mangel, Jonathan Prieto-Cubides, Elisabeth Stenholm, Maša Žaucer and Victor Blanchi.

Created on 2022-03-12.
Last modified on 2025-02-14.

{-# OPTIONS --lossy-unification #-}

module finite-group-theory.permutations where
Imports
open import elementary-number-theory.modular-arithmetic-standard-finite-types
open import elementary-number-theory.natural-numbers

open import finite-group-theory.orbits-permutations
open import finite-group-theory.permutations-standard-finite-types
open import finite-group-theory.transpositions

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.iterating-functions
open import foundation.iterating-involutions
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.sets
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.generating-sets-groups
open import group-theory.subgroups-generated-by-subsets-groups
open import group-theory.symmetric-groups

open import lists.functoriality-lists
open import lists.lists

open import univalent-combinatorics.2-element-decidable-subtypes
open import univalent-combinatorics.2-element-types
open import univalent-combinatorics.counting
open import univalent-combinatorics.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

A permutation of X is an automorphism of X.

Properties

module _
  {l1 l2 : Level} (X : UU l1) (eX : count X) (f : X  X)
  where

  list-transpositions-permutation-count :
    list
      ( Σ
        ( X  Decidable-Prop l2)
        ( λ P 
          has-cardinality-ℕ 2 (Σ X (type-Decidable-Prop  P))))
  list-transpositions-permutation-count =
    map-list
      ( transposition-conjugation-equiv
        ( Fin (number-of-elements-count eX))
        ( X)
        ( equiv-count eX))
      ( list-transpositions-permutation-Fin
        ( number-of-elements-count eX)
        ( (inv-equiv-count eX ∘e f) ∘e equiv-count eX))

  abstract
    retraction-permutation-list-transpositions-count :
      htpy-equiv
        ( permutation-list-transpositions list-transpositions-permutation-count)
        ( f)
    retraction-permutation-list-transpositions-count x =
      ( correct-transposition-conjugation-equiv-list
        ( Fin (number-of-elements-count eX))
        ( X)
        ( equiv-count eX)
        ( list-transpositions-permutation-Fin
          ( number-of-elements-count eX)
          ( (inv-equiv-count eX ∘e f) ∘e equiv-count eX))
        ( x)) 
        ( ( ap
            ( map-equiv-count eX)
            ( retraction-permutation-list-transpositions-Fin
              ( number-of-elements-count eX)
              ( (inv-equiv-count eX ∘e f) ∘e equiv-count eX)
              ( map-inv-equiv-count eX x))) 
          ( ( htpy-eq-equiv
              ( right-inverse-law-equiv (equiv-count eX))
              ( map-equiv ((f ∘e (equiv-count eX)) ∘e inv-equiv-count eX) x)) 
            ( ap
              ( λ g  map-equiv (f ∘e g) x)
              ( right-inverse-law-equiv (equiv-count eX)))))

For X finite, the symmetric group of X is generated by transpositions

module _
  {l1 l2 : Level} (n : ) (X : Type-With-Cardinality-ℕ l1 n)
  where

  is-generated-transposition-symmetric-Fin-Level :
    is-generating-set-Group
      ( symmetric-Group (set-Type-With-Cardinality-ℕ n X))
      ( is-transposition-permutation-Prop)
  is-generated-transposition-symmetric-Fin-Level f =
    apply-universal-property-trunc-Prop
      ( has-cardinality-type-Type-With-Cardinality-ℕ n X)
      ( subset-subgroup-subset-Group
        ( symmetric-Group (set-Type-With-Cardinality-ℕ n X))
        ( is-transposition-permutation-Prop)
        ( f))
      ( λ h 
        unit-trunc-Prop
          ( pair
            ( map-list
              ( λ x 
                pair
                  ( inr star)
                  ( pair
                    ( transposition x)
                    ( unit-trunc-Prop (pair x refl))))
              ( list-transpositions-permutation-count
                ( type-Type-With-Cardinality-ℕ n X)
                ( pair n h)
                ( f)))
            ( ( lemma
                ( list-transpositions-permutation-count
                  ( type-Type-With-Cardinality-ℕ n X)
                  ( pair n h)
                  ( f))) 
              ( eq-htpy-equiv
                ( retraction-permutation-list-transpositions-count
                  ( type-Type-With-Cardinality-ℕ n X)
                  ( pair n h)
                  ( f))))))
    where
    lemma :
      (l :
        list
          ( 2-Element-Decidable-Subtype l2
            ( type-Type-With-Cardinality-ℕ n X))) 
      Id
        ( ev-formal-combination-subset-Group
          ( symmetric-Group (set-Type-With-Cardinality-ℕ n X))
          ( is-transposition-permutation-Prop)
          ( map-list
            ( λ x 
              pair
                ( inr star)
                ( pair (transposition x) (unit-trunc-Prop (pair x refl))))
            ( l)))
        ( permutation-list-transpositions l)
    lemma nil = refl
    lemma (cons x l) = ap ((transposition x) ∘e_) (lemma l)
module _
  {l : Level} (n : ) (X : Type-With-Cardinality-ℕ l n)
  (f : type-Type-With-Cardinality-ℕ n X  type-Type-With-Cardinality-ℕ n X)
  where

  parity-transposition-permutation : UU (lsuc l)
  parity-transposition-permutation =
    Σ ( Fin 2)
      ( λ k 
        type-trunc-Prop
          ( Σ
            ( list
              ( Σ
                ( type-Type-With-Cardinality-ℕ n X  Decidable-Prop l)
                ( λ P 
                  has-cardinality-ℕ 2
                    ( Σ ( type-Type-With-Cardinality-ℕ n X)
                        ( type-Decidable-Prop  P)))))
            ( λ li 
              Id k (mod-two-ℕ (length-list li)) ×
              Id f (permutation-list-transpositions li))))

  abstract
    is-contr-parity-transposition-permutation :
      is-contr parity-transposition-permutation
    is-contr-parity-transposition-permutation =
      apply-universal-property-trunc-Prop
        ( has-cardinality-type-Type-With-Cardinality-ℕ n X)
        ( is-trunc-Prop neg-two-𝕋 parity-transposition-permutation)
        ( λ h 
          pair
            ( pair
              ( mod-two-ℕ (length-list (list-transposition-f h)))
              ( unit-trunc-Prop
                ( pair (list-transposition-f h)
                  ( pair refl
                    ( inv
                      ( eq-htpy-equiv
                        ( retraction-permutation-list-transpositions-count
                          ( type-Type-With-Cardinality-ℕ n X)
                          ( pair n h)
                          ( f))))))))
            ( λ (pair k u) 
              eq-pair-Σ
                ( apply-universal-property-trunc-Prop u
                  ( Id-Prop
                    ( Fin-Set 2)
                    ( mod-two-ℕ (length-list (list-transposition-f h)))
                    ( k))
                  ( λ (pair li (pair q r)) 
                    is-injective-iterate-involution
                      ( mod-two-ℕ (length-list (list-transposition-f h)))
                      ( k)
                      ( sign-permutation-orbit
                        ( n)
                        ( pair
                          ( type-Type-With-Cardinality-ℕ n X)
                          ( unit-trunc-Prop h))
                        ( id-equiv))
                      ( inv
                        ( iterate-involution
                          ( succ-Fin 2)
                          ( is-involution-aut-Fin-2 (equiv-succ-Fin 2))
                          ( length-list (list-transposition-f h))
                          ( sign-permutation-orbit
                            ( n)
                            ( pair
                              ( type-Type-With-Cardinality-ℕ n X)
                              ( unit-trunc-Prop h))
                            ( id-equiv))) 
                        ( ( sign-list-transpositions-count
                            ( type-Type-With-Cardinality-ℕ n X)
                            ( pair n h)
                            ( list-transposition-f h)) 
                          ( ap
                            ( sign-permutation-orbit
                              ( n)
                              ( pair
                                ( type-Type-With-Cardinality-ℕ n X)
                                ( unit-trunc-Prop h)))
                            { x =
                              permutation-list-transpositions
                                ( list-transposition-f h)}
                            { y = permutation-list-transpositions li}
                            ( ( eq-htpy-equiv
                                ( retraction-permutation-list-transpositions-count
                                  ( type-Type-With-Cardinality-ℕ n X)
                                  ( pair n h)
                                  ( f))) 
                              ( r)) 
                            ( inv
                              ( sign-list-transpositions-count
                                ( type-Type-With-Cardinality-ℕ n X)
                                ( pair n h)
                                ( li)) 
                              ( ( iterate-involution
                                  ( succ-Fin 2)
                                  ( is-involution-aut-Fin-2
                                    ( equiv-succ-Fin 2))
                                  ( length-list li)
                                ( sign-permutation-orbit
                                  ( n)
                                  ( pair
                                    ( type-Type-With-Cardinality-ℕ n X)
                                    ( unit-trunc-Prop h))
                                  ( id-equiv))) 
                                ( ap
                                  ( λ k 
                                    iterate
                                      ( nat-Fin 2 k)
                                      (succ-Fin 2)
                                      ( sign-permutation-orbit
                                        ( n)
                                        ( pair
                                          ( type-Type-With-Cardinality-ℕ
                                            ( n)
                                            ( X))
                                          ( unit-trunc-Prop h))
                                        ( id-equiv)))
                                  ( inv q)))))))))
                ( eq-is-prop is-prop-type-trunc-Prop)))
      where
      list-transposition-f :
        (h : Fin n  (type-Type-With-Cardinality-ℕ n X)) 
        list
          ( Σ
            ( type-Type-With-Cardinality-ℕ n X  Decidable-Prop l)
            ( λ P 
              has-cardinality-ℕ 2
                ( Σ ( type-Type-With-Cardinality-ℕ n X)
                    ( type-Decidable-Prop  P))))
      list-transposition-f h =
        list-transpositions-permutation-count
          ( type-Type-With-Cardinality-ℕ n X)
          ( pair n h)
          ( f)
      is-injective-iterate-involution :
        (k k' x : Fin 2) 
        Id
          ( iterate (nat-Fin 2 k) (succ-Fin 2) x)
          ( iterate (nat-Fin 2 k') (succ-Fin 2) x) 
        Id k k'
      is-injective-iterate-involution
        (inl (inr star)) (inl (inr star)) x p =
        refl
      is-injective-iterate-involution
        (inl (inr star)) (inr star) (inl (inr star)) p =
        ex-falso (neq-inl-inr p)
      is-injective-iterate-involution
        (inl (inr star)) (inr star) (inr star) p =
        ex-falso (neq-inr-inl p)
      is-injective-iterate-involution
        (inr star) (inl (inr star)) (inl (inr star)) p =
        ex-falso (neq-inr-inl p)
      is-injective-iterate-involution
        (inr star) (inl (inr star)) (inr star) p =
        ex-falso (neq-inl-inr p)
      is-injective-iterate-involution
        (inr star) (inr star) x p = refl

Recent changes