Library mathcomp.fingroup.perm
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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.
Set Implicit Arguments.
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 perm_subType := Eval hnf in [subType for pval].
Definition perm_eqMixin := Eval hnf in [eqMixin of perm_type by <:].
Canonical perm_eqType := Eval hnf in EqType perm_type perm_eqMixin.
Definition perm_choiceMixin := [choiceMixin of perm_type by <:].
Canonical perm_choiceType := Eval hnf in ChoiceType perm_type perm_choiceMixin.
Definition perm_countMixin := [countMixin of perm_type by <:].
Canonical perm_countType := Eval hnf in CountType perm_type perm_countMixin.
Canonical perm_subCountType := Eval hnf in [subCountType of perm_type].
Definition perm_finMixin := [finMixin of perm_type by <:].
Canonical perm_finType := Eval hnf in FinType perm_type perm_finMixin.
Canonical perm_subFinType := Eval hnf in [subFinType of perm_type].
Canonical perm_for_subType := Eval hnf in [subType of pT].
Canonical perm_for_eqType := Eval hnf in [eqType of pT].
Canonical perm_for_choiceType := Eval hnf in [choiceType of pT].
Canonical perm_for_countType := Eval hnf in [countType of pT].
Canonical perm_for_subCountType := Eval hnf in [subCountType of pT].
Canonical perm_for_finType := Eval hnf in [finType of pT].
Canonical perm_for_subFinType := Eval hnf in [subFinType of pT].
Lemma perm_proof (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 : ∀ T, perm_type T → T → T.
Parameter perm : ∀ (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 fun_of_perm_unlock := Unlockable PermDef.fun_of_permE.
Canonical perm_unlock := Unlockable PermDef.permE.
Coercion fun_of_perm : perm_type >-> Funclass.
Section Theory.
Variable T : finType.
Implicit Types (x y : T) (s t : {perm T}) (S : {set T}).
Lemma permP s t : s =1 t ↔ s = t.
Lemma pvalE s : pval s = s :> (T → T).
Lemma permE f f_inj : @perm T f f_inj =1 f.
Lemma perm_inj s : injective s.
Implicit Arguments perm_inj [].
Hint Resolve perm_inj.
Lemma perm_onto s : codom s =i predT.
Definition perm_one := perm (@inj_id T).
Lemma perm_invK s : cancel (fun x ⇒ iinv (perm_onto s x)) s.
Definition perm_inv s := perm (can_inj (perm_invK s)).
Definition perm_mul s t := perm (inj_comp (perm_inj t) (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 perm_baseFinGroupType :=
Eval hnf in BaseFinGroupType (perm_type T) perm_of_baseFinGroupMixin.
Canonical perm_finGroupType := @FinGroupType perm_baseFinGroupType perm_invP.
Canonical perm_of_baseFinGroupType :=
Eval hnf in [baseFinGroupType of {perm T}].
Canonical perm_of_finGroupType := Eval hnf in [finGroupType of {perm T} ].
Lemma perm1 x : (1 : {perm T}) x = x.
Lemma permM s t x : (s × t) x = t (s x).
Lemma permK s : cancel s s^-1.
Lemma permKV s : cancel s^-1 s.
Lemma permJ s t x : (s ^ t) (t x) = t (s x).
Lemma permX s x n : (s ^+ n) x = iter n s x.
Lemma im_permV s S : s^-1 @: S = s @^-1: S.
Lemma preim_permV 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 S s x : perm_on S s → (s x \in S) = (x \in S).
Lemma perm_on1 H : perm_on H 1.
Lemma perm_onM H s t : perm_on H s → perm_on H t → perm_on H (s × t).
Lemma out_perm S u x : perm_on S u → x \notin S → u x = x.
Lemma im_perm_on u S : perm_on S u → u @: S = S.
Lemma tperm_proof x y : 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 → 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 x y z : tperm_spec x y z (tperm x y z).
Lemma tpermL x y : tperm x y x = y.
Lemma tpermR x y : tperm x y y = x.
Lemma tpermD x y z : x != z → y != z → tperm x y z = z.
Lemma tpermC x y : tperm x y = tperm y x.
Lemma tperm1 x : tperm x x = 1.
Lemma tpermK x y : involutive (tperm x y).
Lemma tpermKg x y : involutive (mulg (tperm x y)).
Lemma tpermV x y : (tperm x y)^-1 = tperm x y.
Lemma tperm2 x y : tperm x y × tperm x y = 1.
Lemma card_perm A : #|perm_on A| = (#|A|)`!.
End Theory.
Lemma inj_tperm (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 (T : finType) x y (s : {perm T}) :
(tperm x y) ^ s = tperm (s x) (s y).
Lemma tuple_perm_eqP {T : eqType} {n} {s : seq T} {t : n.-tuple T} :
reflect (∃ p : 'S_n, s = [tuple tnth t (p i) | i < n]) (perm_eq s t).
Section PermutationParity.
Variable T : finType.
Implicit Types (s t u v : {perm T}) (x y z a b : 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 x s : aperm x s = s x.
Lemma mem_pcycle s i x : (s ^+ i) x \in pcycle s x.
Lemma pcycle_id s x : x \in pcycle s x.
Lemma uniq_traject_pcycle s x : uniq (traject s x #|pcycle s x|).
Lemma pcycle_traject s x : pcycle s x =i traject s x #|pcycle s x|.
Lemma iter_pcycle s x : iter #|pcycle s x| s x = x.
Lemma eq_pcycle_mem s x y : (pcycle s x == pcycle s y) = (x \in pcycle s y).
Lemma pcycle_sym s x y : (x \in pcycle s y) = (y \in pcycle s x).
Lemma pcycle_perm s i x : pcycle s ((s ^+ i) x) = pcycle s x.
Lemma ncycles_mul_tperm s x y : let t := tperm x y in
#|pcycles (t × s)| + (x \notin pcycle s y).*2 = #|pcycles s| + (x != y).
Lemma odd_perm1 : odd_perm 1 = false.
Lemma odd_mul_tperm x y s : odd_perm (tperm x y × s) = (x != y) (+) odd_perm s.
Lemma odd_tperm 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 s :
{ts : seq (T × T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}.
Lemma odd_perm_prod 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 s : odd_perm s^-1 = odd_perm s.
Lemma odd_permJ 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 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 i j s : lift_perm i j s i = j.
Lemma lift_perm_lift i j s k' :
lift_perm i j s (lift i k') = lift j (s k') :> 'I_n.+1.
Lemma lift_permM i j k s t :
lift_perm i j s × lift_perm j k t = lift_perm i k (s × t).
Lemma lift_perm1 i : lift_perm i i 1 = 1.
Lemma lift_permV i j s : (lift_perm i j s)^-1 = lift_perm j i s^-1.
Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.
End LiftPerm.