Library mathcomp.fingroup.perm
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 HB Require Import structures.
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 := perm_type.
Identity Coercion type_of_perm : perm_of >-> perm_type.
Lemma perm_proof (f : T → T) : injective f → injectiveb (finfun f).
End PermDefSection.
Arguments perm_of T%type.
Notation "{ 'perm' T }" := (perm_of 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").
Canonical perm_unlock := Unlockable perm.unlock.
Canonical fun_of_perm_unlock := Unlockable fun_of_perm.unlock.
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.
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).
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).
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 (T : finType) x (s : {perm T}) := s x.
Canonical porbit_unlockable := Unlockable porbit.unlock.
Definition porbits (T : finType) (s : {perm T}) := porbit s @: T.
Section PermutationParity.
Variable T : finType.
Implicit Types (s t u v : {perm T}) (x y z a b : 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 porbit_setP s t x : porbit s x =i porbit t x ↔ porbit s x = porbit t x.
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.
Canonical porbit_unlockable := Unlockable porbit.unlock.
Definition porbits (T : finType) (s : {perm T}) := porbit s @: T.
Section PermutationParity.
Variable T : finType.
Implicit Types (s t u v : {perm T}) (x y z a b : 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 porbit_setP s t x : porbit s x =i porbit t x ↔ porbit s x = porbit t x.
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.