Documentation

TauCeti.RepresentationTheory.Symmetric.Partitions

Partitions and conjugacy classes of permutations #

This file gives the equivalence between partitions and conjugacy classes of permutations. It is proved for permutations of any finite type and specialized to Equiv.Perm (Fin n) for the roadmap API. Mathlib's partition of a permutation includes the fixed points as parts of size one.

The specialization to Fin n carries a transport along Fintype.card (Fin n) = n, which TauCeti.parts_partitionEquivConjClasses_symm_mk discharges on the parts: the partition indexing the class of σ has the parts of the cycle type of σ.

References #

source
theorem TauCeti.exists_perm_partition_eq {α : Type u_1} [Fintype α] [DecidableEq α] (p : (Fintype.card α).Partition) :
∃ (σ : Equiv.Perm α), σ.partition = p

Every partition of the cardinality of a finite type is the partition of a permutation.

source
def TauCeti.permConjClassPartition {α : Type u_1} [Fintype α] [DecidableEq α] :
ConjClasses (Equiv.Perm α) → (Fintype.card α).Partition

The partition of a conjugacy class of permutations.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.permConjClassPartition_mk {α : Type u_1} [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
    permConjClassPartition (ConjClasses.mk σ) = σ.partition

    Taking the partition of the class of a permutation recovers its partition.

    source
    theorem TauCeti.permConjClassPartition_injective {α : Type u_1} [Fintype α] [DecidableEq α] :
    Function.Injective permConjClassPartition

    The partition distinguishes conjugacy classes of permutations.

    source
    theorem TauCeti.permConjClassPartition_surjective {α : Type u_1} [Fintype α] [DecidableEq α] :
    Function.Surjective permConjClassPartition

    Every partition is attained by a conjugacy class of permutations.

    source
    noncomputable def TauCeti.partitionEquivPermConjClasses (α : Type u_1) [Fintype α] [DecidableEq α] :
    (Fintype.card α).Partition ≃ ConjClasses (Equiv.Perm α)

    Partitions of the cardinality of a finite type are equivalent to conjugacy classes of its permutations.

    Equations
    Instances For
      source
      noncomputable def TauCeti.partitionEquivConjClasses (n : ℕ) :
      n.Partition ≃ ConjClasses (Equiv.Perm (Fin n))

      Partitions of n are equivalent to conjugacy classes of the symmetric group on Fin n.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.permConjClassPartition_partitionEquivPermConjClasses (α : Type u_1) [Fintype α] [DecidableEq α] (p : (Fintype.card α).Partition) :
        permConjClassPartition ((partitionEquivPermConjClasses α) p) = p

        The conjugacy class associated to a partition has that partition.

        source
        @[simp]
        theorem TauCeti.permConjClassPartition_partitionEquivConjClasses (n : ℕ) (p : n.Partition) :
        permConjClassPartition ((partitionEquivConjClasses n) p) = (Equiv.cast ⋯) p

        The conjugacy class associated to a partition of n has that partition.

        source
        @[simp]
        theorem TauCeti.partitionEquivPermConjClasses_symm_mk (α : Type u_1) [Fintype α] [DecidableEq α] (σ : Equiv.Perm α) :
        (partitionEquivPermConjClasses α).symm (ConjClasses.mk σ) = σ.partition

        The inverse class-to-partition map sends a representative to its permutation partition.

        source
        @[simp]
        theorem TauCeti.partitionEquivConjClasses_symm_mk (n : ℕ) (σ : Equiv.Perm (Fin n)) :
        (partitionEquivConjClasses n).symm (ConjClasses.mk σ) = (Equiv.cast ⋯).symm σ.partition

        The inverse class-to-partition map for Fin n sends a representative to its permutation partition.

        source
        theorem TauCeti.parts_partitionEquivConjClasses_symm_mk (n : ℕ) (σ : Equiv.Perm (Fin n)) :
        ((partitionEquivConjClasses n).symm (ConjClasses.mk σ)).parts = σ.partition.parts

        The partition indexing the class of σ has the parts of the cycle type of σ. This is TauCeti.partitionEquivConjClasses_symm_mk with the transport along Fintype.card (Fin n) = n carried out on the parts, which is the form in which the partition is compared with σ itself.

        source
        theorem TauCeti.card_conjClasses_perm_eq_card_partition (α : Type u_1) [Fintype α] [DecidableEq α] :
        Fintype.card (ConjClasses (Equiv.Perm α)) = Fintype.card (Fintype.card α).Partition

        The number of conjugacy classes of permutations of a finite type is the number of partitions of its cardinality.

        source
        theorem TauCeti.card_conjClasses_perm (n : ℕ) :
        Fintype.card (ConjClasses (Equiv.Perm (Fin n))) = Fintype.card n.Partition

        The number of conjugacy classes of the symmetric group on Fin n is the number of partitions of n.