Documentation

LeanPool.RegtsSevenster.RS.Classical.SchurTheory.StabCount

Stabiliser count for colourings #

For f : Fin n → Fin N, the number of permutations π with f ∘ π = f equals ∏ j, (fibreCard f j)!.

Simp helper for the sigma-fibre equivalence #

Forward and backward maps #

source
def RS.toFibrePerms {n N : ℕ} (f : Fin n → Fin N) (π : Equiv.Perm (Fin n)) (hπ : f ∘ ⇑π = f) (j : Fin N) :
Equiv.Perm { i : Fin n // f i = j }

Forward: a fixing permutation restricts to each fibre.

Equations
Instances For
    source
    def RS.ofFibrePerms {n N : ℕ} (f : Fin n → Fin N) (σ : (j : Fin N) → Equiv.Perm { i : Fin n // f i = j }) :
    Equiv.Perm (Fin n)

    Backward: fibre permutations assemble into a global fixing permutation.

    Equations
    Instances For
      source
      theorem RS.ofFibrePerms_fixes {n N : ℕ} (f : Fin n → Fin N) (σ : (j : Fin N) → Equiv.Perm { i : Fin n // f i = j }) :
      f ∘ ⇑(ofFibrePerms f σ) = f

      Permuting within each fibre fixes the colouring.

      The fixing-perms–fibre-perms equivalence #

      source
      def RS.fixingEquiv {n N : ℕ} (f : Fin n → Fin N) :
      { π : Equiv.Perm (Fin n) // f ∘ ⇑π = f } ≃ ((j : Fin N) → Equiv.Perm { i : Fin n // f i = j })

      The bijection between fixing permutations and families of fibre permutations.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem RS.ofFibrePerms_def {n N : ℕ} (f : Fin n → Fin N) (σ : (j : Fin N) → Equiv.Perm { i : Fin n // f i = j }) :
        ofFibrePerms f σ = (Equiv.sigmaFiberEquiv f).permCongr (Equiv.Perm.sigmaCongrRight σ)

        ofFibrePerms unfolds to the conjugated sigma-congruence.

        source
        theorem RS.fixingEquiv_symm_apply {n N : ℕ} (f : Fin n → Fin N) (σ : (j : Fin N) → Equiv.Perm { i : Fin n // f i = j }) :
        ↑((fixingEquiv f).symm σ) = ofFibrePerms f σ

        The inverse of the fixing equivalence is ofFibrePerms.

        The cardinality step #

        source
        theorem RS.fibreCard_eq_card {n N : ℕ} (f : Fin n → Fin N) (j : Fin N) :
        fibreCard f j = Fintype.card { i : Fin n // f i = j }

        Fibre card equals the Fintype card of the fibre subtype.

        source
        theorem RS.card_fixing_perms {n N : ℕ} (f : Fin n → Fin N) :
        {π : Equiv.Perm (Fin n) | f ∘ ⇑π = f}.card = ∏ j : Fin N, (fibreCard f j).factorial

        The stabiliser count: the permutations fixing a colouring are exactly those, so there are the product of the fibre factorials.