Permutations

{-# 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.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.functions
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.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
    retr-permutation-list-transpositions-count :
      htpy-equiv
        ( permutation-list-transpositions list-transpositions-permutation-count)
        ( f)
    retr-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)
            ( retr-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 : UU-Fin l1 n)
  where

  is-generated-transposition-symmetric-Fin-Level :
    is-generating-subset-Group
      ( symmetric-Group (set-UU-Fin n X))
      ( is-transposition-permutation-Prop)
  is-generated-transposition-symmetric-Fin-Level f =
    apply-universal-property-trunc-Prop
      ( has-cardinality-type-UU-Fin n X)
      ( subset-subgroup-subset-Group
        ( symmetric-Group (set-UU-Fin 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-UU-Fin n X)
                ( pair n h)
                ( f)))
            ( ( lemma
                ( list-transpositions-permutation-count
                  ( type-UU-Fin n X)
                  ( pair n h)
                  ( f))) 
              ( eq-htpy-equiv
                ( retr-permutation-list-transpositions-count
                  ( type-UU-Fin n X)
                  ( pair n h)
                  ( f))))))
    where
    lemma :
      (l : list (2-Element-Decidable-Subtype l2 (type-UU-Fin n X))) 
      Id
        ( ev-formal-combination-subset-Group
          ( symmetric-Group (set-UU-Fin 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 : UU-Fin l n)
  where

  module _
    (f : (type-UU-Fin n X)  (type-UU-Fin n X))
    where

    parity-transposition-permutation : UU (lsuc l)
    parity-transposition-permutation =
      Σ ( Fin 2)
        ( λ k 
          type-trunc-Prop
            ( Σ
              ( list
                ( Σ
                  ( type-UU-Fin n X  Decidable-Prop l)
                  ( λ P 
                    has-cardinality 2
                      ( Σ (type-UU-Fin 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-UU-Fin 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
                          ( retr-permutation-list-transpositions-count
                            ( type-UU-Fin 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-UU-Fin n X) (unit-trunc-Prop h))
                          ( id-equiv))
                        ( inv
                          ( iterate-involution
                            ( succ-Fin 2)
                            ( is-involution-aut-Fin-two-ℕ (equiv-succ-Fin 2))
                            ( length-list (list-transposition-f h))
                            ( sign-permutation-orbit
                              ( n)
                              ( pair (type-UU-Fin n X) (unit-trunc-Prop h))
                              ( id-equiv))) 
                          ( ( sign-list-transpositions-count
                              ( type-UU-Fin n X)
                              ( pair n h)
                              ( list-transposition-f h)) 
                            ( ap
                              ( sign-permutation-orbit
                                ( n)
                                ( pair (type-UU-Fin n X) (unit-trunc-Prop h)))
                              { x =
                                permutation-list-transpositions
                                  ( list-transposition-f h)}
                              { y = permutation-list-transpositions li}
                              ( ( eq-htpy-equiv
                                  ( retr-permutation-list-transpositions-count
                                    ( type-UU-Fin n X)
                                    ( pair n h)
                                    ( f))) 
                                ( r)) 
                              ( inv
                                ( sign-list-transpositions-count
                                  ( type-UU-Fin n X)
                                  ( pair n h)
                                  ( li)) 
                                ( ( iterate-involution
                                    ( succ-Fin 2)
                                    ( is-involution-aut-Fin-two-ℕ
                                      ( equiv-succ-Fin 2))
                                    ( length-list li)
                                  ( sign-permutation-orbit
                                    ( n)
                                    ( pair
                                      ( type-UU-Fin n X)
                                      ( unit-trunc-Prop h))
                                    ( id-equiv))) 
                                  ( ap
                                    ( λ k 
                                      iterate
                                        ( nat-Fin 2 k)
                                        (succ-Fin 2)
                                        ( sign-permutation-orbit
                                          ( n)
                                          ( pair
                                            ( type-UU-Fin 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-UU-Fin n X)) 
          list
            ( Σ
              ( type-UU-Fin n X  Decidable-Prop l)
              ( λ P 
                has-cardinality 2
                  ( Σ (type-UU-Fin n X) (type-Decidable-Prop  P))))
        list-transposition-f h =
          list-transpositions-permutation-count (type-UU-Fin 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