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 morphism.
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 morphism.
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
cast_perm Emn s == the 'S_m permutation cast as a 'S_n permutation using
Emn : m = n
porbit 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, ...}.
porbits 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).
Sym S == the set of permutations with support S
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.
Arguments pval _ _%g.
Bind Scope group_scope with perm_type.
Bind Scope group_scope with perm_of.
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 permX_fix s x n : s x = x → (s ^+ n) x = 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 perm_onV H s : perm_on H s → perm_on H s^-1.
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 perm_on_id u S : perm_on S u → #|S| ≤ 1 → u = 1%g.
Lemma perm_onC (S1 S2 : {set T}) (u1 u2 : {perm T}) :
perm_on S1 u1 → perm_on S2 u2 →
[disjoint S1 & S2] →
commute u1 u2.
Lemma imset_perm1 (S : {set T}) : [set (1 : {perm T}) x | x in 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 tperm_on x y : perm_on [set x; y] (tperm x y).
Lemma card_perm A : #|perm_on A| = (#|A|)`!.
End Theory.
Arguments perm_inj {T s} [x1 x2] eq_sx12.
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 porbit s x is the orbit of x by < [s]> under the action aperm.
Hence, the porbit lemmas below are special cases of more general lemmas
on orbits that will be stated in action.v.
Defining porbit directly here avoids a dependency of matrix.v on
action.v and hence morphism.v.
Definition aperm x s := s x.
Definition porbit s x := aperm x @: <[s]>.
Definition porbits s := porbit s @: T.
Definition odd_perm (s : perm_type T) := odd #|T| (+) odd #|porbits s|.
Lemma apermE x s : aperm x s = s x.
Lemma mem_porbit s i x : (s ^+ i) x \in porbit s x.
Lemma porbit_id s x : x \in porbit s x.
Lemma card_porbit_neq0 s x : #|porbit s x| != 0.
Lemma uniq_traject_porbit s x : uniq (traject s x #|porbit s x|).
Lemma porbit_traject s x : porbit s x =i traject s x #|porbit s x|.
Lemma iter_porbit s x : iter #|porbit s x| s x = x.
Lemma eq_porbit_mem s x y : (porbit s x == porbit s y) = (x \in porbit s y).
Lemma porbit_sym s x y : (x \in porbit s y) = (y \in porbit s x).
Lemma porbit_perm s i x : porbit s ((s ^+ i) x) = porbit s x.
Lemma porbitPmin s x y :
y \in porbit s x → exists2 i, i < #[s] & y = (s ^+ i) x.
Lemma porbitP s x y :
reflect (∃ i, y = (s ^+ i) x) (y \in porbit s x).
Lemma porbitV s : porbit s^-1 =1 porbit s.
Lemma porbitsV s : porbits s^-1 = porbits s.
Lemma porbits_mul_tperm s x y : let t := tperm x y in
#|porbits (t × s)| + (x \notin porbit s y).*2 = #|porbits 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].
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.
Arguments dpair {eT}.
Section Symmetry.
Variables (T : finType) (S : {set T}).
Definition Sym : {set {perm T}} := [set s | perm_on S s].
Lemma Sym_group_set : group_set Sym.
Canonical Sym_group : {group {perm T}} := Group Sym_group_set.
Lemma card_Sym : #|Sym| = #|S|`!.
End Symmetry.
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.
Lemma card_Sn : #|'S_(n)| = 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.
Lemma permS0 : all_equal_to (1 : 'S_0).
Lemma permS1 : all_equal_to (1 : 'S_1).
Lemma permS01 n : n ≤ 1 → all_equal_to (1 : 'S_n).
Section CastSn.
Definition cast_perm m n (eq_mn : m = n) (s : 'S_m) :=
let: erefl in _ = n := eq_mn return 'S_n in s.
Lemma cast_perm_id n eq_n s : cast_perm eq_n s = s :> 'S_n.
Lemma cast_ord_permE m n eq_m_n (s : 'S_m) i :
@cast_ord m n eq_m_n (s i) = (cast_perm eq_m_n s) (cast_ord eq_m_n i).
Lemma cast_permE m n (eq_m_n : m = n) (s : 'S_m) (i : 'I_n) :
cast_perm eq_m_n s i = cast_ord eq_m_n (s (cast_ord (esym eq_m_n) i)).
Lemma cast_perm_comp m n p (eq_m_n : m = n) (eq_n_p : n = p) s :
cast_perm eq_n_p (cast_perm eq_m_n s) = cast_perm (etrans eq_m_n eq_n_p) s.
Lemma cast_permK m n eq_m_n :
cancel (@cast_perm m n eq_m_n) (cast_perm (esym eq_m_n)).
Lemma cast_permKV m n eq_m_n :
cancel (cast_perm (esym eq_m_n)) (@cast_perm m n eq_m_n).
Lemma cast_perm_sym m n (eq_m_n : m = n) s t :
s = cast_perm eq_m_n t → t = cast_perm (esym eq_m_n) s.
Lemma cast_perm_inj m n eq_m_n : injective (@cast_perm m n eq_m_n).
Lemma cast_perm_morphM m n eq_m_n :
{morph @cast_perm m n eq_m_n : x y / x × y >-> x × y}.
Canonical morph_of_cast_perm m n eq_m_n :=
@Morphism _ _ setT (cast_perm eq_m_n) (in2W (@cast_perm_morphM m n eq_m_n)).
Lemma isom_cast_perm m n eq_m_n : isom setT setT (@cast_perm m n eq_m_n).
End CastSn.