Library Combi.SymGroup.presentSn: The Coxeter Presentation of the Symmetric Group
The Coxeter Presentation of the Symmetric Group
- compute the size-lexicographically minimal reduced word of a permutation
- straighten a word to the previous reduced word.
- 's_i == the i-th elementary transposition. It is of type 'S_n.+1 where n is inferred from the context. i is an integer smaller than n (otherwise eltr i is the identity)
- invset s == the set of inversion of s
- Delta == the set of pair (i, j) such that 0 <= i < j < n.+1; n is infered from the context
- is_invset IS == IS is the inversion set of a permutation, that is subdiagonal transitive and co-transitive
- length s == the number of inversion of s we show latter that this is the Coxeter length of s
- rsymrel IS == the reflexive and antisymmetric closure of the binary relation associated to the inversion set IS
- perm_of_invset IS == the permutation whose inversion set is IS
- c \is a code == c is a list such that c_i <= i.
- wordcd c == for a code c the list 0, 1-c1..1, 2-c2..2, ..
- is_code_of_size c n == the predicate c is a code of size n
- enum_codesz n == a list enumerating all the code of size n
- codesz n == sigma type for codes of size n, canonically a finType
- cocode s == the recursively defined Lehmer code of s^-1
- canword s == the canonical reduced word for s as a seq 'I_n
- prods_codesz c == the product eltr i associated to the code c that is for i <- wordcd c. Lemma prods_codesz_bij shows that it is a bijection from codesz n.+1 to 'S_n.+1.
- w \is reduced == w is a word of size length 's_[w].
- braid_aba == the braid rewriting rule a a.+1 a == a.+1 a a.+1
- braidC == the braid rewriting rule a b == b a if |b - a| > 1
- braidrule == the union of the two previous rules
- braidcongr == the braid monoid congruence generated by braidrule
- braidclass s == the braid monoid class of s
- a =Br b == a and b are equivalent under the braid congruence
- reduce u v == u reduces to v using the rule [:: i i] -> [::]
- braidred u v == either u =Br v or reduce u v
- inscode c i == the insertion the letter i in the code c. If c is the code for the permutation s then it is the code for the permutation s * 's_i
- path_catl p w == append w to all the sequences of p that is [seq v ++ w | v <- p]
- straighten w == the straigtened reduced word equivalent to w
- relat_Sn n g == if g : nat -> gT for a finGroupType gt. A
proposition which asserts that the relation of the symmetric
group holds for the g i denoted 'g_i. Namely
- forall i, i < n -> 'g_i^+2 = 1
- forall i, i.+1 < n -> 'g_i * 'g_i.+1 * 'g_i = 'g_i.+1 * 'g_i * 'g_i.+1
- forall i j, i.+1 < j < n -> 'g_i * 'g_j = 'g_j * 'g_i
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup perm morphism presentation.
From mathcomp Require Import ssralg poly ssrint.
Require Import permcomp tools permuted combclass congr.
Set Implicit Arguments.
Section SRel.
Variable T : finType.
Implicit Type (S A B : {set T * T}).
Definition srel S := [rel x y : T | (x, y) \in S].
Lemma srelE S1 S2 : srel S1 =2 srel S2 -> S1 = S2.
Definition tclosure A : {set T * T} :=
[set p | (p.1 != p.2) && (connect (srel A) p.1 p.2)].
Lemma tclosure_sub A B :
A \subset B -> transitive (srel B) -> tclosure A \subset B.
End SRel.
Notation "''SG_' n" := [set: 'S_n]
(at level 8, n at level 2, format "''SG_' n").
Reserved Notation "''s_' i"
(at level 8, i at level 2, format "''s_' i").
Reserved Notation "''s_' [ w ] "
(at level 8, w at level 100, format "''s_' [ w ]").
#[local] Reserved Notation "''II_' n" (at level 8, n at level 2).
#[local] Reserved Notation "a =Br b" (at level 70).
#[local] Reserved Notation "''I[' a '..' b ']'" (at level 0, a, b at level 2).
Lemma ieqi1F i : (i == i.+1) = false.
Lemma ieqi2F i : (i == i.+2) = false.
Lemma i1eqiF i : (i.+1 == i) = false.
Lemma i2eqiF i : (i.+2 == i) = false.
Lemma inordi n i : i < n -> (@inord n i = i :> nat).
Lemma inordi1 n i : i < n -> (@inord n i.+1 = i.+1 :> nat).
Lemma inord1i n i : i.+1 < n -> (@inord n i = i :> nat).
Lemma inordi_neq_i1 n i : i < n -> (@inord n i != @inord n i.+1).
Definition trivSimpl := (eq_refl, eqSS, ieqi1F, ieqi2F, i1eqiF, i2eqiF).
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup perm morphism presentation.
From mathcomp Require Import ssralg poly ssrint.
Require Import permcomp tools permuted combclass congr.
Set Implicit Arguments.
Section SRel.
Variable T : finType.
Implicit Type (S A B : {set T * T}).
Definition srel S := [rel x y : T | (x, y) \in S].
Lemma srelE S1 S2 : srel S1 =2 srel S2 -> S1 = S2.
Definition tclosure A : {set T * T} :=
[set p | (p.1 != p.2) && (connect (srel A) p.1 p.2)].
Lemma tclosure_sub A B :
A \subset B -> transitive (srel B) -> tclosure A \subset B.
End SRel.
Notation "''SG_' n" := [set: 'S_n]
(at level 8, n at level 2, format "''SG_' n").
Reserved Notation "''s_' i"
(at level 8, i at level 2, format "''s_' i").
Reserved Notation "''s_' [ w ] "
(at level 8, w at level 100, format "''s_' [ w ]").
#[local] Reserved Notation "''II_' n" (at level 8, n at level 2).
#[local] Reserved Notation "a =Br b" (at level 70).
#[local] Reserved Notation "''I[' a '..' b ']'" (at level 0, a, b at level 2).
Lemma ieqi1F i : (i == i.+1) = false.
Lemma ieqi2F i : (i == i.+2) = false.
Lemma i1eqiF i : (i.+1 == i) = false.
Lemma i2eqiF i : (i.+2 == i) = false.
Lemma inordi n i : i < n -> (@inord n i = i :> nat).
Lemma inordi1 n i : i < n -> (@inord n i.+1 = i.+1 :> nat).
Lemma inord1i n i : i.+1 < n -> (@inord n i = i :> nat).
Lemma inordi_neq_i1 n i : i < n -> (@inord n i != @inord n i.+1).
Definition trivSimpl := (eq_refl, eqSS, ieqi1F, ieqi2F, i1eqiF, i2eqiF).
Section Codes.
Definition code := [qualify a c : seq nat |
all (fun i => nth 0 c i <= i) (iota 0 (size c)) ].
Definition wordcd (c : seq nat) : seq nat :=
flatten [seq rev (iota (i - nth 0 c i) (nth 0 c i)) | i <- iota 0 (size c)].
Lemma size_wordcd c : size (wordcd c) = sumn c.
Lemma is_codeP c :
reflect (forall i, i < size c -> nth 0 c i <= i) (c \is a code).
Lemma is_code_rcons c i : i <= size c -> c \is a code -> rcons c i \is a code.
Lemma is_code_rconsK c i : rcons c i \is a code -> c \is a code.
Lemma code_ltn_size c : c \is a code -> all (gtn (size c)) c.
Lemma wordcd_ltn c :
c \is a code -> all (gtn (size c).-1) (wordcd c).
Lemma insub_wordcdK n c :
c \is a code -> size c <= n.+1 ->
[seq (i : nat) | i : 'I_n <- pmap insub (wordcd c)] = wordcd c.
Definition is_code_of_size n c := (c \is a code) && (size c == n).
Fixpoint enum_codesz n :=
if n is n'.+1 then
flatten [seq [seq rcons c i | c <- enum_codesz n'] | i <- iota 0 n]
else [:: [::]].
Lemma enum_codeszP n : all (is_code_of_size n) (enum_codesz n).
Lemma enum_codesz_countE n c :
is_code_of_size n c -> count_mem c (enum_codesz n) = 1.
Definition code := [qualify a c : seq nat |
all (fun i => nth 0 c i <= i) (iota 0 (size c)) ].
Definition wordcd (c : seq nat) : seq nat :=
flatten [seq rev (iota (i - nth 0 c i) (nth 0 c i)) | i <- iota 0 (size c)].
Lemma size_wordcd c : size (wordcd c) = sumn c.
Lemma is_codeP c :
reflect (forall i, i < size c -> nth 0 c i <= i) (c \is a code).
Lemma is_code_rcons c i : i <= size c -> c \is a code -> rcons c i \is a code.
Lemma is_code_rconsK c i : rcons c i \is a code -> c \is a code.
Lemma code_ltn_size c : c \is a code -> all (gtn (size c)) c.
Lemma wordcd_ltn c :
c \is a code -> all (gtn (size c).-1) (wordcd c).
Lemma insub_wordcdK n c :
c \is a code -> size c <= n.+1 ->
[seq (i : nat) | i : 'I_n <- pmap insub (wordcd c)] = wordcd c.
Definition is_code_of_size n c := (c \is a code) && (size c == n).
Fixpoint enum_codesz n :=
if n is n'.+1 then
flatten [seq [seq rcons c i | c <- enum_codesz n'] | i <- iota 0 n]
else [:: [::]].
Lemma enum_codeszP n : all (is_code_of_size n) (enum_codesz n).
Lemma enum_codesz_countE n c :
is_code_of_size n c -> count_mem c (enum_codesz n) = 1.
Section FinType.
Variable n : nat.
Structure codesz : Set :=
CodeSZ {cdval :> seq nat; _ : (cdval \is a code) && (size cdval == n)}.
Implicit Type (c : codesz).
Lemma codeszP c : val c \is a code.
Lemma size_codesz c : size c = n.
Lemma enum_codeszE : map val (enum {:codesz}) = enum_codesz n.
End FinType.
Lemma card_codesz n : #|{:codesz n}| = n`!.
End Codes.
#[export] Hint Resolve codeszP : core.
Import GroupScope.
Variable n : nat.
Structure codesz : Set :=
CodeSZ {cdval :> seq nat; _ : (cdval \is a code) && (size cdval == n)}.
Implicit Type (c : codesz).
Lemma codeszP c : val c \is a code.
Lemma size_codesz c : size c = n.
Lemma enum_codeszE : map val (enum {:codesz}) = enum_codesz n.
End FinType.
Lemma card_codesz n : #|{:codesz n}| = n`!.
End Codes.
#[export] Hint Resolve codeszP : core.
Import GroupScope.
Section Transp.
Variable T : finType.
Implicit Types (x y z t : T).
Lemma tperm_braid x y z :
x != y -> y != z ->
tperm x y * tperm y z * tperm x y = tperm y z * tperm x y * tperm y z.
Lemma tpermC x y a b :
x != a -> y != a -> x != b -> y != b ->
tperm x y * tperm a b = tperm a b * tperm x y.
End Transp.
Section MaxPerm.
Context {n : nat}.
Definition maxperm : 'S_n := perm (@rev_ord_inj n).
Lemma maxpermK : involutive maxperm.
Lemma maxpermV : maxperm^-1 = maxperm.
End MaxPerm.
#[local] Notation "''II_' n" := ('I_n * 'I_n)%type.
Variable T : finType.
Implicit Types (x y z t : T).
Lemma tperm_braid x y z :
x != y -> y != z ->
tperm x y * tperm y z * tperm x y = tperm y z * tperm x y * tperm y z.
Lemma tpermC x y a b :
x != a -> y != a -> x != b -> y != b ->
tperm x y * tperm a b = tperm a b * tperm x y.
End Transp.
Section MaxPerm.
Context {n : nat}.
Definition maxperm : 'S_n := perm (@rev_ord_inj n).
Lemma maxpermK : involutive maxperm.
Lemma maxpermV : maxperm^-1 = maxperm.
End MaxPerm.
#[local] Notation "''II_' n" := ('I_n * 'I_n)%type.
Section InvSet.
Context {n : nat}.
Implicit Type (p : 'II_n) (IS S : {set 'II_n}).
Implicit Type s t : 'S_n.
Definition Delta : {set 'II_n} := [set p : 'II_n | (p.1 < p.2)].
Definition invset s : {set 'II_n} :=
[set p : 'II_n | (p.1 < p.2) && (s p.1 > s p.2) ].
Definition rsymrel IS :=
[rel i j : 'I_n |
[|| (i == j), (j, i) \in IS | (i < j) && ((i, j) \notin IS)]].
Definition length s := #|invset s|.
Variant is_invset IS : Prop :=
IsInvset of IS \subset Delta
& transitive (srel IS)
& transitive (srel (Delta :\: IS)).
Lemma mem_Delta i j : (i, j) \in Delta = (i < j).
Lemma DeltaP i j : (i, j) \in Delta -> (i < j).
Lemma card_Delta : #|Delta| = 'C(n, 2).
Lemma is_invset_Delta IS : is_invset IS -> IS \subset Delta.
Lemma transitive_DeltaI1 IS :
(transitive (srel (Delta :\: IS))) <->
(forall i j k : 'I_n,
i < j < k -> (i, k) \in IS -> ((i, j) \in IS \/ (j, k) \in IS)).
Lemma invset_Delta s : invset s \subset Delta.
Lemma invset_permV s :
invset s^-1 = [set (s (p.2), s (p.1)) | p in invset s].
Lemma invsetP s : is_invset (invset s).
Lemma invset_maxperm : invset (@maxperm n) = Delta.
Lemma invset_maxpermMr s : invset (s * maxperm) = Delta :\: invset s.
Lemma invset_maxpermMl s :
invset (maxperm * s) =
Delta :\: [set (maxperm p.2, maxperm p.1) | p in invset s].
Lemma rsymrel_refl IS : reflexive (rsymrel IS).
Lemma rsymrel_anti IS :
IS \subset Delta -> antisymmetric (rsymrel IS).
Lemma rsymrel_trans IS : is_invset IS -> transitive (rsymrel IS).
Lemma rsymrel_total (IS : {set 'II_n}) :
IS \subset Delta -> total (rsymrel IS).
Lemma rsym_invset_refl s : reflexive (rsymrel (invset s)).
Lemma rsym_invset_anti s : antisymmetric (rsymrel (invset s)).
Lemma rsym_invset_trans s : transitive (rsymrel (invset s)).
Lemma rsym_invset_total s : total (rsymrel (invset s)).
Lemma perm_of_relP (r : rel 'I_n) :
injective (fun i : 'I_n => nth i (sort r (enum 'I_n)) i).
Definition perm_of_invset IS :=
(perm (@perm_of_relP (rsymrel IS)))^-1.
Lemma rsym_invsetP s :
sorted (rsymrel (invset s)) [seq s^-1 i | i : 'I_n].
Lemma invsetK : cancel invset perm_of_invset.
Theorem invset_inj : injective invset.
Theorem perm_of_invsetK (IS : {set 'II_n}) :
is_invset IS -> invset (perm_of_invset IS) = IS.
Lemma length1 : length 1 = 0.
Lemma lengthV s : length s^-1 = length s.
Lemma length_max s : length s <= 'C(n, 2).
Lemma length_maxperm : length (@maxperm n) = 'C(n, 2).
Lemma length_maxpermE s : length s = 'C(n, 2) -> s = (@maxperm n).
Lemma length_maxpermMr s : length (s * maxperm) = 'C(n, 2) - length s.
Lemma length_maxpermMl s : length (maxperm * s) = 'C(n, 2) - length s.
End InvSet.
Section ElemTransp.
Variable n0 : nat.
Notation n := n0.+1.
Definition eltr i : 'S_n0.+1 := tperm (inord i) (inord i.+1).
Notation "''s_' i" := (eltr i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Implicit Type s t : 'S_n.
Lemma eltrV i : 's_i^-1 = 's_i.
Lemma eltrK i : involutive 's_i.
Lemma eltr2 i : 's_i * 's_i = 1.
Lemma eltr_braid i :
i.+1 < n0 -> 's_i * 's_i.+1 * 's_i = 's_i.+1 * 's_i * 's_i.+1.
Lemma eltr_comm i j :
i.+1 < j < n0 -> 's_i * 's_j = 's_j * 's_i.
#[local] Lemma eltrL_ord (i : 'I_n) : 's_i i = inord i.+1.
#[local] Lemma eltrR_ord (i : 'I_n) : 's_i (inord i.+1) = i.
#[local] Lemma eltrD_ord (i j : 'I_n) : i != j -> inord i.+1 != j -> 's_i j = j.
Definition eltrL := (eltrL_ord, tpermL).
Definition eltrR := (eltrR_ord, tpermR).
Definition eltrD := (eltrD_ord, tpermD).
Lemma prods_iota_mi (m : 'I_n) i :
i <= m -> 's_[iota (m - i) i] (inord (m - i)) = m.
Lemma prods_iota_ltmi i (m u : 'I_n) :
u < m - i -> 's_[(iota (m - i) i)] u = u.
Lemma cycleij_j (i j : 'I_n) :
i <= j -> 's_[index_iota i j] i = j.
Lemma cycleij_lt (i j k : 'I_n) :
i <= j -> k < i -> 's_[index_iota i j] k = k.
Lemma cycleij_gt (i j : nat) (k : 'I_n) :
j < k -> 's_[index_iota i j] k = k.
Lemma cycleij_inS i (j k : 'I_n) :
i <= k < j -> 's_[index_iota i j] (inord k.+1) = k.
Lemma cycleij_in i (j k : 'I_n) :
i < k <= j -> 's_[index_iota i j] k = (inord k.-1).
Lemma prodsK w : 's_[w] * 's_[rev w] = 1.
Lemma prodsV w : 's_[rev w] = 's_[w]^-1.
Lemma odd_eltr i : (i < n0)%N -> odd_perm 's_i.
End ElemTransp.
Section PermOfInvSetEltr.
Variable n0 : nat.
Local Notation n := n0.+1.
Implicit Type s t : 'S_n.
Notation "''s_' i" := (eltr _ i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Lemma eltr_exchange i (a b : 'I_n) :
i < n0 -> a < b -> 's_i a < 's_i b = (i != a) || (i.+1 != b).
Lemma invset_eltrL s (i : 'I_n) :
i < n0 -> s i < s (inord i.+1) ->
invset ('s_i * s) =
(i, inord i.+1) |: [set ('s_i p.1, 's_i p.2) | p in invset s].
Lemma invset_eltrR s (i : 'I_n) :
i < n0 -> s^-1 i < s^-1 (inord i.+1) ->
invset (s * 's_i) = (s^-1 i, s^-1 (inord i.+1)) |: invset s.
End PermOfInvSetEltr.
Arguments Delta {n}.
Section Length.
Variable n0 : nat.
Notation n := n0.+1.
Notation "''s_' i" := (eltr n0 i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Implicit Type s t u : 'S_n.
Context {n : nat}.
Implicit Type (p : 'II_n) (IS S : {set 'II_n}).
Implicit Type s t : 'S_n.
Definition Delta : {set 'II_n} := [set p : 'II_n | (p.1 < p.2)].
Definition invset s : {set 'II_n} :=
[set p : 'II_n | (p.1 < p.2) && (s p.1 > s p.2) ].
Definition rsymrel IS :=
[rel i j : 'I_n |
[|| (i == j), (j, i) \in IS | (i < j) && ((i, j) \notin IS)]].
Definition length s := #|invset s|.
Variant is_invset IS : Prop :=
IsInvset of IS \subset Delta
& transitive (srel IS)
& transitive (srel (Delta :\: IS)).
Lemma mem_Delta i j : (i, j) \in Delta = (i < j).
Lemma DeltaP i j : (i, j) \in Delta -> (i < j).
Lemma card_Delta : #|Delta| = 'C(n, 2).
Lemma is_invset_Delta IS : is_invset IS -> IS \subset Delta.
Lemma transitive_DeltaI1 IS :
(transitive (srel (Delta :\: IS))) <->
(forall i j k : 'I_n,
i < j < k -> (i, k) \in IS -> ((i, j) \in IS \/ (j, k) \in IS)).
Lemma invset_Delta s : invset s \subset Delta.
Lemma invset_permV s :
invset s^-1 = [set (s (p.2), s (p.1)) | p in invset s].
Lemma invsetP s : is_invset (invset s).
Lemma invset_maxperm : invset (@maxperm n) = Delta.
Lemma invset_maxpermMr s : invset (s * maxperm) = Delta :\: invset s.
Lemma invset_maxpermMl s :
invset (maxperm * s) =
Delta :\: [set (maxperm p.2, maxperm p.1) | p in invset s].
Lemma rsymrel_refl IS : reflexive (rsymrel IS).
Lemma rsymrel_anti IS :
IS \subset Delta -> antisymmetric (rsymrel IS).
Lemma rsymrel_trans IS : is_invset IS -> transitive (rsymrel IS).
Lemma rsymrel_total (IS : {set 'II_n}) :
IS \subset Delta -> total (rsymrel IS).
Lemma rsym_invset_refl s : reflexive (rsymrel (invset s)).
Lemma rsym_invset_anti s : antisymmetric (rsymrel (invset s)).
Lemma rsym_invset_trans s : transitive (rsymrel (invset s)).
Lemma rsym_invset_total s : total (rsymrel (invset s)).
Lemma perm_of_relP (r : rel 'I_n) :
injective (fun i : 'I_n => nth i (sort r (enum 'I_n)) i).
Definition perm_of_invset IS :=
(perm (@perm_of_relP (rsymrel IS)))^-1.
Lemma rsym_invsetP s :
sorted (rsymrel (invset s)) [seq s^-1 i | i : 'I_n].
Lemma invsetK : cancel invset perm_of_invset.
Theorem invset_inj : injective invset.
Theorem perm_of_invsetK (IS : {set 'II_n}) :
is_invset IS -> invset (perm_of_invset IS) = IS.
Lemma length1 : length 1 = 0.
Lemma lengthV s : length s^-1 = length s.
Lemma length_max s : length s <= 'C(n, 2).
Lemma length_maxperm : length (@maxperm n) = 'C(n, 2).
Lemma length_maxpermE s : length s = 'C(n, 2) -> s = (@maxperm n).
Lemma length_maxpermMr s : length (s * maxperm) = 'C(n, 2) - length s.
Lemma length_maxpermMl s : length (maxperm * s) = 'C(n, 2) - length s.
End InvSet.
Section ElemTransp.
Variable n0 : nat.
Notation n := n0.+1.
Definition eltr i : 'S_n0.+1 := tperm (inord i) (inord i.+1).
Notation "''s_' i" := (eltr i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Implicit Type s t : 'S_n.
Lemma eltrV i : 's_i^-1 = 's_i.
Lemma eltrK i : involutive 's_i.
Lemma eltr2 i : 's_i * 's_i = 1.
Lemma eltr_braid i :
i.+1 < n0 -> 's_i * 's_i.+1 * 's_i = 's_i.+1 * 's_i * 's_i.+1.
Lemma eltr_comm i j :
i.+1 < j < n0 -> 's_i * 's_j = 's_j * 's_i.
#[local] Lemma eltrL_ord (i : 'I_n) : 's_i i = inord i.+1.
#[local] Lemma eltrR_ord (i : 'I_n) : 's_i (inord i.+1) = i.
#[local] Lemma eltrD_ord (i j : 'I_n) : i != j -> inord i.+1 != j -> 's_i j = j.
Definition eltrL := (eltrL_ord, tpermL).
Definition eltrR := (eltrR_ord, tpermR).
Definition eltrD := (eltrD_ord, tpermD).
Lemma prods_iota_mi (m : 'I_n) i :
i <= m -> 's_[iota (m - i) i] (inord (m - i)) = m.
Lemma prods_iota_ltmi i (m u : 'I_n) :
u < m - i -> 's_[(iota (m - i) i)] u = u.
Lemma cycleij_j (i j : 'I_n) :
i <= j -> 's_[index_iota i j] i = j.
Lemma cycleij_lt (i j k : 'I_n) :
i <= j -> k < i -> 's_[index_iota i j] k = k.
Lemma cycleij_gt (i j : nat) (k : 'I_n) :
j < k -> 's_[index_iota i j] k = k.
Lemma cycleij_inS i (j k : 'I_n) :
i <= k < j -> 's_[index_iota i j] (inord k.+1) = k.
Lemma cycleij_in i (j k : 'I_n) :
i < k <= j -> 's_[index_iota i j] k = (inord k.-1).
Lemma prodsK w : 's_[w] * 's_[rev w] = 1.
Lemma prodsV w : 's_[rev w] = 's_[w]^-1.
Lemma odd_eltr i : (i < n0)%N -> odd_perm 's_i.
End ElemTransp.
Section PermOfInvSetEltr.
Variable n0 : nat.
Local Notation n := n0.+1.
Implicit Type s t : 'S_n.
Notation "''s_' i" := (eltr _ i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Lemma eltr_exchange i (a b : 'I_n) :
i < n0 -> a < b -> 's_i a < 's_i b = (i != a) || (i.+1 != b).
Lemma invset_eltrL s (i : 'I_n) :
i < n0 -> s i < s (inord i.+1) ->
invset ('s_i * s) =
(i, inord i.+1) |: [set ('s_i p.1, 's_i p.2) | p in invset s].
Lemma invset_eltrR s (i : 'I_n) :
i < n0 -> s^-1 i < s^-1 (inord i.+1) ->
invset (s * 's_i) = (s^-1 i, s^-1 (inord i.+1)) |: invset s.
End PermOfInvSetEltr.
Arguments Delta {n}.
Section Length.
Variable n0 : nat.
Notation n := n0.+1.
Notation "''s_' i" := (eltr n0 i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Implicit Type s t u : 'S_n.
Lemma length_add1L s (i : 'I_n) :
i < n0 -> s i < s (inord i.+1) -> length ('s_i * s) = (length s).+1.
Lemma length_sub1L s (i : 'I_n) :
i < n0 -> s i > s (inord i.+1) -> length s = (length ('s_i * s)).+1.
Lemma length_descL s (i : 'I_n) :
i < n0 -> (s i < s (inord i.+1)) = (length ('s_i * s) > length s).
Lemma length_add1R s (i : 'I_n) :
i < n0 -> s^-1 i < s^-1 (inord i.+1) -> length (s * 's_i) = (length s).+1.
Lemma length_sub1R s (i : 'I_n) :
i < n0 -> s^-1 i > s^-1 (inord i.+1) -> length s = (length (s * 's_i)).+1.
Lemma length_descR s (i : 'I_n) :
i < n0 -> (s^-1 i < s^-1 (inord i.+1)) = (length (s * 's_i) > length s).
Lemma length_eltr (i : 'I_n0) : length 's_i = 1%N.
Lemma length_prods (w : seq 'I_n0) : length 's_[w] <= size w.
Fixpoint cocode_rec m c (s : 'S_n) : seq nat :=
if m is m'.+1 then
let mo := inord m' in
cocode_rec m' (mo - s mo :: c) (s * 's_[iota (s mo) (mo - s mo)])
else c.
Definition cocode s := cocode_rec n [::] s.
Definition canword s : seq 'I_n0 := pmap insub (wordcd (cocode s)).
if m is m'.+1 then
let mo := inord m' in
cocode_rec m' (mo - s mo :: c) (s * 's_[iota (s mo) (mo - s mo)])
else c.
Definition cocode s := cocode_rec n [::] s.
Definition canword s : seq 'I_n0 := pmap insub (wordcd (cocode s)).
Lemma cocode_rec_cat m c s : cocode_rec m c s = (cocode_rec m [::] s ++ c).
Lemma wordcdE c :
's_[wordcd c] =
\prod_(i <- iota 0 (size c)) 's_[rev (iota (i - nth 0 c i) (nth 0 c i))].
Lemma size_cocode_rec m s c : size (cocode_rec m c s) = m + size c.
Lemma size_cocode s : size (cocode s) = n.
Lemma wordcdE c :
's_[wordcd c] =
\prod_(i <- iota 0 (size c)) 's_[rev (iota (i - nth 0 c i) (nth 0 c i))].
Lemma size_cocode_rec m s c : size (cocode_rec m c s) = m + size c.
Lemma size_cocode s : size (cocode s) = n.
Section PartCode.
Let is_partcode m c :=
forall i, i < size c -> nth 0 c i <= i + m.
Let word_of_partcocode m c : seq nat :=
flatten [seq rev (iota (m + i - nth 0 c i) (nth 0 c i)) |
i <- iota 0 (size c)].
Lemma perm_on_cocode_recP m c s0 s :
m <= n ->
is_partcode m c ->
s0 = s * 's_[word_of_partcocode m c] ->
perm_on [set k : 'I_n | k < m] s ->
let cf := cocode_rec m c s in cf \is a code /\ s0 = 's_[wordcd cf].
End PartCode.
Lemma perm_on_prods c m :
c \is a code -> m <= size c -> m <= n ->
perm_on [set k : 'I_n | k < m]
(\prod_(i <- iota 0 m) 's_[(rev (iota (i - nth 0 c i) (nth 0 c i)))]).
Lemma perm_on_prods_length_ord s i (m : 'I_n) :
i <= m -> perm_on [set k : 'I_n | k < m] s ->
length (s * 's_[rev (iota (m - i) i)]) = length s + i.
Lemma perm_on_prods_length s i m :
m < n -> i <= m -> perm_on [set k : 'I_n | k < m] s ->
length (s * 's_[(rev (iota (m - i) i))]) = length s + i.
Lemma length_permcd c :
c \is a code -> size c <= n -> length 's_[wordcd c] = sumn c.
Lemma cocode2P s :
let c := cocode s in c \is a code /\ s = 's_[wordcd c].
Lemma cocodeP s : cocode s \is a code.
Lemma cocodeE s : s = 's_[wordcd (cocode s)].
Let is_partcode m c :=
forall i, i < size c -> nth 0 c i <= i + m.
Let word_of_partcocode m c : seq nat :=
flatten [seq rev (iota (m + i - nth 0 c i) (nth 0 c i)) |
i <- iota 0 (size c)].
Lemma perm_on_cocode_recP m c s0 s :
m <= n ->
is_partcode m c ->
s0 = s * 's_[word_of_partcocode m c] ->
perm_on [set k : 'I_n | k < m] s ->
let cf := cocode_rec m c s in cf \is a code /\ s0 = 's_[wordcd cf].
End PartCode.
Lemma perm_on_prods c m :
c \is a code -> m <= size c -> m <= n ->
perm_on [set k : 'I_n | k < m]
(\prod_(i <- iota 0 m) 's_[(rev (iota (i - nth 0 c i) (nth 0 c i)))]).
Lemma perm_on_prods_length_ord s i (m : 'I_n) :
i <= m -> perm_on [set k : 'I_n | k < m] s ->
length (s * 's_[rev (iota (m - i) i)]) = length s + i.
Lemma perm_on_prods_length s i m :
m < n -> i <= m -> perm_on [set k : 'I_n | k < m] s ->
length (s * 's_[(rev (iota (m - i) i))]) = length s + i.
Lemma length_permcd c :
c \is a code -> size c <= n -> length 's_[wordcd c] = sumn c.
Lemma cocode2P s :
let c := cocode s in c \is a code /\ s = 's_[wordcd c].
Lemma cocodeP s : cocode s \is a code.
Lemma cocodeE s : s = 's_[wordcd (cocode s)].
Properties of canword s
Lemma canwordE s :
[seq (i : nat) | i : 'I_n0 <- canword s] = wordcd (cocode s).
Theorem canwordP s : 's_[canword s] = s.
As a consequence 'SG_n is generated by the elementary transpositions
The corresponding induction theorem
Theorem eltr_ind (P : 'S_n -> Type) :
P 1 -> (forall s i, i < n0 -> P s -> P ('s_i * s)) ->
forall s, P s.
Corollary morph_eltr (gT : finGroupType)
(f g : {morphism 'SG_n >-> gT}) :
(forall i : 'I_n0, f 's_i = g 's_i) -> f =1 g.
P 1 -> (forall s i, i < n0 -> P s -> P ('s_i * s)) ->
forall s, P s.
Corollary morph_eltr (gT : finGroupType)
(f g : {morphism 'SG_n >-> gT}) :
(forall i : 'I_n0, f 's_i = g 's_i) -> f =1 g.
A simple application
Lemma sumn_cocode s : sumn (cocode s) = length s.
Theorem size_canword s : size (canword s) = length s.
Corollary length_eq0 s : length s = 0 -> s = 1.
Corollary length_eq1 s : length s = 1%N -> exists i : 'I_n0, s = 's_i.
Corollary lengthM s t : length (s * t) <= length s + length t.
Corollary lengthME s t :
length s + length t <= length (s * t) -> length (s * t) = length s + length t.
Corollary lengthKR s t u :
length (s * t * u) = length s + length t + length u ->
length (t * u) = length t + length u.
Corollary lengthKL s t u :
length (s * t * u) = length s + length t + length u ->
length (s * t) = length s + length t.
Definition prods_codesz (c : codesz n) : 'S_n := 's_[wordcd c].
Lemma prods_codesz_bij : bijective prods_codesz.
Lemma prods_wordcd_inj c1 c2 :
c1 \is a code -> c2 \is a code -> size c1 = n -> size c2 = n ->
's_[wordcd c1] = 's_[wordcd c2] -> c1 = c2.
End Length.
#[export] Hint Resolve cocodeP : core.
#[export] Hint Resolve codeszP : core.
Theorem size_canword s : size (canword s) = length s.
Corollary length_eq0 s : length s = 0 -> s = 1.
Corollary length_eq1 s : length s = 1%N -> exists i : 'I_n0, s = 's_i.
Corollary lengthM s t : length (s * t) <= length s + length t.
Corollary lengthME s t :
length s + length t <= length (s * t) -> length (s * t) = length s + length t.
Corollary lengthKR s t u :
length (s * t * u) = length s + length t + length u ->
length (t * u) = length t + length u.
Corollary lengthKL s t u :
length (s * t * u) = length s + length t + length u ->
length (s * t) = length s + length t.
Definition prods_codesz (c : codesz n) : 'S_n := 's_[wordcd c].
Lemma prods_codesz_bij : bijective prods_codesz.
Lemma prods_wordcd_inj c1 c2 :
c1 \is a code -> c2 \is a code -> size c1 = n -> size c2 = n ->
's_[wordcd c1] = 's_[wordcd c2] -> c1 = c2.
End Length.
#[export] Hint Resolve cocodeP : core.
#[export] Hint Resolve codeszP : core.
Let's do some real combinatorics !!!
Section Combi.
Import GRing.Theory.
Open Scope ring_scope.
Corollary genfun_length n :
\sum_(s : 'S_n) 'X^(length s) =
\prod_(0 <= i < n) \sum_(0 <= j < i.+1) 'X^j : {poly int}.
End Combi.
Section Reduced.
Variable n : nat.
Implicit Type u v w : seq 'I_n.
Notation "''s_' i" := (eltr n i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Definition reduced_word := [qualify w : seq 'I_n | length 's_[w] == size w ].
Notation reduced := reduced_word.
Lemma reducedP w : reflect (length 's_[w] = size w) (w \is reduced).
Lemma reduced_nil : [::] \is reduced.
Hint Resolve reduced_nil : core.
Lemma reduced_iiF i : [:: i; i] \is reduced = false.
Lemma reduced_rev w : w \is reduced -> rev w \is reduced.
Lemma reduced_revE w : (w \is reduced) = (rev w \is reduced).
Lemma reduced_sprod_code c :
c \is a code -> size c <= n.+1 -> pmap insub (wordcd c) \is reduced.
Variable n : nat.
Implicit Type u v w : seq 'I_n.
Notation "''s_' i" := (eltr n i).
Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
Definition reduced_word := [qualify w : seq 'I_n | length 's_[w] == size w ].
Notation reduced := reduced_word.
Lemma reducedP w : reflect (length 's_[w] = size w) (w \is reduced).
Lemma reduced_nil : [::] \is reduced.
Hint Resolve reduced_nil : core.
Lemma reduced_iiF i : [:: i; i] \is reduced = false.
Lemma reduced_rev w : w \is reduced -> rev w \is reduced.
Lemma reduced_revE w : (w \is reduced) = (rev w \is reduced).
Lemma reduced_sprod_code c :
c \is a code -> size c <= n.+1 -> pmap insub (wordcd c) \is reduced.
Theorem canword_reduced s : canword s \is reduced.
Lemma reduced_catr u v : u ++ v \is reduced -> v \is reduced.
Lemma reduced_catl u v : u ++ v \is reduced -> u \is reduced.
Lemma reduced_consK i u : i :: u \is reduced -> u \is reduced.
Lemma reduced_rconsK u i : rcons u i \is reduced -> u \is reduced.
Lemma reducedM (s t : 'S_(n.+1)) :
length (s * t) = length s + length t -> canword s ++ canword t \is reduced.
Lemma canword1 : canword (1 : 'S_n.+1) = [::].
Lemma reduced_catr u v : u ++ v \is reduced -> v \is reduced.
Lemma reduced_catl u v : u ++ v \is reduced -> u \is reduced.
Lemma reduced_consK i u : i :: u \is reduced -> u \is reduced.
Lemma reduced_rconsK u i : rcons u i \is reduced -> u \is reduced.
Lemma reducedM (s t : 'S_(n.+1)) :
length (s * t) = length s + length t -> canword s ++ canword t \is reduced.
Lemma canword1 : canword (1 : 'S_n.+1) = [::].
Definition braid_aba :=
fun s : seq 'I_n => match s with
| [:: a; b; c] => if (a == c) && ((a.+1 == b) || (b.+1 == a))
then [:: [:: b; a; b]] else [::]
| _ => [::]
end.
Definition braidC :=
fun s : seq 'I_n => match s with
| [:: a; b] => if (a.+1 < b) || (b.+1 < a)
then [:: [:: b; a]] else [::]
| _ => [::]
end.
Definition braidrule := [fun s => braid_aba s ++ braidC s].
Lemma braid_abaP (u v : seq 'I_n) :
reflect (exists a b : 'I_n,
[/\ ((a.+1 == b) || (b.+1 == a)),
u = [:: a; b; a] & v = [:: b; a; b] ] )
(v \in braid_aba u).
Lemma braidCP (u v : seq 'I_n) :
reflect (exists a b : 'I_n,
[/\ ((a.+1 < b) || (b.+1 < a)), u = [:: a; b] & v = [:: b; a] ] )
(v \in braidC u).
Lemma braidrule_sym (u v : seq 'I_n) :
v \in (braidrule u) -> u \in (braidrule v).
Lemma braidrule_homog (u : seq 'I_n) :
all [pred v | size v == size u] (braidrule u).
Definition braidcongr := gencongr_hom braidrule_homog.
Definition braidclass := genclass_hom braidrule_homog.
#[local] Notation "a =Br b" := (braidcongr a b).
Lemma braid_equiv : equivalence_rel braidcongr.
Lemma braid_refl : reflexive braidcongr.
Lemma braidww w : braidcongr w w.
Lemma braid_sym : symmetric braidcongr.
Lemma braid_ltrans : left_transitive braidcongr.
Lemma braid_trans : transitive braidcongr.
Lemma braid_is_congr : congruence_rel braidcongr.
Definition braid_cons := congr_cons braid_is_congr.
Definition braid_rcons := congr_rcons braid_is_congr.
Definition braid_catl := congr_catl braid_is_congr.
Definition braid_catr := congr_catr braid_is_congr.
Definition braid_cat := congr_cat braid_is_congr braid_equiv.
Lemma size_braid u v : u =Br v -> size u = size v.
Lemma braid_rev u v : u =Br v -> rev u =Br rev v.
Lemma class_braid1 (i : 'I_n) u : u =Br [:: i] -> u = [:: i].
Theorem braid_prods v w : v =Br w -> 's_[v] = 's_[w].
Corollary braid_reduced (v w : seq 'I_n) :
v =Br w -> v \is reduced -> w \is reduced.
fun s : seq 'I_n => match s with
| [:: a; b; c] => if (a == c) && ((a.+1 == b) || (b.+1 == a))
then [:: [:: b; a; b]] else [::]
| _ => [::]
end.
Definition braidC :=
fun s : seq 'I_n => match s with
| [:: a; b] => if (a.+1 < b) || (b.+1 < a)
then [:: [:: b; a]] else [::]
| _ => [::]
end.
Definition braidrule := [fun s => braid_aba s ++ braidC s].
Lemma braid_abaP (u v : seq 'I_n) :
reflect (exists a b : 'I_n,
[/\ ((a.+1 == b) || (b.+1 == a)),
u = [:: a; b; a] & v = [:: b; a; b] ] )
(v \in braid_aba u).
Lemma braidCP (u v : seq 'I_n) :
reflect (exists a b : 'I_n,
[/\ ((a.+1 < b) || (b.+1 < a)), u = [:: a; b] & v = [:: b; a] ] )
(v \in braidC u).
Lemma braidrule_sym (u v : seq 'I_n) :
v \in (braidrule u) -> u \in (braidrule v).
Lemma braidrule_homog (u : seq 'I_n) :
all [pred v | size v == size u] (braidrule u).
Definition braidcongr := gencongr_hom braidrule_homog.
Definition braidclass := genclass_hom braidrule_homog.
#[local] Notation "a =Br b" := (braidcongr a b).
Lemma braid_equiv : equivalence_rel braidcongr.
Lemma braid_refl : reflexive braidcongr.
Lemma braidww w : braidcongr w w.
Lemma braid_sym : symmetric braidcongr.
Lemma braid_ltrans : left_transitive braidcongr.
Lemma braid_trans : transitive braidcongr.
Lemma braid_is_congr : congruence_rel braidcongr.
Definition braid_cons := congr_cons braid_is_congr.
Definition braid_rcons := congr_rcons braid_is_congr.
Definition braid_catl := congr_catl braid_is_congr.
Definition braid_catr := congr_catr braid_is_congr.
Definition braid_cat := congr_cat braid_is_congr braid_equiv.
Lemma size_braid u v : u =Br v -> size u = size v.
Lemma braid_rev u v : u =Br v -> rev u =Br rev v.
Lemma class_braid1 (i : 'I_n) u : u =Br [:: i] -> u = [:: i].
Theorem braid_prods v w : v =Br w -> 's_[v] = 's_[w].
Corollary braid_reduced (v w : seq 'I_n) :
v =Br w -> v \is reduced -> w \is reduced.
Fixpoint reduces (u v : seq 'I_n) :=
match u with
| [::] | [:: _] => false
| [:: a, b & l] =>
((a == b) && (l == v))
|| if v is v0 :: v' then (a == v0) && reduces (b :: l) v'
else false
end.
Lemma reducesP (u v : seq 'I_n) :
reflect
(exists x i y, u = x ++ [:: i; i] ++ y /\ v = x ++ y)
(reduces u v).
Lemma reduces_catl u v w : reduces u v -> reduces (u ++ w) (v ++ w).
Lemma prods_reducesE u v : reduces u v -> 's_[u] = 's_[v].
Definition braid_reduces (u v : seq 'I_n) := (u =Br v) || (reduces u v).
Lemma braidred_catl (u v w : seq 'I_n) :
braid_reduces u v -> braid_reduces (u ++ w) (v ++ w).
Lemma braidredE u v : braid_reduces u v -> 's_[u] = 's_[v].
End Reduced.
Arguments reducedP {n w}.
Notation reduced := (reduced_word _).
Notation braidred := (@braid_reduces _).
#[export] Hint Resolve braidww : core.
match u with
| [::] | [:: _] => false
| [:: a, b & l] =>
((a == b) && (l == v))
|| if v is v0 :: v' then (a == v0) && reduces (b :: l) v'
else false
end.
Lemma reducesP (u v : seq 'I_n) :
reflect
(exists x i y, u = x ++ [:: i; i] ++ y /\ v = x ++ y)
(reduces u v).
Lemma reduces_catl u v w : reduces u v -> reduces (u ++ w) (v ++ w).
Lemma prods_reducesE u v : reduces u v -> 's_[u] = 's_[v].
Definition braid_reduces (u v : seq 'I_n) := (u =Br v) || (reduces u v).
Lemma braidred_catl (u v w : seq 'I_n) :
braid_reduces u v -> braid_reduces (u ++ w) (v ++ w).
Lemma braidredE u v : braid_reduces u v -> 's_[u] = 's_[v].
End Reduced.
Arguments reducedP {n w}.
Notation reduced := (reduced_word _).
Notation braidred := (@braid_reduces _).
#[export] Hint Resolve braidww : core.
Section CanWord.
Variable (n0 : nat).
#[local] Notation n := n0.+1.
#[local] Notation "''s_' i" := (eltr n i) : group_scope.
#[local] Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
#[local] Notation "a =Br b" := (braidcongr a b).
Fixpoint inscode (c : seq nat) (i : 'I_n) :=
if c is c0 :: c' then
let m := size c' in
if i > m - c0 then c0 :: inscode c' (inord i.-1)
else if i == m - c0 :> nat then c0.-1 :: c'
else if i.+1 == m - c0 :> nat then c0.+1 :: c'
else c0 :: inscode c' i
else [::].
Lemma size_inscode c i : size (inscode c i) = size c.
Lemma head_revcode c0 c : rev (c0 :: c) \is a code -> c0 <= size c.
Lemma inord_predS (i : 'I_n) a b :
a < i -> i < b -> (inord (n' := n0) i.-1).+1 < b.
Lemma inscodeP c (i : 'I_n) :
rev c \is a code -> i.+1 < size c -> rev (inscode c i) \is a code.
Let wcord c : seq 'I_n := map inord (wordcd (rev c)).
Lemma wcordE c :
rev c \is a code -> size c <= n.+1 -> wcord c = pmap insub (wordcd (rev c)).
Lemma reduced_wcord c :
rev c \is a code -> size c <= n.+1 -> wcord c \is reduced.
Lemma wcord_cons c i :
wcord (i :: c) = wcord c ++ map inord (rev (iota (size c - i) i)).
Lemma ltn_braidC (s : seq 'I_n) (i : 'I_n) :
(forall u, u \in s -> u.+1 < i) -> [:: i] ++ s =Br s ++ [:: i].
Lemma gtn_braidC (s : seq 'I_n) (i : 'I_n) :
(forall u, u \in s -> i.+1 < u) -> [:: i] ++ s =Br s ++ [:: i].
Lemma iota_cut_i (l b : nat) (i : 'I_n) :
l <= b -> b - l < i -> i < b -> iota (b - l) l =
(iota (b - l) (i.-1 - (b - l))) ++ [:: i.-1; i : nat] ++ (iota i.+1 (b - i.+1)).
#[local] Notation "''I[' a '..' b ']'" :=
[seq inord i | i <- rev (iota (b - a) a)].
Lemma braid_pred_lineC (i : 'I_n) (sz c : nat) :
sz <= n -> i < sz -> c <= sz -> sz - c < i ->
([:: inord i.-1] ++ 'I[c .. sz]) =Br ('I[c .. sz] ++ [:: i]).
Lemma braid_ltn_lineC (i : 'I_n) (sz c : nat) :
sz <= n -> i.+1 < sz - c -> c <= sz ->
[:: i] ++ 'I[c .. sz] =Br 'I[c .. sz] ++ [:: i].
Implicit Type (u v w : seq 'I_n).
Lemma path_braidred_catl p u w :
path braidred u p -> path braidred (u ++ w) [seq v ++ w | v <- p].
Lemma braidred_inscode_path c (i : 'I_n) :
rev c \is a code -> size c <= n.+1 -> i.+1 < size c ->
{ p | path braidred ((wcord c) ++ [:: i]) p /\
last ((wcord c) ++ [:: i]) p = wcord (inscode c i) }.
Variable (n0 : nat).
#[local] Notation n := n0.+1.
#[local] Notation "''s_' i" := (eltr n i) : group_scope.
#[local] Notation "''s_' [ w ]" := (\prod_(i <- w) 's_i).
#[local] Notation "a =Br b" := (braidcongr a b).
Fixpoint inscode (c : seq nat) (i : 'I_n) :=
if c is c0 :: c' then
let m := size c' in
if i > m - c0 then c0 :: inscode c' (inord i.-1)
else if i == m - c0 :> nat then c0.-1 :: c'
else if i.+1 == m - c0 :> nat then c0.+1 :: c'
else c0 :: inscode c' i
else [::].
Lemma size_inscode c i : size (inscode c i) = size c.
Lemma head_revcode c0 c : rev (c0 :: c) \is a code -> c0 <= size c.
Lemma inord_predS (i : 'I_n) a b :
a < i -> i < b -> (inord (n' := n0) i.-1).+1 < b.
Lemma inscodeP c (i : 'I_n) :
rev c \is a code -> i.+1 < size c -> rev (inscode c i) \is a code.
Let wcord c : seq 'I_n := map inord (wordcd (rev c)).
Lemma wcordE c :
rev c \is a code -> size c <= n.+1 -> wcord c = pmap insub (wordcd (rev c)).
Lemma reduced_wcord c :
rev c \is a code -> size c <= n.+1 -> wcord c \is reduced.
Lemma wcord_cons c i :
wcord (i :: c) = wcord c ++ map inord (rev (iota (size c - i) i)).
Lemma ltn_braidC (s : seq 'I_n) (i : 'I_n) :
(forall u, u \in s -> u.+1 < i) -> [:: i] ++ s =Br s ++ [:: i].
Lemma gtn_braidC (s : seq 'I_n) (i : 'I_n) :
(forall u, u \in s -> i.+1 < u) -> [:: i] ++ s =Br s ++ [:: i].
Lemma iota_cut_i (l b : nat) (i : 'I_n) :
l <= b -> b - l < i -> i < b -> iota (b - l) l =
(iota (b - l) (i.-1 - (b - l))) ++ [:: i.-1; i : nat] ++ (iota i.+1 (b - i.+1)).
#[local] Notation "''I[' a '..' b ']'" :=
[seq inord i | i <- rev (iota (b - a) a)].
Lemma braid_pred_lineC (i : 'I_n) (sz c : nat) :
sz <= n -> i < sz -> c <= sz -> sz - c < i ->
([:: inord i.-1] ++ 'I[c .. sz]) =Br ('I[c .. sz] ++ [:: i]).
Lemma braid_ltn_lineC (i : 'I_n) (sz c : nat) :
sz <= n -> i.+1 < sz - c -> c <= sz ->
[:: i] ++ 'I[c .. sz] =Br 'I[c .. sz] ++ [:: i].
Implicit Type (u v w : seq 'I_n).
Lemma path_braidred_catl p u w :
path braidred u p -> path braidred (u ++ w) [seq v ++ w | v <- p].
Lemma braidred_inscode_path c (i : 'I_n) :
rev c \is a code -> size c <= n.+1 -> i.+1 < size c ->
{ p | path braidred ((wcord c) ++ [:: i]) p /\
last ((wcord c) ++ [:: i]) p = wcord (inscode c i) }.
Fixpoint straighten_rev w :=
if w is w0 :: w then inscode (straighten_rev w) w0 else (nseq n.+1 0).
Definition straighten w := straighten_rev (rev w).
Lemma size_straighten w : size (straighten w) = n.+1.
Lemma is_code_straighten w : rev (straighten w) \is a code.
Lemma straighten_path_npos w :
{ p | path braidred w p /\ last w p = wcord (straighten w) }.
Theorem prods_straighten w : 's_[wcord (straighten w)] = 's_[w].
Corollary cocode_straightenE w : rev (straighten w) = cocode 's_[w].
Corollary canword_straightenE w : wcord (straighten w) = canword 's_[w].
Corollary canword_path_npos w :
{ p | path braidred w p /\ last w p = canword 's_[w] }.
End CanWord.
Notation "''s_' i" := (eltr _ i) : group_scope.
Notation "''s_[' w ']'" := (\prod_(i <- w) 's_i) : group_scope.
#[local] Notation "a =Br b" := (braidcongr a b) : bool_scope.
Section BraidRed.
Variable n : nat.
Implicit Types (u v w : seq 'I_n).
Theorem braidred_to_canword w :
{ p | path braidred w p /\ last w p = canword 's_[w] }.
Lemma braidred_size_decr w p : path braidred w p -> size w >= size (last w p).
Theorem braid_to_canword w : w \is reduced -> w =Br canword 's_[w].
Theorem reduceP u : u \isn't reduced -> exists v w, u =Br v /\ reduces v w.
if w is w0 :: w then inscode (straighten_rev w) w0 else (nseq n.+1 0).
Definition straighten w := straighten_rev (rev w).
Lemma size_straighten w : size (straighten w) = n.+1.
Lemma is_code_straighten w : rev (straighten w) \is a code.
Lemma straighten_path_npos w :
{ p | path braidred w p /\ last w p = wcord (straighten w) }.
Theorem prods_straighten w : 's_[wcord (straighten w)] = 's_[w].
Corollary cocode_straightenE w : rev (straighten w) = cocode 's_[w].
Corollary canword_straightenE w : wcord (straighten w) = canword 's_[w].
Corollary canword_path_npos w :
{ p | path braidred w p /\ last w p = canword 's_[w] }.
End CanWord.
Notation "''s_' i" := (eltr _ i) : group_scope.
Notation "''s_[' w ']'" := (\prod_(i <- w) 's_i) : group_scope.
#[local] Notation "a =Br b" := (braidcongr a b) : bool_scope.
Section BraidRed.
Variable n : nat.
Implicit Types (u v w : seq 'I_n).
Theorem braidred_to_canword w :
{ p | path braidred w p /\ last w p = canword 's_[w] }.
Lemma braidred_size_decr w p : path braidred w p -> size w >= size (last w p).
Theorem braid_to_canword w : w \is reduced -> w =Br canword 's_[w].
Theorem reduceP u : u \isn't reduced -> exists v w, u =Br v /\ reduces v w.
Matsumoto Theorem
Corollary reduced_braid v w :
v \is reduced -> w \is reduced -> ('s_[v] == 's_[w] :> 'S_n.+1) = (v =Br w).
Lemma canword_eltr (i : 'I_n) : canword 's_i = [:: i].
End BraidRed.
v \is reduced -> w \is reduced -> ('s_[v] == 's_[w] :> 'S_n.+1) = (v =Br w).
Lemma canword_eltr (i : 'I_n) : canword 's_i = [:: i].
End BraidRed.
Section PresentationSn.
Variable n : nat.
Variable gT : finGroupType.
Variable eltrG : nat -> gT.
#[local] Notation "''g_' i" :=
(eltrG i) (at level 8, i at level 2, format "''g_' i").
Variant relat_Sn : Prop :=
RelatSn of
(forall i, i < n -> 'g_i^+2 = 1) &
(forall i, i.+1 < n -> 'g_i * 'g_i.+1 * 'g_i = 'g_i.+1 * 'g_i * 'g_i.+1) &
(forall i j, i.+1 < j < n -> 'g_i * 'g_j = 'g_j * 'g_i)
: relat_Sn.
Theorem presentation_Sn_eltr :
relat_Sn ->
exists f : {morphism 'SG_n.+1 >-> gT}, forall i, i < n -> f 's_i = 'g_i.
End PresentationSn.
Lemma joingU1 (gt : finGroupType) (a : gt) (S : {set gt}) :
<[a]> <*> <<S>> = << a |: S >>.
Lemma presentation_S2 :
'SG_2 \isog Grp ( s0 : s0^+2 ).
Lemma presentation_S3 :
'SG_3 \isog Grp ( s0 : s1 : (s0^+2 = s1^+2 = 1, s0*s1*s0 = s1*s0*s1) ).
Lemma presentation_S4 :
'SG_4 \isog Grp (
s0 : s1 : s2 :
(s0^+2, s1^+2, s2^+2,
s0*s1*s0 = s1*s0*s1, s1*s2*s1 = s2*s1*s2,
s0*s2 = s2*s0
) ).
Lemma presentation_S5 :
'SG_5 \isog Grp (
s0 : s1 : s2 : s3 :
(s0^+2, s1^+2, s2^+2, s3^+2,
s0*s1*s0 = s1*s0*s1, s1*s2*s1 = s2*s1*s2, s2*s3*s2 = s3*s2*s3,
s0*s2 = s2*s0, s0*s3 = s3*s0, s1*s3 = s3*s1
) ).
Variable n : nat.
Variable gT : finGroupType.
Variable eltrG : nat -> gT.
#[local] Notation "''g_' i" :=
(eltrG i) (at level 8, i at level 2, format "''g_' i").
Variant relat_Sn : Prop :=
RelatSn of
(forall i, i < n -> 'g_i^+2 = 1) &
(forall i, i.+1 < n -> 'g_i * 'g_i.+1 * 'g_i = 'g_i.+1 * 'g_i * 'g_i.+1) &
(forall i j, i.+1 < j < n -> 'g_i * 'g_j = 'g_j * 'g_i)
: relat_Sn.
Theorem presentation_Sn_eltr :
relat_Sn ->
exists f : {morphism 'SG_n.+1 >-> gT}, forall i, i < n -> f 's_i = 'g_i.
End PresentationSn.
Lemma joingU1 (gt : finGroupType) (a : gt) (S : {set gt}) :
<[a]> <*> <<S>> = << a |: S >>.
Lemma presentation_S2 :
'SG_2 \isog Grp ( s0 : s0^+2 ).
Lemma presentation_S3 :
'SG_3 \isog Grp ( s0 : s1 : (s0^+2 = s1^+2 = 1, s0*s1*s0 = s1*s0*s1) ).
Lemma presentation_S4 :
'SG_4 \isog Grp (
s0 : s1 : s2 :
(s0^+2, s1^+2, s2^+2,
s0*s1*s0 = s1*s0*s1, s1*s2*s1 = s2*s1*s2,
s0*s2 = s2*s0
) ).
Lemma presentation_S5 :
'SG_5 \isog Grp (
s0 : s1 : s2 : s3 :
(s0^+2, s1^+2, s2^+2, s3^+2,
s0*s1*s0 = s1*s0*s1, s1*s2*s1 = s2*s1*s2, s2*s3*s2 = s3*s2*s3,
s0*s2 = s2*s0, s0*s3 = s3*s0, s1*s3 = s3*s1
) ).