Library mathcomp_eulerian.cycles

From mathcomp Require Import all_ssreflect fingroup perm.
From mathcomp_eulerian Require Import ordinal_reindex perm_compress descent.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


cycle_count s is the number of cycles in the disjoint-cycle decomposition of s, equivalently the cardinality of porbits s, the set of orbits of s acting on T by iteration. Stanley's c(w).
Definition cycle_count {T : finType} (s : {perm T}) : nat := #|porbits s|.


stirling_c n k is the number of permutations of 'I_n with exactly k cycles in their disjoint-cycle decomposition. This is Stanley's c(n, k), the signless Stirling number of the first kind (Stanley EC1 §1.3.2).
Definition stirling_c (n k : nat) : nat :=
  #|[set s : {perm 'I_n} | cycle_count s == k]|.


Section CycleBasic.

Each cycle is non-empty, so cycle_count s ≤ #|T|. Cycle analogue of des_le for descents.
Lemma cycle_count_le {T : finType} (s : {perm T}) :
  cycle_count s ≤ #|T|.
Proof.
rewrite /cycle_count /porbits.
exact: leq_imset_card.
Qed.

Under the identity permutation each porbit is the singleton {x}. Used in cycle_count_id.
Lemma porbit_id_singleton (T : finType) (x : T) :
  porbit (1 : {perm T}) x = [set x].
Proof.
apply/setP⇒ y; rewrite !inE.
apply/porbitP/eqP.
- by case⇒ i ->; rewrite expg1n perm1.
- by move⇒ ->; ∃ 0; rewrite expg1n perm1.
Qed.

The identity permutation on T has exactly #|T| cycles, one singleton per element (Stanley §1.3.1: each fixed point is a 1-cycle).
Lemma cycle_count_id (T : finType) :
  cycle_count (1 : {perm T}) = #|T|.
Proof.
rewrite /cycle_count /porbits.
rewrite -[in RHS](card_imset [pred x : T | true] set1_inj).
apply: eq_card ⇒ P; apply/imsetP/imsetP.
- case⇒ x _ →.
  by ∃ x; rewrite ?inE //; rewrite porbit_id_singleton.
- case⇒ x _ →.
  by ∃ x ⇒ //; rewrite porbit_id_singleton.
Qed.

End CycleBasic.


Row sum: summing stirling_c n k over all cycle counts k ≤ n recovers the total number of permutations of 'I_n. Mirrors eulerian_row_sum in eulerian.v.
Lemma stirling_c_row_sum n :
  \sum_(k < n.+1) stirling_c n k = #|{perm 'I_n}|.
Proof.
rewrite /stirling_c -sum1_card.
rewrite (partition_big (fun s : {perm 'I_n} ⇒ inord (cycle_count s) : 'I_n.+1)
                       xpredT) //=.
apply: eq_bigr ⇒ k _; rewrite -sum1_card; apply: eq_bigl ⇒ s; rewrite inE.
rewrite -val_eqE /= inordK //.
have := cycle_count_le s.
by rewrite card_ord.
Qed.

Row sum, factorial form: \sum_k c(n, k) = n!. Stanley's identity derived from stirling_c_row_sum via card_Sn.
Lemma stirling_c_row_sum_fact n :
  \sum_(k < n.+1) stirling_c n k = n`!.
Proof. by rewrite stirling_c_row_sum card_Sn. Qed.