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