Permutations realizing an order pattern

Fix an injective tuple q : Fin k ↪ α in a finite linear order. Each permutation of α sorts q in exactly one of the k ! possible orders, and the resulting classes are equinumerous, so one permutation in k ! leaves q in increasing order.

Main declarations

• factorial_mul_card_monotone_comp — k ! * #{σ | Monotone (σ ∘ q)} = n !.
• card_monotone_comp_eq — the k ! classes are equinumerous.

Implementation notes

Tuple.comp_sort_eq_comp_iff_monotone supplies uniqueness of the sorting reordering and Equiv.Perm.viaEmbedding transports a reordering of Fin k to a permutation of α fixing everything off the tuple, which turns precomposition into postcomposition and gives the bijections between classes.

[UPSTREAM] Mathlib has no permutation-pattern material; this belongs at Mathlib/Combinatorics/Enumerative/PermutationPattern.lean.

theorem card_monotone_comp_eq {α : Type u_1} [LinearOrder α] [Fintype α] [DecidableEq α] {k : ℕ} (q : Fin k ↪ α) (ρ : Equiv.Perm (Fin k)) : {σ : Equiv.Perm α | Monotone (⇑σ ∘ ⇑q ∘ ⇑ρ)}.card = {σ : Equiv.Perm α | Monotone (⇑σ ∘ ⇑q)}.card

The permutations sorting a fixed injective tuple into a given order all number the same: Perm α splits into k ! equinumerous classes, one per reordering of the tuple.

theorem factorial_mul_card_monotone_comp {α : Type u_1} [LinearOrder α] [Fintype α] [DecidableEq α] {k : ℕ} (q : Fin k ↪ α) : k.factorial * {σ : Equiv.Perm α | Monotone (⇑σ ∘ ⇑q)}.card = (Fintype.card α).factorial

A fixed injective tuple is sorted by one permutation in k !.