Library perm

 This file contains the definition and properties associated to the group   
 of permutations of an arbitrary finite type.                               
     {perm T} == the type of permutations of a finite type T, i.e.,         
                 injective (finite) functions from T to T. Permutations     
                 coerce to CiC functions.                                   
         'S_n == the set of all permutations of 'I_n, i.e., of {0,.., n-1}  
  perm_on A u == u is a permutation with support A, i.e., u only displaces  
                 elements of A (u x != x implies x \in A).                  
    tperm x y == the transposition of x, y                                  
    aperm x s == the image of x under the action of the permutation s       
              := s x                                                        
   pcycle s x == the set of all elements that are in the same cycle of the  
                 permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...}        
    pcycles s == the set of all the cycles of the permutation s             
   (s : bool) == s is an odd permutation (the coercion is called odd_perm)  
      dpair u == u is a pair (x, y) of distinct objects (i.e., x != y)      
 lift_perm i j s == the permutation obtained by lifting s : 'S_n.-1 over    
                 (i |-> j), that maps i to j and lift i k to lift j (s k).  
 Canonical structures are defined allowing permutations to be an eqType,    
 choiceType, countType, finType, subType, finGroupType; permutations with   
 composition form a group, therefore inherit all generic group notations:   
 1 == identity permutation, * == composition, ^-1 == inverse permutation.   


Import GroupScope.

Section PermDefSection.

Variable T : finType.

Inductive perm_type : predArgType :=
  Perm (pval : {ffun T -> T}) & injectiveb pval.
Definition pval p := let: Perm f _ := p in f.
Definition perm_of of phant T := perm_type.
Identity Coercion type_of_perm : perm_of >-> perm_type.

Notation pT := (perm_of (Phant T)).

Canonical Structure perm_subType :=
  Eval hnf in [subType for pval by perm_type_rect].
Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
Canonical Structure perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
Canonical Structure perm_choiceType :=
  Eval hnf in ChoiceType perm_type perm_choiceMixin.
Definition perm_countMixin := [countMixin of perm_type by <:].
Canonical Structure perm_countType :=
  Eval hnf in CountType perm_type perm_countMixin.
Canonical Structure perm_subCountType :=
  Eval hnf in [subCountType of perm_type].
Definition perm_finMixin := [finMixin of perm_type by <:].
Canonical Structure perm_finType := Eval hnf in FinType perm_type perm_finMixin.
Canonical Structure perm_subFinType := Eval hnf in [subFinType of perm_type].

Canonical Structure perm_for_subType := Eval hnf in [subType of pT].
Canonical Structure perm_for_eqType := Eval hnf in [eqType of pT].
Canonical Structure perm_for_choiceType := Eval hnf in [choiceType of pT].
Canonical Structure perm_for_countType := Eval hnf in [countType of pT].
Canonical Structure perm_for_subCountType := Eval hnf in [subCountType of pT].
Canonical Structure perm_for_finType := Eval hnf in [finType of pT].
Canonical Structure perm_for_subFinType := Eval hnf in [subFinType of pT].

Lemma perm_proof : forall f : T -> T, injective f -> injectiveb (finfun f).

End PermDefSection.

Notation "{ 'perm' T }" := (perm_of (Phant T))
  (at level 0, format "{ 'perm' T }") : type_scope.



Notation "''S_' n" := {perm 'I_n}
  (at level 8, n at level 2, format "''S_' n").

Notation Local fun_of_perm_def := (fun T (u : perm_type T) => val u : T -> T).
Notation Local perm_def := (fun T f injf => Perm (@perm_proof T f injf)).

Module Type PermDefSig.
Parameter fun_of_perm : forall T, perm_type T -> T -> T.
Parameter perm : forall (T : finType) (f : T -> T), injective f -> {perm T}.
Axiom fun_of_permE : fun_of_perm = fun_of_perm_def.
Axiom permE : perm = perm_def.
End PermDefSig.

Module PermDef : PermDefSig.
Definition fun_of_perm := fun_of_perm_def.
Definition perm := perm_def.
Lemma fun_of_permE : fun_of_perm = fun_of_perm_def.

Lemma permE : perm = perm_def.

End PermDef.

Notation fun_of_perm := PermDef.fun_of_perm.
Notation "@ 'perm'" := (@PermDef.perm) (at level 10, format "@ 'perm'").
Notation perm := (@PermDef.perm _ _).
Canonical Structure fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
Canonical Structure perm_unlock := Unlockable PermDef.permE.
Coercion fun_of_perm : perm_type >-> Funclass.

Section Theory.

Variable T : finType.
Implicit Types s t : {perm T}.
Implicit Type S : {set T}.

Lemma permP : forall s t, s =1 t <-> s = t.

Lemma pvalE : forall s, pval s = s :> (T -> T).

Lemma permE : forall f f_inj, @perm T f f_inj =1 f.

Lemma perm_inj : forall s, injective s.

Implicit Arguments perm_inj [].
Hint Resolve perm_inj.

Lemma perm_onto : forall s, codom s =i predT.

Definition perm_one := perm (@inj_id T).

Lemma perm_invK : forall s, cancel (fun x => iinv (perm_onto s x)) s.

Definition perm_inv s := perm (can_inj (perm_invK s)).

Definition perm_mul s v := perm (inj_comp (perm_inj v) (perm_inj s)).

Lemma perm_oneP : left_id perm_one perm_mul.

Lemma perm_invP : left_inverse perm_one perm_inv perm_mul.

Lemma perm_mulP : associative perm_mul.

Definition perm_of_baseFinGroupMixin : FinGroup.mixin_of (perm_type T) :=
  FinGroup.Mixin perm_mulP perm_oneP perm_invP.
Canonical Structure perm_baseFinGroupType :=
  Eval hnf in BaseFinGroupType (perm_type T) perm_of_baseFinGroupMixin.
Canonical Structure perm_finGroupType :=
  @FinGroupType perm_baseFinGroupType perm_invP.

Canonical Structure perm_of_baseFinGroupType :=
  Eval hnf in [baseFinGroupType of {perm T}].
Canonical Structure perm_of_finGroupType :=
  Eval hnf in [finGroupType of {perm T} ].

Lemma perm1 : forall x, (1 : {perm T}) x = x.

Lemma permM : forall s t x, (s * t) x = t (s x).

Lemma permK : forall s, cancel s s^-1.

Lemma permKV : forall s, cancel s^-1 s.

Lemma permJ : forall s t x, (s ^ t) (t x) = t (s x).

Lemma permX : forall s x n, (s ^+ n) x = iter n s x.

Lemma im_permV : forall s S, s^-1 @: S = s @^-1: S.

Lemma preim_permV : forall s S, s^-1 @^-1: S = s @: S.

Definition perm_on S : pred {perm T} := fun s => [pred x | s x != x] \subset S.

Lemma perm_closed : forall S s x, perm_on S s -> (s x \in S) = (x \in S).

Lemma perm_on1 : forall H, perm_on H 1.

Lemma perm_onM : forall H s t, perm_on H s -> perm_on H t -> perm_on H (s * t).

Lemma out_perm : forall S u x, perm_on S u -> x \notin S -> u x = x.

Lemma im_perm_on : forall u S, perm_on S u -> u @: S = S.

Lemma tperm_proof : forall x y : T,
  involutive [fun z => z with x |-> y, y |-> x].

Definition tperm x y := perm (can_inj (tperm_proof x y)).

CoInductive tperm_spec (x y z : T) : T -> Type :=
  | TpermFirst of z = x : tperm_spec x y z y
  | TpermSecond of z = y : tperm_spec x y z x
  | TpermNone of z <> x & z <> y : tperm_spec x y z z.

Lemma tpermP : forall x y z, tperm_spec x y z (tperm x y z).

Lemma tpermL : forall x y : T, tperm x y x = y.

Lemma tpermR : forall x y : T, tperm x y y = x.

Lemma tpermD : forall x y z : T, x != z -> y != z -> tperm x y z = z.

Lemma tpermC : forall x y : T, tperm x y = tperm y x.

Lemma tperm1 : forall x : T, tperm x x = 1.

Lemma tpermK : forall x y : T, involutive (tperm x y).

Lemma tpermKg : forall x y : T, involutive (mulg (tperm x y)).

Lemma tpermV : forall x y : T, (tperm x y)^-1 = tperm x y.

Lemma tperm2 : forall x y : T, tperm x y * tperm x y = 1.

Lemma card_perm : forall A : {set T}, #|perm_on A| = (#|A|)`!.

End Theory.


Lemma inj_tperm : forall (T T' : finType) (f : T -> T') x y z,
  injective f -> f (tperm x y z) = tperm (f x) (f y) (f z).

Lemma tpermJ : forall (T : finType) x y (s : {perm T}),
  (tperm x y) ^ s = tperm (s x) (s y).

Section PermutationParity.

Variable T : finType.

Implicit Type s : {perm T}.
Implicit Types x y z : T.

 Note that pcycle s x is the orbit of x by <[s]> under the action aperm. 
 Hence, the pcycle lemmas below are special cases of more general lemmas 
 on orbits that will be stated in action.v.                              
   Defining pcycle directly here avoids a dependency of matrix.v on      
 action.v and hence morphism.v.                                          

Definition aperm x s := s x.
Definition pcycle s x := aperm x @: <[s]>.
Definition pcycles s := pcycle s @: T.
Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|pcycles s|.

Lemma apermE : forall x a, aperm x a = a x.

Lemma mem_pcycle : forall s i x, (s ^+ i) x \in pcycle s x.

Lemma pcycle_id : forall s x, x \in pcycle s x.

Lemma uniq_traject_pcycle : forall s x, uniq (traject s x #|pcycle s x|).

 improved #[s] to #|pcycle s x| 
Lemma pcycle_traject : forall s x, pcycle s x =i traject s x #|pcycle s x|.

Lemma iter_pcycle : forall s x, iter #|pcycle s x| s x = x.

Lemma eq_pcycle_mem : forall s x y,
  (pcycle s x == pcycle s y) = (x \in pcycle s y).

Lemma pcycle_sym : forall s x y, (x \in pcycle s y) = (y \in pcycle s x).

Lemma pcycle_perm : forall s i x, pcycle s ((s ^+ i) x) = pcycle s x.

Lemma ncycles_mul_tperm : forall s x y (t := tperm x y),
  #|pcycles (t * s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).

Lemma odd_perm1 : odd_perm 1 = false.

Lemma odd_mul_tperm : forall x y s,
  odd_perm (tperm x y * s) = (x != y) (+) odd_perm s.

Lemma odd_tperm : forall x y, odd_perm (tperm x y) = (x != y).

Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT].
Implicit Arguments dpair [eT].

Lemma prod_tpermP : forall s : {perm T},
  {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.

Lemma odd_perm_prod : forall ts,
  all dpair ts -> odd_perm (\prod_(t <- ts) tperm t.1 t.2) = odd (size ts).

Lemma odd_permM : {morph odd_perm : s1 s2 / s1 * s2 >-> s1 (+) s2}.

Lemma odd_permV : forall s, odd_perm s^-1 = odd_perm s.

Lemma odd_permJ : forall s1 s2, odd_perm (s1 ^ s2) = odd_perm s1.

End PermutationParity.

Coercion odd_perm : perm_type >-> bool.
Implicit Arguments dpair [eT].

Section LiftPerm.
 Somewhat more specialised constructs for permutations on ordinals. 

Variable n : nat.
Implicit Types i j : 'I_n.+1.
Implicit Types s t : 'S_n.

Definition lift_perm_fun i j s k :=
  if unlift i k is Some k' then lift j (s k') else j.

Lemma lift_permK : forall i j s,
  cancel (lift_perm_fun i j s) (lift_perm_fun j i s^-1).

Definition lift_perm i j s := perm (can_inj (lift_permK i j s)).

Lemma lift_perm_id : forall i j s, lift_perm i j s i = j.

Lemma lift_perm_lift : forall i j s k',
  lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.

Lemma lift_permM : forall i j k s t,
  lift_perm i j s * lift_perm j k t = lift_perm i k (s * t).

Lemma lift_perm1 : forall i, lift_perm i i 1 = 1.

Lemma lift_permV : forall i j s, (lift_perm i j s)^-1 = lift_perm j i s^-1.

Lemma odd_lift_perm : forall i j s,
  lift_perm i j s = odd i (+) odd j (+) s :> bool.

End LiftPerm.