The first element of a finset under a permutation

This file counts permutations by the element of a finset that they place first. A permutation σ of a finite linear order places x first among the elements of D when x ∈ D and σ.symm attains its minimum on D at x, so that x comes earliest among the elements of D in the sequence σ 0, σ 1, …. Composing σ with the swap of two elements of D exchanges which of them comes first. A family of permutations closed under such swaps therefore places each element of D first equally often, and a uniformly random permutation places each element of D first with probability 1 / #D.

Main results

• Equiv.Perm.card_filter_isMinOn_symm_mul_card: in a family S closed under swaps of elements of D, the permutations placing an element of Y first among D, counted #D times, number #S * #(Y ∩ D).
• Equiv.Perm.card_filter_isMinOn_symm_univ_mul_card: the same count over all permutations.

theorem Equiv.Perm.eq_of_isMinOn_symm {α : Type u_1} [LinearOrder α] {D : Finset α} {σ : Perm α} {x y : α} (hx : x ∈ D) (hy : y ∈ D) (hxm : IsMinOn (⇑(Equiv.symm σ)) (↑D) x) (hym : IsMinOn (⇑(Equiv.symm σ)) (↑D) y) : x = y

A permutation places at most one element of D first.

theorem Equiv.Perm.exists_isMinOn_symm {α : Type u_1} [LinearOrder α] {D : Finset α} (hD : D.Nonempty) (σ : Perm α) : ∃ x ∈ D, IsMinOn (⇑(Equiv.symm σ)) (↑D) x

Every permutation places some element of a nonempty D first.

theorem Equiv.Perm.isMinOn_symm_swap_mul_iff {α : Type u_1} [LinearOrder α] {D : Finset α} {σ : Perm α} {y y' x : α} (hy : y ∈ D) (hy' : y' ∈ D) : IsMinOn (⇑(Equiv.symm (swap y y' * σ))) (↑D) ((swap y y') x) ↔ IsMinOn (⇑(Equiv.symm σ)) (↑D) x

Composing with the swap of two elements y and y' of D exchanges them as the first element of D.

theorem Equiv.Perm.card_filter_isMinOn_symm_mul_card {α : Type u_1} [LinearOrder α] (S : Finset (Perm α)) (D Y : Finset α) (hS : ∀ y ∈ D, ∀ y' ∈ D, ∀ σ ∈ S, swap y y' * σ ∈ S) : {σ ∈ S | ∃ x ∈ Y ∩ D, IsMinOn (⇑(Equiv.symm σ)) (↑D) x}.card * D.card = S.card * (Y ∩ D).card

In a family S of permutations closed under swaps of elements of D, the permutations placing an element of Y first among D, counted #D times, number #S * #(Y ∩ D).

theorem Equiv.Perm.card_filter_isMinOn_symm_univ_mul_card {α : Type u_1} [LinearOrder α] [Fintype α] (D Y : Finset α) : {σ : Perm α | ∃ x ∈ Y ∩ D, IsMinOn (⇑(Equiv.symm σ)) (↑D) x}.card * D.card = (Fintype.card α).factorial * (Y ∩ D).card

The permutations placing an element of Y first among D, counted #D times, number (card α)! * #(Y ∩ D).