The sign homomorphism

Content created by Egbert Rijke, Fredrik Bakke, Eléonore Mangel, Jonathan Prieto-Cubides, Elisabeth Stenholm, Julian KG, fernabnor and louismntnu.

Created on 2022-03-24.
Last modified on 2023-11-24.

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

open import finite-group-theory.permutations
open import finite-group-theory.transpositions

open import foundation.action-on-identifications-functions
open import foundation.automorphisms
open import foundation.contractible-types
open import foundation.coproduct-types
open import foundation.decidable-propositions
open import foundation.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.propositional-truncations
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels

open import group-theory.homomorphisms-groups
open import group-theory.homomorphisms-semigroups
open import group-theory.symmetric-groups

open import lists.concatenation-lists
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.finite-types
open import univalent-combinatorics.standard-finite-types

Idea

The sign of a permutation is defined as the parity of the length of the decomposition of the permutation into transpositions. We show that each such decomposition as the same parity, so the sign map is well defined. We then show that the sign map is a group homomorphism.

Definitions

The sign homomorphism into ℤ/2

module _
  {l : Level} (n : ℕ) (X : UU-Fin l n)
  where

  sign-homomorphism-Fin-two : Aut (type-UU-Fin n X) → Fin 2
  sign-homomorphism-Fin-two f =
    pr1 (center (is-contr-parity-transposition-permutation n X f))

  preserves-add-sign-homomorphism-Fin-two :
    (f g : (type-UU-Fin n X) ≃ (type-UU-Fin n X)) →
    Id
      ( sign-homomorphism-Fin-two (f ∘e g))
      ( add-Fin 2 (sign-homomorphism-Fin-two f) (sign-homomorphism-Fin-two g))
  preserves-add-sign-homomorphism-Fin-two f g =
    apply-universal-property-trunc-Prop
      ( has-cardinality-type-UU-Fin n X)
      ( Id-Prop
        ( Fin-Set 2)
        ( sign-homomorphism-Fin-two (f ∘e g))
        ( add-Fin 2
          ( sign-homomorphism-Fin-two f)
          ( sign-homomorphism-Fin-two g)))
      ( λ h →
        ( ap
          ( pr1)
          ( eq-is-contr
            ( is-contr-parity-transposition-permutation n X (f ∘e g))
            { x =
              center (is-contr-parity-transposition-permutation n X (f ∘e g))}
            { y =
              pair
                ( mod-two-ℕ (length-list (list-comp-f-g h)))
                ( unit-trunc-Prop
                  ( pair
                    ( list-comp-f-g h)
                    ( pair refl (eq-list-comp-f-g h))))})) ∙
        ( ( ap
            ( mod-two-ℕ)
            ( length-concat-list (list-trans f h) (list-trans g h))) ∙
          ( ( mod-succ-add-ℕ 1
              ( length-list (list-trans f h))
              ( length-list (list-trans g h))) ∙
            ( ( ap
                ( λ P →
                  add-Fin 2 (pr1 P)
                    ( mod-two-ℕ (length-list (list-trans g h))))
                { x =
                  pair
                    ( mod-two-ℕ (length-list (list-trans f h)))
                    ( unit-trunc-Prop
                      ( pair
                        ( list-trans f h)
                        ( pair
                          ( refl)
                          ( inv
                            ( eq-htpy-equiv
                              ( retraction-permutation-list-transpositions-count
                                ( type-UU-Fin n X)
                                ( pair n h)
                                ( f)))))))}
                { y = center (is-contr-parity-transposition-permutation n X f)}
                ( eq-is-contr
                  ( is-contr-parity-transposition-permutation n X f))) ∙
              ( ap
                ( λ P → add-Fin 2 (sign-homomorphism-Fin-two f) (pr1 P))
                { x =
                  pair
                    ( mod-two-ℕ (length-list (list-trans g h)))
                    ( unit-trunc-Prop
                      ( pair
                        ( list-trans g h)
                        ( pair
                          ( refl)
                          ( inv
                            ( eq-htpy-equiv
                              ( retraction-permutation-list-transpositions-count
                                ( type-UU-Fin n X)
                                ( pair n h)
                                ( g)))))))}
                { y = center (is-contr-parity-transposition-permutation n X g)}
                ( eq-is-contr
                  ( is-contr-parity-transposition-permutation n X g)))))))
    where
    list-trans :
      ( f' : (type-UU-Fin n X) ≃ (type-UU-Fin n X))
      ( 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-trans f' h =
      list-transpositions-permutation-count (type-UU-Fin n X) (pair n h) f'
    list-comp-f-g :
      ( 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-comp-f-g h = concat-list (list-trans f h) (list-trans g h)
    eq-list-comp-f-g :
      ( h : Fin n ≃ type-UU-Fin n X) →
      Id
        ( f ∘e g)
        ( permutation-list-transpositions
          ( list-comp-f-g h))
    eq-list-comp-f-g h =
      eq-htpy-equiv
        ( λ x →
          ( inv
            ( retraction-permutation-list-transpositions-count
              ( type-UU-Fin n X)
              ( pair n h)
              ( f)
              ( map-equiv g x))) ∙
          ( ap
            ( map-equiv
              ( permutation-list-transpositions
                ( list-trans f h)))
            ( inv
              ( retraction-permutation-list-transpositions-count
                ( type-UU-Fin n X)
                ( pair n h)
                ( g)
                ( x))))) ∙
              ( eq-concat-permutation-list-transpositions
                ( list-trans f h)
                ( list-trans g h))

  eq-sign-homomorphism-Fin-two-transposition :
    ( Y : 2-Element-Decidable-Subtype l (type-UU-Fin n X)) →
    Id
      ( sign-homomorphism-Fin-two (transposition Y))
      ( inr star)
  eq-sign-homomorphism-Fin-two-transposition Y =
    ap pr1
      { x =
        center
          ( is-contr-parity-transposition-permutation n X (transposition Y))}
      { y =
        pair
          ( inr star)
          ( unit-trunc-Prop
            ( pair
              ( unit-list Y)
              ( pair refl (inv (right-unit-law-equiv (transposition Y))))))}
      ( eq-is-contr
        ( is-contr-parity-transposition-permutation n X (transposition Y)))

module _
  {l l' : Level} (n : ℕ) (X : UU-Fin l n) (Y : UU-Fin l' n)
  where

  preserves-conjugation-sign-homomorphism-Fin-two :
    (f : (type-UU-Fin n X) ≃ (type-UU-Fin n X)) →
    (g : (type-UU-Fin n X) ≃ (type-UU-Fin n Y)) →
    Id
      ( sign-homomorphism-Fin-two n Y (g ∘e (f ∘e inv-equiv g)))
      ( sign-homomorphism-Fin-two n X f)
  preserves-conjugation-sign-homomorphism-Fin-two f g =
    apply-universal-property-trunc-Prop
      ( has-cardinality-type-UU-Fin n X)
      ( Id-Prop
        ( Fin-Set 2)
        ( sign-homomorphism-Fin-two n Y (g ∘e (f ∘e inv-equiv g)))
        ( sign-homomorphism-Fin-two n X f))
      ( λ h →
        ( ap
          ( pr1)
            ( eq-is-contr
              ( is-contr-parity-transposition-permutation
                ( n)
                ( Y)
                ( g ∘e (f ∘e inv-equiv g)))
              { x =
                center
                  ( is-contr-parity-transposition-permutation
                    ( n)
                    ( Y)
                    ( g ∘e (f ∘e inv-equiv g)))}
              { y =
                pair
                  ( mod-two-ℕ
                    ( length-list
                      ( map-list
                        ( map-equiv
                          ( equiv-universes-2-Element-Decidable-Subtype
                            ( type-UU-Fin n Y)
                            ( l)
                            ( l')))
                        ( list-conjugation h))))
                  ( unit-trunc-Prop
                    ( pair
                      ( map-list
                        ( map-equiv
                          ( equiv-universes-2-Element-Decidable-Subtype
                            ( type-UU-Fin n Y)
                            ( l)
                            ( l')))
                        ( list-conjugation h))
                      ( pair
                        ( refl)
                        ( ( inv
                          ( ( eq-htpy-equiv
                            ( correct-transposition-conjugation-equiv-list
                              ( type-UU-Fin n X)
                              ( type-UU-Fin n Y)
                              ( g)
                              ( list-trans h))) ∙
                            ( ap
                              ( λ h' → g ∘e (h' ∘e inv-equiv g))
                              ( eq-htpy-equiv
                                { e =
                                  permutation-list-transpositions
                                    ( list-trans h)}
                                ( retraction-permutation-list-transpositions-count
                                  ( type-UU-Fin n X)
                                  ( pair n h)
                                  ( f)))))) ∙
                          ( eq-equiv-universes-transposition-list
                            ( type-UU-Fin n Y)
                            ( l)
                            ( l')
                            ( list-conjugation h))))))})) ∙
          ( ( ap
            ( mod-two-ℕ)
            ( ( length-map-list
              ( map-equiv
                ( equiv-universes-2-Element-Decidable-Subtype
                  ( type-UU-Fin n Y)
                  ( l)
                  ( l')))
              ( list-conjugation h)) ∙
              ( length-map-list
              ( transposition-conjugation-equiv
                ( type-UU-Fin n X)
                ( type-UU-Fin n Y)
                ( g))
              ( list-trans h)))) ∙
            ( ap
              ( pr1)
              { x =
                pair
                  ( mod-two-ℕ (length-list (list-trans h)))
                  ( unit-trunc-Prop
                    ( pair
                      ( list-trans h)
                      ( pair
                        ( refl)
                        ( inv
                          ( eq-htpy-equiv
                            ( retraction-permutation-list-transpositions-count
                              ( type-UU-Fin n X)
                              ( pair n h)
                              ( f)))))))}
              { y = center (is-contr-parity-transposition-permutation n X f)}
              ( eq-is-contr
                ( is-contr-parity-transposition-permutation n X f)))))
    where
    list-trans :
      ( 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-trans h =
      list-transpositions-permutation-count
        ( type-UU-Fin n X)
        ( pair n h)
        ( f)
    list-conjugation :
      ( h : Fin n ≃ type-UU-Fin n X) →
      list
        ( Σ ( (type-UU-Fin n Y) → Decidable-Prop l)
            ( λ P →
              has-cardinality 2
                ( Σ
                  ( type-UU-Fin n Y)
                  ( type-Decidable-Prop ∘ P))))
    list-conjugation h =
      map-list
        ( transposition-conjugation-equiv
          { l4 = l}
          ( type-UU-Fin n X)
          ( type-UU-Fin n Y)
          ( g))
        ( list-trans h)

The sign homomorphism into the symmetric group S₂

module _
  {l : Level} (n : ℕ) (X : UU-Fin l n)
  where

  map-sign-homomorphism : Aut (type-UU-Fin n X) → Aut (Fin 2)
  map-sign-homomorphism f =
    aut-point-Fin-two-ℕ (sign-homomorphism-Fin-two n X f)

  preserves-comp-map-sign-homomorphism :
    preserves-mul _∘e_ _∘e_ map-sign-homomorphism
  preserves-comp-map-sign-homomorphism {f} {g} =
    ( ap
      ( aut-point-Fin-two-ℕ)
      ( preserves-add-sign-homomorphism-Fin-two n X f g)) ∙
    ( preserves-add-aut-point-Fin-two-ℕ
      ( sign-homomorphism-Fin-two n X f)
      ( sign-homomorphism-Fin-two n X g))

  sign-homomorphism :
    hom-Group
      ( symmetric-Group (set-UU-Fin n X))
      ( symmetric-Group (Fin-Set 2))
  pr1 sign-homomorphism = map-sign-homomorphism
  pr2 sign-homomorphism = preserves-comp-map-sign-homomorphism

  eq-sign-homomorphism-transposition :
    ( Y : 2-Element-Decidable-Subtype l (type-UU-Fin n X)) →
    Id
      ( map-hom-Group
        ( symmetric-Group (set-UU-Fin n X))
        ( symmetric-Group (Fin-Set 2))
        ( sign-homomorphism)
        ( transposition Y))
      ( equiv-succ-Fin 2)
  eq-sign-homomorphism-transposition Y =
    ap aut-point-Fin-two-ℕ (eq-sign-homomorphism-Fin-two-transposition n X Y)

Recent changes