Library mathcomp_eulerian.cycles_rec

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

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

Section H1.
Variable n : nat.
Variable s : {perm 'I_n}.

Iterating perm.lift_perm ord_max ord_max s at ord_max stays at ord_max. Used in porbit_lift_perm_id_max.

Lemma lift_perm_id_iter i :
((perm.lift_perm ord_max ord_max s) ^+ i)%g ord_max = ord_max.
Proof.
elim: i ⇒ [|i IH]; first by rewrite expg0 perm1.
by rewrite expgSr permM IH perm.lift_perm_id.
Qed.

The porbit of ord_max under perm.lift_perm ord_max ord_max s is the singleton {ord_max}.

Lemma porbit_lift_perm_id_max :
porbit (perm.lift_perm ord_max ord_max s) ord_max = [set ord_max].
Proof.
apply/setP⇒ y; rewrite !inE.
apply/porbitP/eqP.
- by case⇒ i ->; rewrite lift_perm_id_iter.
- by move⇒ ->; ∃ 0; rewrite expg0 perm1.
Qed.

Iteration on lifted points commutes with lift ord_max: applying (perm.lift_perm ord_max ord_max s)^+i at lift ord_max k is the lift of (s^+i) k.

Lemma lift_perm_id_iter_lift i (k : 'I_n) :
((perm.lift_perm ord_max ord_max s) ^+ i)%g (lift ord_max k)
= lift ord_max ((s ^+ i)%g k).
Proof.
elim: i k ⇒ [|i IH] k; first by rewrite !expg0 !perm1.
by rewrite !expgSr !permM IH perm.lift_perm_lift.
Qed.

The porbit of lift ord_max k under the lifted perm is the lift ord_max-image of the porbit of k under s.

Lemma porbit_lift_perm_id_lift (k : 'I_n) :
  porbit (perm.lift_perm ord_max ord_max s) (lift ord_max k)
  = (lift ord_max) @: (porbit s k).
Proof.
apply/setP⇒ y; apply/porbitP/imsetP.
- case⇒ i ->; rewrite lift_perm_id_iter_lift.
  by ∃ ((s ^+ i)%g k); rewrite // mem_porbit.
- case⇒ z /porbitP[i ->] →.
  by ∃ i; rewrite lift_perm_id_iter_lift.
Qed.

Decomposition of porbits (perm.lift_perm ord_max ord_max s) into the singleton orbit {ord_max} and the lift ord_max-images of the orbits of s. Used in cycle_count_lift_perm_id.

Lemma porbits_lift_perm_id :
  porbits (perm.lift_perm ord_max ord_max s)
  = ([set [set ord_max] : {set 'I_n.+1}] :|:
     [set (lift ord_max) @: (P : {set 'I_n}) | P in porbits s])%SET.
Proof.
apply/setP⇒ P; rewrite !inE.
apply/imsetP/orP.
- case⇒ y _ →.
  case: (unliftP ord_max y) ⇒ [k → | ->].
  + right; apply/imsetP.
    ∃ (porbit s k); first by apply/imsetP; ∃ k.
    by rewrite porbit_lift_perm_id_lift.
  + by left; rewrite porbit_lift_perm_id_max eqxx.
- case.
  + move⇒ /eqP ->; ∃ ord_max ⇒ //.
    by rewrite porbit_lift_perm_id_max.
  + case/imsetP⇒ Q /imsetP[k _ ->] →.
    ∃ (lift ord_max k) ⇒ //.
    by rewrite porbit_lift_perm_id_lift.
Qed.

H1 proper: extending s with ord_max as a fixed point adds exactly one cycle. Building block for the j = ord_max class of the Stirling fiber bijection (see stirling_fiber.v).

Lemma cycle_count_lift_perm_id :
  cycle_count (perm.lift_perm ord_max ord_max s) = (cycle_count s).+1.
Proof.
rewrite /cycle_count porbits_lift_perm_id cardsU1.
rewrite (card_imset _ _) /=; last first.
  move⇒ P Q /setP eqfPQ; apply/setP⇒ x.
  by have := eqfPQ (lift ord_max x); rewrite !(mem_imset _ _ lift_inj).
have not_in : [set ord_max] \notin
  [set (lift ord_max) @: (P : {set 'I_n}) | P in porbits s].
  apply/imsetP⇒ [[Q QinP /setP HQ]].
  have := HQ ord_max; rewrite inE eqxx /= ⇒ /esym.
  case/imsetP⇒ k _ /eqP.
  by rewrite (negbTE (neq_lift _ _)).
by rewrite not_in add1n.
Qed.

End H1.