- -

Library mathcomp.fingroup.perm

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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").
- -
- -
-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.
- Hint Resolve perm_inj : core.
- -
-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)).
- -
-Variant 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.
- -
- -
-

- -

- Shorthand for using a permutation to reindex a bigop. -

-Notation reindex_perm s := (reindex_inj (@perm_inj _ s)).
- -
-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_permP {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 ].
- -
-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.
- -
-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.
- -
- -
-Notation tuple_perm_eqP :=
-  (deprecate tuple_perm_eqP tuple_permP) (only parsing).
- -
-