Library mathcomp.fingroup.perm
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype tuple finfun bigop finset binomial.
From mathcomp Require Import fingroup.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
From mathcomp Require Import choice fintype tuple finfun bigop finset binomial.
From mathcomp Require Import fingroup.
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).
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).