Theory Coxeter
section ‹Coxeter systems and complexes›
text ‹
A Coxeter system is a group that affords a presentation, where each generator is of order two,
and each relator is an alternating word of even length in two generators.
›
theory Coxeter
imports Chamber
begin
subsection ‹Coxeter-like systems›
text ‹First we work in a group generated by elements of order two.›
subsubsection ‹Locale definition and basic facts›
locale PreCoxeterSystem =
fixes S :: "'w::group_add set"
assumes genset_order2: "s∈S ⟹ add_order s = 2"
begin
abbreviation "W ≡ ⟨S⟩"
abbreviation "S_length ≡ word_length S"
abbreviation "S_reduced_for ≡ reduced_word_for S"
abbreviation "S_reduced ≡ reduced_word S"
abbreviation "relfun ≡ λs t. add_order (s+t)"
lemma no_zero_genset: "0∉S"
proof
assume "0∈S"
moreover have "add_order (0::'w) = 1" using add_order0 by fast
ultimately show False using genset_order2 by simp
qed
lemma genset_order2_add: "s∈S ⟹ s + s = 0"
using add_order[of s] by (simp add: genset_order2 nataction_2)
lemmas genset_uminus = minus_unique[OF genset_order2_add]
lemma relfun_S: "s∈S ⟹ relfun s s = 1"
using add_order_relator[of s] by (auto simp add: genset_order2 nataction_2)
lemma relfun_eq1: "⟦ s∈S; relfun s t = 1 ⟧ ⟹ t=s"
using add_order_add_eq1 genset_uminus by fastforce
lemma S_relator_list: "s∈S ⟹ pair_relator_list s s = [s,s]"
using relfun_S alternating_list2 by simp
lemma S_sym: "T ⊆ S ⟹ uminus ` T ⊆ T"
using genset_uminus by auto
lemmas special_subgroup_eq_sum_list =
genby_sym_eq_sum_lists[OF S_sym]
lemmas genby_S_reduced_word_for_arg_min =
reduced_word_for_genby_sym_arg_min[OF S_sym]
lemmas in_genby_S_reduced_letter_set =
in_genby_sym_imp_in_reduced_letter_set[OF S_sym]
end
subsubsection ‹Special cosets›
text ‹
From a Coxeter system we will eventually construct an associated chamber complex. To do so, we
will consider the collection of special cosets: left cosets of subgroups generated by subsets of
the generating set @{term S}. This collection forms a poset under the supset relation that, under
a certain extra assumption, can be used to form a simplicial complex whose poset of simplices
is isomorphic to this poset of special cosets. In the literature, groups generated by subsets of
@{term S} are often referred to as parabolic subgroups of @{term W}, and their cosets as parabolic
cosets, but following Garrett \<^cite>‹"Garrett:Buildings"› we have opted for the names special
subgroups and special cosets.
›
context PreCoxeterSystem
begin
definition special_cosets :: "'w set set"
where "special_cosets ≡ (⋃T∈Pow S. (⋃w∈W. { w +o ⟨T⟩ }))"
abbreviation "𝒫 ≡ special_cosets"
lemma special_cosetsI: "T∈Pow S ⟹ w∈W ⟹ w +o ⟨T⟩ ∈ 𝒫"
using special_cosets_def by auto
lemma special_coset_singleton: "w∈W ⟹ {w}∈𝒫"
using special_cosetsI genby_lcoset_empty[of w] by fastforce
lemma special_coset_nempty: "X∈𝒫 ⟹ X ≠ {}"
using special_cosets_def genby_lcoset_refl by fastforce
lemma special_subgroup_special_coset: "T∈Pow S ⟹ ⟨T⟩ ∈ 𝒫"
using genby_0_closed special_cosetsI[of T] by fastforce
lemma special_cosets_lcoset_closed: "w∈W ⟹ X∈𝒫 ⟹ w +o X ∈ 𝒫"
using genby_add_closed unfolding special_cosets_def
by (fastforce simp add: set_plus_rearrange2)
lemma special_cosets_lcoset_shift: "w∈W ⟹ ((+o) w) ` 𝒫 = 𝒫"
using special_cosets_lcoset_closed genby_uminus_closed
by (force simp add: set_plus_rearrange2)
lemma special_cosets_has_bottom: "supset_has_bottom 𝒫"
proof (rule ordering.has_bottomI, rule supset_poset)
show "W∈𝒫" using special_subgroup_special_coset by fast
next
fix X assume X: "X∈𝒫"
from this obtain w T where wT: "w∈W" "T∈Pow S" "X = w +o ⟨T⟩"
using special_cosets_def by auto
thus "X ⊆ W" using genby_mono[of T] genby_lcoset_closed[of w] by auto
qed
lemma special_cosets_bottom: "supset_bottom 𝒫 = W"
proof (rule supset_bottomI[THEN sym])
fix X assume "X∈𝒫"
from this obtain w T where "w∈W" "T∈Pow S" "X = w +o ⟨T⟩"
using special_cosets_def by auto
thus "X⊆W"
using genby_mono[of T S] set_plus_mono[of "⟨T⟩" W] genby_lcoset_el_reduce
by force
qed (auto simp add: special_subgroup_special_coset)
end
subsubsection ‹Transfer from the free group over generators›
text ‹
We form a set of relators and show that it and @{term S} form a
@{const GroupWithGeneratorsRelators}. The associated quotient group @{term G} maps surjectively
onto @{term W}. In the ‹CoxeterSystem› locale below, this correspondence will be assumed
to be injective as well.
›
context PreCoxeterSystem
begin
abbreviation R :: "'w list set" where "R ≡ (⋃s∈S. ⋃t∈S. {pair_relator_list s t})"
abbreviation "P ≡ map (charpair S) ` R"
abbreviation "P' ≡ GroupWithGeneratorsRelators.P' S R"
abbreviation "Q ≡ GroupWithGeneratorsRelators.Q S R"
abbreviation "G ≡ GroupWithGeneratorsRelators.G S R"
abbreviation "relator_freeword ≡
GroupWithGeneratorsRelators.relator_freeword S"
abbreviation pair_relator_freeword :: "'w ⇒ 'w ⇒ 'w freeword"
where "pair_relator_freeword s t ≡ Abs_freelist (pair_relator_list s t)"
abbreviation "freeliftid ≡ freeword_funlift id"
abbreviation induced_id :: "'w freeword set permutation ⇒ 'w"
where "induced_id ≡ GroupWithGeneratorsRelators.induced_id S R"
lemma S_relator_freeword: "s∈S ⟹ pair_relator_freeword s s = s[+]s"
by (simp add: S_relator_list Abs_freeletter_add)
lemma map_charpair_map_pairtrue_R:
"s∈S ⟹ t∈S ⟹
map (charpair S) (pair_relator_list s t) = map pairtrue (pair_relator_list s t)"
using set_alternating_list map_charpair_uniform by fastforce
lemma relator_freeword:
"s∈S ⟹ t∈S ⟹
pair_relator_freeword s t = relator_freeword (pair_relator_list s t)"
using set_alternating_list
arg_cong[OF map_charpair_map_pairtrue_R, of s t Abs_freeword]
by fastforce
lemma relator_freewords: "Abs_freelist ` R = P'"
using relator_freeword by force
lemma GroupWithGeneratorsRelators_S_R: "GroupWithGeneratorsRelators S R"
proof
fix rs assume rs: "rs∈R"
hence rs': "rs ∈ lists S" using set_alternating_list by fast
from rs' show "rs ∈ lists (S ∪ uminus ` S)" by fast
from rs show "sum_list rs = 0" using sum_list_pair_relator_list by fast
from rs' show "proper_signed_list (map (charpair S) rs)"
using proper_signed_list_map_uniform_snd
arg_cong[of "map (charpair S) rs" "map pairtrue rs" proper_signed_list]
by fastforce
qed
lemmas GroupByPresentation_S_P =
GroupWithGeneratorsRelators.GroupByPresentation_S_P[
OF GroupWithGeneratorsRelators_S_R
]
lemmas Q_FreeS = GroupByPresentation.Q_FreeS[OF GroupByPresentation_S_P]
lemma relator_freeword_Q: "s∈S ⟹ t∈S ⟹ pair_relator_freeword s t ∈ Q"
using relator_freeword
GroupByPresentation.relators[OF GroupByPresentation_S_P]
by fastforce
lemmas P'_FreeS =
GroupWithGeneratorsRelators.P'_FreeS[
OF GroupWithGeneratorsRelators_S_R
]
lemmas GroupByPresentationInducedFun_S_P_id =
GroupWithGeneratorsRelators.GroupByPresentationInducedFun_S_P_id[
OF GroupWithGeneratorsRelators_S_R
]
lemma rconj_relator_freeword:
"⟦ s∈S; t∈S; proper_signed_list xs; fst ` set xs ⊆ S ⟧ ⟹
rconjby (Abs_freeword xs) (pair_relator_freeword s t) ∈ Q"
using GroupWithGeneratorsRelators.rconj_relator_freeword[
OF GroupWithGeneratorsRelators_S_R
]
relator_freeword
by force
lemma lconjby_Abs_freelist_relator_freeword:
"⟦ s∈S; t∈S; xs∈lists S ⟧ ⟹
lconjby (Abs_freelist xs) (pair_relator_freeword s t) ∈ Q"
using GroupWithGeneratorsRelators.lconjby_Abs_freelist_relator_freeword[
OF GroupWithGeneratorsRelators_S_R
]
relator_freeword
by force
lemma Abs_freelist_rev_append_alternating_list_in_Q:
assumes "s∈S" "t∈S"
shows "Abs_freelist (rev (alternating_list n s t) @ alternating_list n s t) ∈ Q"
proof (induct n)
case (Suc m)
define u where "u = (if even m then s else t)"
define x where "x = Abs_freelist (rev (alternating_list m s t) @ alternating_list m s t)"
from u_def x_def assms have
"Abs_freelist (rev (alternating_list (Suc m) s t) @
alternating_list (Suc m) s t) =
(pair_relator_freeword u u) + rconjby (Abs_freeletter u) x"
using Abs_freelist_append[of
"u # rev (alternating_list m s t) @ alternating_list m s t"
"[u]"
]
Abs_freelist_Cons[of
u
"rev (alternating_list m s t) @ alternating_list m s t"
]
by (simp add: add.assoc[THEN sym] S_relator_freeword)
moreover from Suc assms u_def x_def have "rconjby (Abs_freeletter u) x ∈ Q"
using Abs_freeletter_in_FreeGroup_iff[of _ S]
FreeGroup_genby_set_lconjby_set_rconjby_closed
by fastforce
ultimately show ?case
using u_def assms relator_freeword_Q genby_add_closed by fastforce
qed (simp add: zero_freeword.abs_eq[THEN sym] genby_0_closed)
lemma Abs_freeword_freelist_uminus_add_in_Q:
"proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹
- Abs_freelistfst xs + Abs_freeword xs ∈ Q"
proof (induct xs)
case (Cons x xs)
from Cons(2) have 1:
"- Abs_freelistfst (x#xs) + Abs_freeword (x#xs) =
-Abs_freelistfst xs + -Abs_freeletter (fst x)
+ Abs_freeword [x] + Abs_freeword xs"
using Abs_freelist_Cons[of "fst x" "map fst xs"]
by (simp add: Abs_freeword_Cons[THEN sym] add.assoc minus_add)
show ?case
proof (cases "snd x")
case True
with Cons show ?thesis
using 1
by (simp add:
Abs_freeletter_prod_conv_Abs_freeword
binrelchain_Cons_reduce
)
next
case False
define s where "s = fst x"
with Cons(3) have s_S: "s∈S" by simp
define q where "q = rconjby (Abs_freelistfst xs) (pair_relator_freeword s s)"
from s_def False Cons(3) have
"- Abs_freelistfst (x#xs) + Abs_freeword (x#xs) =
-Abs_freelistfst xs + -pair_relator_freeword s s + Abs_freeword xs"
using 1 surjective_pairing[of x] S_relator_freeword[of s]
uminus_Abs_freeword_singleton[of s False, THEN sym]
by (simp add: add.assoc)
with q_def have 2:
"- Abs_freelistfst (x#xs) + Abs_freeword (x#xs) =
-q + (-Abs_freelistfst xs + Abs_freeword xs)"
by (simp add: rconjby_uminus[THEN sym] add.assoc[THEN sym])
moreover from q_def s_def Cons(3) have "-q∈Q"
using proper_signed_list_map_uniform_snd[of True "map fst xs"]
rconj_relator_freeword genby_uminus_closed
by fastforce
moreover from Cons have "-Abs_freelistfst xs + Abs_freeword xs ∈ Q"
by (simp add: binrelchain_Cons_reduce)
ultimately show ?thesis using genby_add_closed by simp
qed
qed (simp add: zero_freeword.abs_eq[THEN sym] genby_0_closed)
lemma Q_freelist_freeword':
"⟦ proper_signed_list xs; fst ` set xs ⊆ S; Abs_freelistfst xs ∈ Q ⟧ ⟹
Abs_freeword xs ∈ Q"
using Abs_freeword_freelist_uminus_add_in_Q genby_add_closed
by fastforce
lemma Q_freelist_freeword:
"c ∈ FreeGroup S ⟹ Abs_freelist (map fst (freeword c)) ∈ Q ⟹ c ∈ Q"
using freeword FreeGroupD Q_freelist_freeword' freeword_inverse[of c]
by fastforce
text ‹
Here we show that the lift of the identity map to the free group on @{term S} is really just
summation.
›
lemma freeliftid_Abs_freeword_conv_sum_list:
"proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹
freeliftid (Abs_freeword xs) = sum_list (map fst xs)"
using freeword_funlift_Abs_freeword[of xs id] genset_uminus
sum_list_map_cong[of xs "apply_sign id" fst]
by fastforce
end
subsubsection ‹Words in generators containing alternating subwords›
text ‹
Besides cancelling subwords equal to relators, the primary algebraic manipulation in seeking to
reduce a word in generators in a Coxeter system is to reverse the order of alternating subwords
of half the length of the associated relator, in order to create adjacent repeated letters that
can be cancelled. Here we detail the mechanics of such manipulations.
›
context PreCoxeterSystem
begin
lemma sum_list_pair_relator_halflist_flip:
"s∈S ⟹ t∈S ⟹
sum_list (pair_relator_halflist s t) = sum_list (pair_relator_halflist t s)"
using add_order[of "s+t"] genset_order2_add
alternating_order2_even_cancel_right[of s t "2*(relfun s t)"]
by (simp add: alternating_sum_list_conv_nataction add_order_add_sym)
definition flip_altsublist_adjacent :: "'w list ⇒ 'w list ⇒ bool"
where "flip_altsublist_adjacent ss ts
≡ ∃s t as bs. ss = as @ (pair_relator_halflist s t) @ bs ∧
ts = as @ (pair_relator_halflist t s) @ bs"
abbreviation "flip_altsublist_chain ≡ binrelchain flip_altsublist_adjacent"
lemma flip_altsublist_adjacentI:
"ss = as @ (pair_relator_halflist s t) @ bs ⟹
ts = as @ (pair_relator_halflist t s) @ bs ⟹
flip_altsublist_adjacent ss ts"
using flip_altsublist_adjacent_def by fast
lemma flip_altsublist_adjacent_Cons_grow:
assumes "flip_altsublist_adjacent ss ts"
shows "flip_altsublist_adjacent (a#ss) (a#ts)"
proof-
from assms obtain s t as bs
where ssts: "ss = as @ (pair_relator_halflist s t) @ bs"
"ts = as @ (pair_relator_halflist t s) @ bs"
using flip_altsublist_adjacent_def
by auto
from ssts have
"a#ss = (a#as) @ (pair_relator_halflist s t) @ bs"
"a#ts = (a#as) @ (pair_relator_halflist t s) @ bs"
by auto
thus ?thesis by (fast intro: flip_altsublist_adjacentI)
qed
lemma flip_altsublist_chain_map_Cons_grow:
"flip_altsublist_chain tss ⟹ flip_altsublist_chain (map ((#) t) tss)"
by (induct tss rule: list_induct_CCons)
(auto simp add:
binrelchain_Cons_reduce[of flip_altsublist_adjacent]
flip_altsublist_adjacent_Cons_grow
)
lemma flip_altsublist_adjacent_refl:
"ss ≠ [] ⟹ ss∈lists S ⟹ flip_altsublist_adjacent ss ss"
proof (induct ss rule: list_nonempty_induct)
case (single s)
hence "[s] = [] @ pair_relator_halflist s s @ []"
using relfun_S by simp
thus ?case by (fast intro: flip_altsublist_adjacentI)
next
case cons thus ?case using flip_altsublist_adjacent_Cons_grow by simp
qed
lemma flip_altsublist_adjacent_sym:
"flip_altsublist_adjacent ss ts ⟹ flip_altsublist_adjacent ts ss"
using flip_altsublist_adjacent_def flip_altsublist_adjacentI by auto
lemma rev_flip_altsublist_chain:
"flip_altsublist_chain xss ⟹ flip_altsublist_chain (rev xss)"
using flip_altsublist_adjacent_sym binrelchain_snoc[of flip_altsublist_adjacent]
by (induct xss rule: list_induct_CCons) auto
lemma flip_altsublist_adjacent_set:
assumes "ss∈lists S" "flip_altsublist_adjacent ss ts"
shows "set ts = set ss"
proof-
from assms obtain s t as bs where ssts:
"ss = as @ (pair_relator_halflist s t) @ bs"
"ts = as @ (pair_relator_halflist t s) @ bs"
using flip_altsublist_adjacent_def
by auto
with assms(1) show ?thesis
using set_alternating_list2[of "relfun s t" s t]
set_alternating_list2[of "relfun t s" t s]
add_order_add_sym[of t s] relfun_eq1
by (cases "relfun s t" rule: nat_cases_2Suc) auto
qed
lemma flip_altsublist_adjacent_set_ball:
"∀ss∈lists S. ∀ts. flip_altsublist_adjacent ss ts ⟶ set ts = set ss"
using flip_altsublist_adjacent_set by fast
lemma flip_altsublist_adjacent_lists:
"ss ∈ lists S ⟹ flip_altsublist_adjacent ss ts ⟹ ts ∈ lists S"
using flip_altsublist_adjacent_set by fast
lemma flip_altsublist_adjacent_lists_ball:
"∀ss∈lists S. ∀ts. flip_altsublist_adjacent ss ts ⟶ ts ∈ lists S"
using flip_altsublist_adjacent_lists by fast
lemma flip_altsublist_chain_lists:
"ss ∈ lists S ⟹ flip_altsublist_chain (ss#xss@[ts]) ⟹ ts ∈ lists S"
using flip_altsublist_adjacent_lists
binrelchain_propcong_Cons_snoc[of
"λss. ss∈lists S" flip_altsublist_adjacent ss xss ts
]
by fast
lemmas flip_altsublist_chain_funcong_Cons_snoc =
binrelchain_setfuncong_Cons_snoc[OF flip_altsublist_adjacent_lists_ball]
lemmas flip_altsublist_chain_set =
flip_altsublist_chain_funcong_Cons_snoc[
OF flip_altsublist_adjacent_set_ball
]
lemma flip_altsublist_adjacent_length:
"flip_altsublist_adjacent ss ts ⟹ length ts = length ss"
unfolding flip_altsublist_adjacent_def
by (auto simp add: add_order_add_sym length_alternating_list)
lemmas flip_altsublist_chain_length =
binrelchain_funcong_Cons_snoc[
of flip_altsublist_adjacent length, OF flip_altsublist_adjacent_length, simplified
]
lemma flip_altsublist_adjacent_sum_list:
assumes "ss ∈ lists S" "flip_altsublist_adjacent ss ts"
shows "sum_list ts = sum_list ss"
proof-
from assms(2) obtain s t as bs where stasbs:
"ss = as @ (pair_relator_halflist s t) @ bs"
"ts = as @ (pair_relator_halflist t s) @ bs"
using flip_altsublist_adjacent_def
by auto
show ?thesis
proof (cases "relfun s t")
case 0 thus ?thesis using stasbs by (simp add: add_order_add_sym)
next
case Suc
with assms stasbs have "s∈S" "t∈S"
using set_alternating_list1[of "add_order (s+t)" s t]
set_alternating_list1[of "add_order (t+s)" t s]
add_order_add_sym[of t]
flip_altsublist_adjacent_lists[of ss ts]
by auto
with stasbs show ?thesis
using sum_list_pair_relator_halflist_flip by simp
qed
qed
lemma flip_altsublist_adjacent_sum_list_ball:
"∀ss∈lists S. ∀ts. flip_altsublist_adjacent ss ts ⟶ sum_list ts = sum_list ss"
using flip_altsublist_adjacent_sum_list by fast
lemma S_reduced_forI_flip_altsublist_adjacent:
"S_reduced_for w ss ⟹ flip_altsublist_adjacent ss ts ⟹ S_reduced_for w ts"
using reduced_word_for_lists[of S] reduced_word_for_sum_list
flip_altsublist_adjacent_lists flip_altsublist_adjacent_sum_list
flip_altsublist_adjacent_length
by (fastforce intro: reduced_word_forI_compare)
lemma flip_altsublist_adjacent_in_Q':
fixes as bs s t
defines xs: "xs ≡ as @ pair_relator_halflist s t @ bs"
and ys: "ys ≡ as @ pair_relator_halflist t s @ bs"
assumes Axs: "Abs_freelist xs ∈ Q"
shows "Abs_freelist ys ∈ Q"
proof-
define X Y A B half_st half2_st half_ts
where "X = Abs_freelist xs"
and "Y = Abs_freelist ys"
and "A = Abs_freelist as"
and "B = Abs_freelist bs"
and "half_st = Abs_freelist (pair_relator_halflist s t)"
and "half2_st = Abs_freelist (pair_relator_halflist2 s t)"
and "half_ts = Abs_freelist (pair_relator_halflist t s)"
define z where "z = -half2_st + B"
define w1 w2 where "w1 = rconjby z (pair_relator_freeword s t)"
and "w2 = Abs_freelist (rev (pair_relator_halflist t s) @ pair_relator_halflist t s)"
define w3 where "w3 = rconjby B w2"
from w1_def z_def
have w1': "w1 = rconjby B (lconjby half2_st (pair_relator_freeword s t))"
by (simp add: rconjby_add)
hence "-w1 = rconjby B (lconjby half2_st (-pair_relator_freeword s t))"
using lconjby_uminus[of "half2_st"] by (simp add: rconjby_uminus[THEN sym])
moreover from X_def xs A_def half_st_def B_def have "X = A + B + rconjby B half_st"
by (simp add:
Abs_freelist_append_append[THEN sym] add.assoc[THEN sym]
)
ultimately have
"X + -w1 = A + B +
( rconjby B (half_st + (half2_st + -pair_relator_freeword s t - half2_st)) )"
by (simp add: add.assoc add_rconjby)
moreover from w2_def half2_st_def half_ts_def have "w2 = half2_st + half_ts"
by (simp add:
Abs_freelist_append[THEN sym]
pair_relator_halflist2_conv_rev_pair_relator_halflist
)
ultimately have
"X + -w1 + w3 = A + B + (rconjby B (-half2_st + (half2_st + half_ts)))"
using half_st_def half2_st_def w3_def add_assoc4[
of half_st half2_st "-pair_relator_freeword s t" "-half2_st"
]
by (simp add:
Abs_freelist_append[THEN sym] pair_relator_halflist_append
add.assoc add_rconjby
)
hence Y': "Y = X - w1 + w3"
using A_def half_ts_def B_def ys Y_def
by (simp add:
add.assoc[THEN sym]
Abs_freelist_append_append[THEN sym]
)
from Axs have xs_S: "xs ∈ lists S" using Q_FreeS FreeGroupD_transfer' by fast
have "w1∈Q ∧ w3∈Q"
proof (cases "relfun s t")
case 0 with w1_def w2_def w3_def show ?thesis using genby_0_closed
by (auto simp add:
zero_freeword.abs_eq[THEN sym]
add_order_add_sym
)
next
case (Suc m) have m: "add_order (s+t) = Suc m" by fact
have st: "{s,t} ⊆ S"
proof (cases m)
case 0 with m xs xs_S show ?thesis
using set_alternating_list1 relfun_eq1 by force
next
case Suc with m xs xs_S show ?thesis
using set_alternating_list2[of "add_order (s+t)" s t] by fastforce
qed
from xs xs_S B_def have B_S: "B ∈ FreeGroup S"
using Abs_freelist_in_FreeGroup[of bs S] by simp
moreover from w2_def have "w2∈Q"
using st Abs_freelist_rev_append_alternating_list_in_Q[of t s "add_order (t+s)"]
by fast
ultimately have "w3 ∈ Q"
using w3_def FreeGroup_genby_set_lconjby_set_rconjby_closed by fast
moreover from half2_st_def have "w1 ∈ Q"
using w1' st B_S alternating_list_in_lists[of s S] alternating_list_in_lists[of t S]
lconjby_Abs_freelist_relator_freeword[of s t]
by (force intro: FreeGroup_genby_set_lconjby_set_rconjby_closed)
ultimately show ?thesis by fast
qed
with X_def Y_def Axs show ?thesis
using Y' genby_diff_closed[of X] genby_add_closed[of "X-w1" _ w3] by simp
qed
lemma flip_altsublist_adjacent_in_Q:
"Abs_freelist ss ∈ Q ⟹ flip_altsublist_adjacent ss ts ⟹ Abs_freelist ts ∈ Q"
using flip_altsublist_adjacent_def flip_altsublist_adjacent_in_Q' by auto
lemma flip_altsublist_chain_G_in_Q:
"⟦ Abs_freelist ss ∈ Q; flip_altsublist_chain (ss#xss@[ts]) ⟧ ⟹ Abs_freelist ts ∈ Q"
using flip_altsublist_adjacent_in_Q
binrelchain_propcong_Cons_snoc[of
"λss. Abs_freelist ss ∈ Q"
flip_altsublist_adjacent
]
by fast
lemma alternating_S_no_flip:
assumes "s∈S" "t∈S" "n > 0" "n < relfun s t ∨ relfun s t = 0"
shows "sum_list (alternating_list n s t) ≠ sum_list (alternating_list n t s)"
proof
assume "sum_list (alternating_list n s t) = sum_list (alternating_list n t s)"
hence "sum_list (alternating_list n s t) + - sum_list (alternating_list n t s) = 0"
by simp
with assms(1,2) have "sum_list (alternating_list (2*n) s t) = 0"
by (cases "even n")
(auto simp add:
genset_order2_add uminus_sum_list_alternating_order2
sum_list.append[THEN sym]
alternating_list_append mult_2
)
with assms(3,4) less_add_order_eq_0_contra add_order_eq0 show False
by (auto simp add: alternating_sum_list_conv_nataction)
qed
lemma exchange_alternating_not_in_alternating:
assumes "n ≥ 2" "n < relfun s t ∨ relfun s t = 0"
"S_reduced_for w (alternating_list n s t @ cs)"
"alternating_list n s t @ cs = xs@[x]@ys" "S_reduced_for w (t#xs@ys)"
shows "length xs ≥ n"
proof-
from assms(1) obtain m k where n: "n = Suc m" and m: "m = Suc k"
using gr0_implies_Suc by fastforce
define altnst altnts altmts altkst
where "altnst = alternating_list n s t"
and "altnts = alternating_list n t s"
and "altmts = alternating_list m t s"
and "altkst = alternating_list k s t"
from altnst_def altmts_def n have altnmst: "altnst = s # altmts"
using alternating_list_Suc_Cons[of m] by fastforce
with assms(3) altnst_def have s_S: "s∈S" using reduced_word_for_lists by fastforce
from assms(5) have t_S: "t∈S" using reduced_word_for_lists by fastforce
from m altnmst altmts_def altkst_def have altnkst: "altnst = s # t # altkst"
using alternating_list_Suc_Cons by fastforce
have "¬ length xs < n"
proof (cases "Suc (length xs) = n")
case True
with assms(4,5) n altnts_def have flip: "S_reduced_for w (altnts @ cs)"
using length_alternating_list[of n s t]
alternating_list_Suc_Cons[of m t s]
by auto
from altnst_def have "sum_list altnst = sum_list altnts"
using reduced_word_for_sum_list[OF assms(3)]
reduced_word_for_sum_list[OF flip]
by auto
with n assms(2) altnst_def altnts_def show ?thesis
using alternating_S_no_flip[OF s_S t_S] by fast
next
case False show ?thesis
proof (cases xs ys rule: two_lists_cases_snoc_Cons)
case Nil1
from Nil1(1) assms(4) altnkst altnst_def have "ys = t # altkst @ cs" by auto
with Nil1(1) assms(5) show ?thesis
using t_S genset_order2_add[of t]
contains_order2_nreduced[of t S "[]" "altkst@cs"]
reduced_word_for_imp_reduced_word
by force
next
case Nil2 with assms(4) altnst_def False show ?thesis
using length_append[of altnst cs]
by (fastforce simp add: length_alternating_list)
next
case (snoc_Cons us u z zs)
with assms(4,5) altnst_def
have 1: "altnst @ cs = us@[u,x,z]@zs" "S_reduced_for w (t#us@[u,z]@zs)"
by auto
from 1(1) snoc_Cons(1) False altnst_def show ?thesis
using take_append[of n altnst cs] take_append[of n "us@[u,x,z]" zs]
set_alternating_list[of n s t]
alternating_list_alternates[of n s t us u]
reduced_word_for_imp_reduced_word[OF 1(2)]
s_S t_S genset_order2_add
contains_order2_nreduced[of u S "t#us"]
by (force simp add: length_alternating_list)
qed
qed
thus ?thesis by fastforce
qed
end
subsubsection ‹Preliminary facts on the word problem›
text ‹
The word problem seeks criteria for determining whether two words over the generator set represent
the same element in @{term W}. Here we establish one direction of the word problem, as well as a
preliminary step toward the other direction.
›
context PreCoxeterSystem
begin
lemmas flip_altsublist_chain_sum_list =
flip_altsublist_chain_funcong_Cons_snoc[OF flip_altsublist_adjacent_sum_list_ball]
lemma reduced_word_problem_eq_hd_step:
assumes step: "⋀y ss ts. ⟦
S_length y < S_length w; y≠0; S_reduced_for y ss; S_reduced_for y ts
⟧ ⟹ ∃xss. flip_altsublist_chain (ss # xss @ [ts])"
and set_up: "S_reduced_for w (a#ss)" "S_reduced_for w (a#ts)"
shows "∃xss. flip_altsublist_chain ((a#ss) # xss @ [a#ts])"
proof (cases "ss=ts")
case True
with set_up(1) have "flip_altsublist_chain ((a#ss) # [] @ [a#ts])"
using reduced_word_for_lists flip_altsublist_adjacent_refl by fastforce
thus ?thesis by fast
next
case False
define y where "y = sum_list ss"
with set_up(1) have ss: "S_reduced_for y ss"
using reduced_word_for_imp_reduced_word reduced_word_Cons_reduce by fast
moreover from y_def ss have ts: "S_reduced_for y ts"
using reduced_word_for_sum_list[OF set_up(1)]
reduced_word_for_sum_list[OF set_up(2)]
reduced_word_for_eq_length[OF set_up(1) set_up(2)]
reduced_word_for_lists[OF set_up(2)]
by (auto intro: reduced_word_forI_compare)
moreover from ss set_up(1) have "S_length y < S_length w"
using reduced_word_for_length reduced_word_for_length by fastforce
moreover from False have "y ≠ 0"
using ss ts reduced_word_for_0_imp_nil reduced_word_for_0_imp_nil by fastforce
ultimately show ?thesis
using step flip_altsublist_chain_map_Cons_grow by fastforce
qed
end
subsubsection ‹Preliminary facts related to the deletion condition›
text ‹
The deletion condition states that in a Coxeter system, every non-reduced word in the generating
set can be shortened to an equivalent word by deleting some particular pair of letters. This
condition is both necessary and sufficient for a group generated by elements of order two to be a
Coxeter system. Here we establish some facts related to the deletion condition that are true in
any group generated by elements of order two.
›
context PreCoxeterSystem
begin
abbreviation "ℋ ≡ (⋃w∈W. lconjby w ` S)"
abbreviation "lift_signed_lconjperm ≡ freeword_funlift signed_lconjpermutation"
lemma lconjseq_reflections: "ss∈lists S ⟹ set (lconjseq ss) ⊆ ℋ"
using special_subgroup_eq_sum_list[of S]
by (induct ss rule: rev_induct) (auto simp add: lconjseq_snoc)
lemma deletion':
"ss ∈ lists S ⟹ ¬ distinct (lconjseq ss) ⟹
∃a b as bs cs. ss = as @ [a] @ bs @ [b] @ cs ∧
sum_list ss = sum_list (as@bs@cs)"
proof (induct ss)
case (Cons s ss)
show ?case
proof (cases "distinct (lconjseq ss)")
case True with Cons(2,3) show ?thesis
using subset_inj_on[OF lconjby_inj, of "set (lconjseq ss)" s]
distinct_map[of "lconjby s"]
genset_order2_add order2_hd_in_lconjseq_deletion[of s ss]
by (force simp add: algebra_simps)
next
case False
with Cons(1,2) obtain a b as bs cs where
"s#ss = (s#as) @ [a] @ bs @ [b] @ cs"
"sum_list (s#ss) = sum_list ((s#as) @ bs @ cs)"
by auto
thus ?thesis by fast
qed
qed simp
lemma S_reduced_imp_distinct_lconjseq':
assumes "ss ∈ lists S" "¬ distinct (lconjseq ss)"
shows "¬ S_reduced ss"
proof
assume ss: "S_reduced ss"
from assms obtain as a bs b cs
where decomp: "ss = as @ [a] @ bs @ [b] @ cs"
"sum_list ss = sum_list (as@bs@cs)"
using deletion'[of ss]
by fast
from ss decomp assms(1) show False
using reduced_word_for_minimal[of S _ ss "as@bs@cs"] by auto
qed
lemma S_reduced_imp_distinct_lconjseq: "S_reduced ss ⟹ distinct (lconjseq ss)"
using reduced_word_for_lists S_reduced_imp_distinct_lconjseq' by fast
lemma permutation_lift_signed_lconjperm_eq_signed_list_lconjaction':
"proper_signed_list xs ⟹ fst ` set xs ⊆ S ⟹
permutation (lift_signed_lconjperm (Abs_freeword xs)) =
signed_list_lconjaction (map fst xs)"
proof (induct xs)
case Nil
have "Abs_freeword ([]::'w signed list) = (0::'w freeword)"
using zero_freeword.abs_eq by simp
thus ?case by (simp add: zero_permutation.rep_eq freeword_funlift_0)
next
case (Cons x xs)
obtain s b where x: "x=(s,b)" by fastforce
with Cons show ?case
using Abs_freeword_Cons[of x xs]
binrelchain_Cons_reduce[of nflipped_signed x xs]
bij_signed_lconjaction[of s] genset_order2_add[of s]
by (cases b)
(auto simp add:
plus_permutation.rep_eq freeword_funlift_add
freeword_funlift_Abs_freeletter
Abs_permutation_inverse uminus_permutation.rep_eq
the_inv_signed_lconjaction_by_order2
freeword_funlift_uminus_Abs_freeletter
)
qed
lemma permutation_lift_signed_lconjperm_eq_signed_list_lconjaction:
"x ∈ FreeGroup S ⟹
permutation (lift_signed_lconjperm x) =
signed_list_lconjaction (map fst (freeword x))"
using freeword FreeGroup_def[of S] freeword_inverse[of x]
permutation_lift_signed_lconjperm_eq_signed_list_lconjaction'
by force
lemma even_count_lconjseq_rev_relator:
"s∈S ⟹ t∈S ⟹ even (count_list (lconjseq (rev (pair_relator_list s t))) x)"
using even_count_lconjseq_alternating_order2[of t]
by (simp add: genset_order2_add add_order rev_pair_relator_list)
lemma GroupByPresentationInducedFun_S_R_signed_lconjaction:
"GroupByPresentationInducedFun S P signed_lconjpermutation"
proof (intro_locales, rule GroupByPresentation_S_P, unfold_locales)
fix ps assume ps: "ps∈P"
define r where "r = Abs_freeword ps"
with ps have r: "r∈P'" by fast
then obtain s t where st: "s∈S" "t∈S" "r = pair_relator_freeword s t"
using relator_freewords by fast
from r st(3)
have 1: "permutation (lift_signed_lconjperm r) =
signed_list_lconjaction (pair_relator_list s t)"
using P'_FreeS
permutation_lift_signed_lconjperm_eq_signed_list_lconjaction
Abs_freelist_inverse[of "pair_relator_list s t"]
map_fst_map_const_snd[of True "pair_relator_list s t"]
by force
have "permutation (lift_signed_lconjperm r) = id"
proof
fix x
show "lift_signed_lconjperm r → x = id x"
proof
show "snd (freeword_funlift signed_lconjpermutation r → x) = snd (id x)"
using 1 st(1,2) even_count_lconjseq_rev_relator genset_order2_add
set_alternating_list[of "2*relfun s t" s t]
signed_list_lconjaction_snd[of "pair_relator_list s t" x]
by fastforce
qed (simp add: 1 signed_list_lconjaction_fst sum_list_pair_relator_list)
qed
moreover
have "permutation (0::'w signed permutation) = (id::'w signed ⇒ 'w signed)"
using zero_permutation.rep_eq
by fast
ultimately show "lift_signed_lconjperm r = 0"
using permutation_inject by fastforce
qed
end
subsection ‹Coxeter-like systems with deletion›
text ‹
Here we add the so-called deletion condition as an assumption, and explore its consequences.
›
subsubsection ‹Locale definition›
locale PreCoxeterSystemWithDeletion = PreCoxeterSystem S
for S :: "'w::group_add set"
+ assumes deletion:
"ss ∈ lists S ⟹ ¬ reduced_word S ss ⟹
∃a b as bs cs. ss = as @ [a] @ bs @ [b] @ cs ∧
sum_list ss = sum_list (as@bs@cs)"
subsubsection ‹Consequences of the deletion condition›
context PreCoxeterSystemWithDeletion
begin
lemma deletion_reduce:
"ss ∈ lists S ⟹ ∃ts. ts ∈ ssubseqs ss ∩ reduced_words_for S (sum_list ss)"
proof (cases "S_reduced ss")
case True
thus "ss ∈ lists S ⟹
∃ts. ts ∈ ssubseqs ss ∩ reduced_words_for S (sum_list ss)"
by (force simp add: ssubseqs_refl)
next
case False
have "ss ∈ lists S ⟹ ¬ S_reduced ss ⟹
∃ts. ts ∈ ssubseqs ss ∩ reduced_words_for S (sum_list ss)"
proof (induct ss rule: length_induct)
fix xs::"'w list"
assume xs:
"∀ys. length ys < length xs ⟶ ys ∈ lists S ⟶ ¬ S_reduced ys
⟶ (∃ts. ts ∈ ssubseqs ys ∩ reduced_words_for S (sum_list ys))"
"xs ∈ lists S" "¬ S_reduced xs"
from xs(2,3) obtain as a bs b cs
where asbscs: "xs = as@[a]@bs@[b]@cs" "sum_list xs = sum_list (as@bs@cs)"
using deletion[of xs]
by fast
show "∃ts. ts ∈ ssubseqs xs ∩ reduced_words_for S (sum_list xs)"
proof (cases "S_reduced (as@bs@cs)")
case True with asbscs xs(2) show ?thesis
using delete2_ssubseqs by fastforce
next
case False
moreover from asbscs(1) xs(2)
have "length (as@bs@cs) < length xs" "as@bs@cs ∈ lists S"
by auto
ultimately obtain ts
where ts: "ts ∈ ssubseqs (as@bs@cs) ∩
reduced_words_for S (sum_list (as@bs@cs))"
using xs(1,2) asbscs(1)
by fast
with asbscs show ?thesis
using delete2_ssubseqs[of as bs cs a b] ssubseqs_subset by auto
qed
qed
with False
show "ss ∈ lists S ⟹
∃ts. ts ∈ ssubseqs ss ∩ reduced_words_for S (sum_list ss)"
by fast
qed
lemma deletion_reduce':
"ss ∈ lists S ⟹ ∃ts∈reduced_words_for S (sum_list ss). set ts ⊆ set ss"
using deletion_reduce[of ss] subseqs_powset[of ss] by auto
end
subsubsection ‹The exchange condition›
text ‹
The exchange condition states that, given a reduced word in the generators, if prepending a
letter to the word does not remain reduced, then the new word can be shortened to a word
equivalent to the original one by deleting some letter other than the prepended one. Thus, one
able to exchange some letter for the addition of a desired letter at the beginning of a word,
without changing the elemented represented.
›
context PreCoxeterSystemWithDeletion
begin
lemma exchange:
assumes "s∈S" "S_reduced_for w ss" "¬ S_reduced (s#ss)"
shows "∃t as bs. ss = as@t#bs ∧ reduced_word_for S w (s#as@bs)"
proof-
from assms(2) have ss_lists: "ss ∈ lists S" using reduced_word_for_lists by fast
with assms(1) have "s#ss ∈ lists S" by simp
with assms(3) obtain a b as bs cs
where del: "s#ss = as @ [a] @ bs @ [b] @ cs"
"sum_list (s#ss) = sum_list (as@bs@cs)"
using deletion[of "s#ss"]
by fastforce
show ?thesis
proof (cases as)
case Nil with assms(1,2) del show ?thesis
using reduced_word_for_sum_list add.assoc[of s s w] genset_order2_add ss_lists
by (fastforce intro: reduced_word_forI_compare)
next
case (Cons d ds) with del assms(2) show ?thesis
using ss_lists reduced_word_for_imp_reduced_word
reduced_word_for_minimal[of S "sum_list ss" ss "ds@bs@cs"]
by fastforce
qed
qed
lemma reduced_head_imp_exchange:
assumes "reduced_word_for S w (s#as)" "reduced_word_for S w cs"
shows "∃a ds es. cs = ds@[a]@es ∧ reduced_word_for S w (s#ds@es)"
proof-
from assms(1) have s_S: "s∈S" using reduced_word_for_lists by fastforce
moreover have "¬ S_reduced (s#cs)"
proof (rule not_reduced_word_for)
show "as ∈ lists S" using reduced_word_for_lists[OF assms(1)] by simp
from assms(1,2) show "sum_list as = sum_list (s#cs)"
using s_S reduced_word_for_sum_list[of S w] add.assoc[of s s] genset_order2_add
by fastforce
from assms(1,2) show "length as < length (s#cs)"
using reduced_word_for_length[of S w] by fastforce
qed
ultimately obtain a ds es
where "cs = ds@[a]@es" "reduced_word_for S w (s#ds@es)"
using assms(2) exchange[of s w cs]
by auto
thus ?thesis by fast
qed
end
subsubsection ‹More on words in generators containing alternating subwords›
text ‹
Here we explore more of the mechanics of manipulating words over @{term S} that contain
alternating subwords, in preparation of the word problem.
›
context PreCoxeterSystemWithDeletion
begin
lemma two_reduced_heads_imp_reduced_alt_step:
assumes "s≠t" "reduced_word_for S w (t#bs)" "n < relfun s t ∨ relfun s t = 0"
"reduced_word_for S w (alternating_list n s t @ cs)"
shows "∃ds. reduced_word_for S w (alternating_list (Suc n) t s @ ds)"
proof-
define altnst where "altnst = alternating_list n s t"
with assms(2,4) obtain x xs ys
where xxsys: "altnst @ cs = xs@[x]@ys" "reduced_word_for S w (t#xs@ys)"
using reduced_head_imp_exchange
by fast
show ?thesis
proof (cases n rule: nat_cases_2Suc)
case 0 with xxsys(2) show ?thesis by auto
next
case 1 with assms(1,4) xxsys altnst_def show ?thesis
using reduced_word_for_sum_list[of S w "s#cs"]
reduced_word_for_sum_list[of S w "t#cs"]
by (cases xs) auto
next
case (SucSuc k)
with assms(3,4) xxsys altnst_def have "length xs ≥ n"
using exchange_alternating_not_in_alternating by simp
moreover define ds where "ds = take (length xs - n) cs"
ultimately have "t#xs@ys = alternating_list (Suc n) t s @ ds @ ys"
using xxsys(1) altnst_def take_append[of "length xs" altnst cs]
alternating_list_Suc_Cons[of n t]
by (fastforce simp add: length_alternating_list)
with xxsys(2) show ?thesis by auto
qed
qed
lemma two_reduced_heads_imp_reduced_alt':
assumes "s≠t" "reduced_word_for S w (s#as)" "reduced_word_for S w (t#bs)"
shows "n ≤ relfun s t ∨ relfun s t = 0 ⟹ (∃cs.
reduced_word_for S w (alternating_list n s t @ cs) ∨
reduced_word_for S w (alternating_list n t s @ cs)
)"
proof (induct n)
case 0 from assms(2) show ?case by auto
next
case (Suc m) thus ?case
using add_order_add_sym[of s t]
two_reduced_heads_imp_reduced_alt_step[
OF assms(1)[THEN not_sym] assms(2), of m
]
two_reduced_heads_imp_reduced_alt_step[OF assms(1,3), of m]
by fastforce
qed
lemma two_reduced_heads_imp_reduced_alt:
assumes "s≠t" "reduced_word_for S w (s#as)" "reduced_word_for S w (t#bs)"
shows "∃cs. reduced_word_for S w (pair_relator_halflist s t @ cs)"
proof-
define altst altts
where "altst = pair_relator_halflist s t"
and "altts = pair_relator_halflist t s"
then obtain cs
where cs: "reduced_word_for S w (altst @ cs) ∨
reduced_word_for S w (altts @ cs)"
using add_order_add_sym[of t] two_reduced_heads_imp_reduced_alt'[OF assms]
by auto
moreover from altst_def altts_def
have "reduced_word_for S w (altts @ cs) ⟹ reduced_word_for S w (altst @ cs)"
using reduced_word_for_lists[OF assms(2)] reduced_word_for_lists[OF assms(3)]
flip_altsublist_adjacent_def
by (force intro: S_reduced_forI_flip_altsublist_adjacent
simp add: add_order_add_sym)
ultimately show "∃cs. reduced_word_for S w (altst @ cs)" by fast
qed
lemma two_reduced_heads_imp_nzero_relfun:
assumes "s≠t" "reduced_word_for S w (s#as)" "reduced_word_for S w (t#bs)"
shows "relfun s t ≠ 0"
proof
assume 1: "relfun s t = 0"
define altst altts
where "altst = alternating_list (Suc (S_length w)) s t"
and "altts = alternating_list (Suc (S_length w)) t s"
with 1 obtain cs
where "reduced_word_for S w (altst @ cs) ∨
reduced_word_for S w (altts @ cs)"
using two_reduced_heads_imp_reduced_alt'[OF assms]
by fast
moreover from altst_def altts_def
have "length (altst @ cs) > S_length w"
"length (altts @ cs) > S_length w"
using length_alternating_list[of _ s] length_alternating_list[of _ t]
by auto
ultimately show False using reduced_word_for_length by fastforce
qed
end
subsubsection ‹The word problem›
text ‹Here we establish the other direction of the word problem for reduced words.›
context PreCoxeterSystemWithDeletion
begin
lemma reduced_word_problem_ConsCons_step:
assumes "⋀y ss ts. ⟦ S_length y < S_length w; y≠0; reduced_word_for S y ss;
reduced_word_for S y ts ⟧ ⟹ ∃xss. flip_altsublist_chain (ss # xss @ [ts])"
"reduced_word_for S w (a#as)" "reduced_word_for S w (b#bs)" "a≠b"
shows "∃xss. flip_altsublist_chain ((a#as)#xss@[b#bs])"
proof-
from assms(2-4) obtain cs
where cs: "reduced_word_for S w (pair_relator_halflist a b @ cs)"
using two_reduced_heads_imp_reduced_alt
by fast
define rs us where "rs = pair_relator_halflist a b @ cs"
and "us = pair_relator_halflist b a @ cs"
from assms(2,3) have a_S: "a∈S" and b_S: "b∈S"
using reduced_word_for_lists[of S _ "a#as"] reduced_word_for_lists[of S _ "b#bs"]
by auto
with rs_def us_def have midlink: "flip_altsublist_adjacent rs us"
using add_order_add_sym[of b a] flip_altsublist_adjacent_def by fastforce
from assms(2-4) have "relfun a b ≠ 0"
using two_reduced_heads_imp_nzero_relfun by fast
from this obtain k where k: "relfun a b = Suc k"
using not0_implies_Suc by auto
define qs vs
where "qs = alternating_list k b a @ cs"
and "vs = alternating_list k a b @ cs"
with k rs_def us_def have rs': "rs = a # qs" and us': "us = b # vs"
using add_order_add_sym[of b a] alternating_list_Suc_Cons[of k] by auto
from assms(1,2) cs rs_def rs'
have startlink: "as ≠ qs ⟹ ∃xss. flip_altsublist_chain ((a#as) # xss @ [rs])"
using reduced_word_problem_eq_hd_step
by fastforce
from assms(1,3) rs_def cs us'
have endlink: "bs ≠ vs ⟹ ∃xss. flip_altsublist_chain (us # xss @ [b#bs])"
using midlink flip_altsublist_adjacent_sym
S_reduced_forI_flip_altsublist_adjacent[of w rs]
reduced_word_problem_eq_hd_step[of w]
by auto
show ?thesis
proof (cases "as = qs" "bs = vs" rule: two_cases)
case both
with rs' us' have "flip_altsublist_chain ((a#as) # [] @ [b#bs])"
using midlink by simp
thus ?thesis by fast
next
case one
with rs' obtain xss
where "flip_altsublist_chain ((a#as) # (us # xss) @ [b#bs])"
using endlink midlink
by auto
thus ?thesis by fast
next
case other
from other(1) obtain xss where "flip_altsublist_chain ((a#as) # xss @ [rs])"
using startlink by fast
with other(2) us' startlink
have "flip_altsublist_chain ((a#as) # (xss@[rs]) @ [b#bs])"
using midlink binrelchain_snoc[of flip_altsublist_adjacent "(a#as)#xss"]
by simp
thus ?thesis by fast
next
case neither
from neither(1) obtain xss
where "flip_altsublist_chain ((a#as) # xss @ [rs])"
using startlink
by fast
with neither(2) obtain yss
where "flip_altsublist_chain ((a#as) # (xss @ [rs,us] @ yss) @ [b#bs])"
using startlink midlink endlink
binrelchain_join[of flip_altsublist_adjacent "(a#as)#xss"]
by auto
thus ?thesis by fast
qed
qed
lemma reduced_word_problem:
"⟦ w≠0; reduced_word_for S w ss; reduced_word_for S w ts ⟧ ⟹
∃xss. flip_altsublist_chain (ss#xss@[ts])"
proof (induct w arbitrary: ss ts rule: measure_induct_rule[of "S_length"])
case (less w)
show ?case
proof (cases ss ts rule: two_lists_cases_Cons_Cons)
case Nil1 from Nil1(1) less(2,3) show ?thesis
using reduced_word_for_sum_list by fastforce
next
case Nil2 from Nil2(2) less(2,4) show ?thesis
using reduced_word_for_sum_list by fastforce
next
case (ConsCons a as b bs)
show ?thesis
proof (cases "a=b")
case True with less ConsCons show ?thesis
using reduced_word_problem_eq_hd_step[of w] by auto
next
case False with less ConsCons show ?thesis
using reduced_word_problem_ConsCons_step[of w] by simp
qed
qed
qed
lemma reduced_word_letter_set:
assumes "S_reduced_for w ss"
shows "reduced_letter_set S w = set ss"
proof (cases "w=0")
case True with assms show ?thesis
using reduced_word_for_0_imp_nil[of S ss] reduced_letter_set_0 by simp
next
case False
show ?thesis
proof
from assms show "set ss ⊆ reduced_letter_set S w" by fast
show "reduced_letter_set S w ⊆ set ss"
proof
fix x assume "x ∈ reduced_letter_set S w"
from this obtain ts where "reduced_word_for S w ts" "x ∈ set ts" by fast
with False assms show "x ∈ set ss"
using reduced_word_for_lists[of S _ ss] reduced_word_problem[of w ss]
flip_altsublist_chain_set
by force
qed
qed
qed
end
subsubsection ‹Special subgroups and cosets›
text ‹
Recall that special subgroups are those generated by subsets of the generating set @{term S}.
Here we show that the presence of the deletion condition guarantees that the collection of
special subgroups and their left cosets forms a poset under reverse inclusion that satisfies the
necessary properties to ensure that the poset of simplices in the associated simplicial complex
is isomorphic to this poset of special cosets.
›
context PreCoxeterSystemWithDeletion
begin
lemma special_subgroup_int_S:
assumes "T ∈ Pow S"
shows "⟨T⟩ ∩ S = T"
proof
show "⟨T⟩ ∩ S ⊆ T"
proof
fix t assume t: "t ∈ ⟨T⟩ ∩ S"
with assms obtain ts where ts: "ts ∈ lists T" "t = sum_list ts"
using special_subgroup_eq_sum_list[of T] by fast
with assms obtain us
where us: "reduced_word_for S (sum_list ts) us" "set us ⊆ set ts"
using deletion_reduce'[of ts]
by auto
with no_zero_genset ts(2) t have "length us = 1"
using reduced_word_for_lists[of S _ us] reduced_word_for_sum_list[of S _ us]
reduced_word_for_imp_reduced_word[of S _ us] el_reduced[of S]
by auto
with us ts show "t∈T"
using reduced_word_for_sum_list[of S _ us] by (cases us) auto
qed
from assms show "T ⊆ ⟨T⟩ ∩ S" using genby_genset_subset by fast
qed
lemma special_subgroup_inj: "inj_on genby (Pow S)"
using special_subgroup_int_S inj_on_inverseI[of _ "λW. W∩S"] by fastforce
lemma special_subgroup_genby_subset_ordering_iso:
"subset_ordering_iso (Pow S) genby"
proof (unfold_locales, rule genby_mono, simp, rule special_subgroup_inj)
fix X Y assume XY: "X ∈ genby ` Pow S" "Y ∈ genby ` Pow S" "X⊆Y"
from XY(1,2) obtain TX TY
where "TX∈Pow S" "X = ⟨TX⟩" "TY∈Pow S" "Y = ⟨TY⟩"
by auto
hence "the_inv_into (Pow S) genby X = X∩S"
"the_inv_into (Pow S) genby Y = Y∩S"
using the_inv_into_f_f[OF special_subgroup_inj] special_subgroup_int_S
by auto
with XY(3)
show "the_inv_into (Pow S) genby X ⊆ the_inv_into (Pow S) genby Y"
by auto
qed
lemmas special_subgroup_genby_rev_mono
= OrderingSetIso.rev_ordsetmap[OF special_subgroup_genby_subset_ordering_iso]
lemma special_subgroup_word_length:
assumes "T∈Pow S" "w∈⟨T⟩"
shows "word_length T w = S_length w"
proof-
from assms obtain ts where ts: "ts ∈ lists T" "w = sum_list ts"
using special_subgroup_eq_sum_list by auto
with assms(1) obtain us where "us ∈ ssubseqs ts" "S_reduced_for w us"
using deletion_reduce[of ts] by fast
with assms(1) ts(1) show ?thesis
using ssubseqs_lists[of ts] reduced_word_for_sum_list
is_arg_min_size_subprop[of length "word_for S w" us "word_for T w"]
unfolding reduced_word_for_def word_length_def
by fast
qed
lemma S_subset_reduced_imp_S_reduced:
"T∈Pow S ⟹ reduced_word T ts ⟹ S_reduced ts"
using reduced_word_for_lists reduced_word_for_lists[of T _ ts]
reduced_word_for_length[of T "sum_list ts" ts] special_subgroup_eq_sum_list[of T]
special_subgroup_word_length[of T "sum_list ts"]
by (fastforce intro: reduced_word_forI_length)
lemma smallest_genby: "T∈Pow S ⟹ w∈⟨T⟩ ⟹ reduced_letter_set S w ⊆ T"
using genby_S_reduced_word_for_arg_min[of T]
reduced_word_for_imp_reduced_word[of T w]
S_subset_reduced_imp_S_reduced[of T "arg_min length (word_for T w)"]
reduced_word_for_sum_list[of T] reduced_word_for_lists reduced_word_letter_set
by fastforce
lemma special_cosets_below_in:
assumes "w∈W" "T ∈ Pow S"
shows "𝒫.⊇(w +o ⟨T⟩) = (⋃R∈(Pow S).⊇T. {w +o ⟨R⟩})"
proof (rule seteqI)
fix A assume "A ∈ 𝒫.⊇(w +o ⟨T⟩)"
hence A: "A∈𝒫" "A ⊇ (w +o ⟨T⟩)" by auto
from A(1) obtain R w' where "R∈Pow S" "A = w' +o ⟨R⟩"
using special_cosets_def by auto
with A(2) assms(2) show "A ∈ (⋃R∈(Pow S).⊇T. {w +o ⟨R⟩})"
using genby_lcoset_subgroup_imp_eq_reps[of w T w' R]
lcoset_eq_reps_subset[of w "⟨T⟩"]
special_subgroup_genby_rev_mono[of T R]
by auto
next
fix B assume "B ∈ (⋃R∈(Pow S).⊇T. {w +o ⟨R⟩})"
from this obtain R where R: " R ∈ (Pow S).⊇T" "B = w +o ⟨R⟩" by auto
moreover hence "B ⊇ w +o ⟨T⟩"
using genby_mono elt_set_plus_def[of w] by auto
ultimately show "B ∈ special_cosets .⊇ (w +o ⟨T⟩)"
using assms(1) special_cosetsI by auto
qed
lemmas special_coset_inj
= comp_inj_on[OF special_subgroup_inj, OF inj_inj_on, OF lcoset_inj_on]
lemma special_coset_eq_imp_eq_gensets:
"⟦ T1∈Pow S; T2∈Pow S; w1 +o ⟨T1⟩ = w2 +o ⟨T2⟩ ⟧ ⟹ T1=T2"
using set_plus_rearrange2[of "-w1" w1 "⟨T1⟩"]
set_plus_rearrange2[of "-w1" w2 "⟨T2⟩"]
genby_lcoset_subgroup_imp_eq_reps[of 0 T1 "-w1+w2" T2]
inj_onD[OF special_subgroup_inj]
by force
lemma special_subgroup_special_coset_subset_ordering_iso:
"subset_ordering_iso (genby ` Pow S) ((+o) w)"
proof
show "⋀a b. a ⊆ b ⟹ w +o a ⊆ w +o b" using elt_set_plus_def by auto
show 2: "inj_on ((+o) w) (genby ` Pow S)"
using lcoset_inj_on inj_inj_on by fast
show "⋀a b. a ∈ (+o) w ` genby ` Pow S ⟹
b ∈ (+o) w ` genby ` Pow S ⟹
a ⊆ b ⟹
the_inv_into (genby ` Pow S) ((+o) w) a ⊆
the_inv_into (genby ` Pow S) ((+o) w) b"
proof-
fix a b
assume ab : "a ∈ (+o) w ` genby ` Pow S" "b ∈ (+o) w ` genby ` Pow S"
and a_b: "a⊆b"
from ab obtain Ta Tb
where "Ta∈Pow S" "a = w +o ⟨Ta⟩" "Tb∈Pow S" "b = w +o ⟨Tb⟩"
by auto
with a_b
show "the_inv_into (genby ` Pow S) ((+o) w) a ⊆
the_inv_into (genby ` Pow S) ((+o) w) b"
using the_inv_into_f_eq[OF 2] lcoset_eq_reps_subset[of w "⟨Ta⟩" "⟨Tb⟩"]
by simp
qed
qed
lemma special_coset_subset_ordering_iso:
"subset_ordering_iso (Pow S) ((+o) w ∘ genby)"
using special_subgroup_genby_subset_ordering_iso
special_subgroup_special_coset_subset_ordering_iso
by (fast intro: OrderingSetIso.iso_comp)
lemmas special_coset_subset_rev_mono =
OrderingSetIso.rev_ordsetmap[OF special_coset_subset_ordering_iso]
lemma special_coset_below_in_subset_ordering_iso:
"subset_ordering_iso ((Pow S).⊇T) ((+o) w ∘ genby)"
using special_coset_subset_ordering_iso by (auto intro: OrderingSetIso.iso_subset)
lemma special_coset_below_in_supset_ordering_iso:
"OrderingSetIso (⊇) (⊃) (⊇) (⊃) ((Pow S).⊇T) ((+o) w ∘ genby)"
using special_coset_below_in_subset_ordering_iso OrderingSetIso.iso_dual by fast
lemma special_coset_pseudominimals:
assumes "supset_pseudominimal_in 𝒫 X"
shows "∃w s. w∈W ∧ s∈S ∧ X = w +o ⟨S-{s}⟩"
proof-
from assms have "X∈𝒫" using supset_pseudominimal_inD1 by fast
from this obtain w T where wT: "w∈W" "T∈Pow S" "X = w +o ⟨T⟩"
using special_cosets_def by auto
show ?thesis
proof (cases "T=S")
case True with wT(1,3) assms show ?thesis
using genby_lcoset_el_reduce supset_pseudominimal_ne_bottom
special_cosets_bottom
by fast
next
case False
with wT(2) obtain s where s: "s∈S" "T ⊆ S-{s}" by fast
from s(2) wT(1,3) assms have "X ⊆ w +o ⟨S-{s}⟩"
using genby_mono by auto
moreover from assms wT(1) s(1) have "¬ X ⊂ w +o ⟨S-{s}⟩"
using special_cosetsI[of _ w]
supset_pseudominimal_inD2[of 𝒫 X "w +o ⟨S-{s}⟩"]
lcoset_eq_reps[of w _ "⟨S⟩"]
inj_onD[OF special_subgroup_inj, of "S-{s}" S]
by (auto simp add: special_cosets_bottom genby_lcoset_el_reduce)
ultimately show ?thesis using wT(1) s(1) by fast
qed
qed
lemma special_coset_pseudominimal_in_below_in:
assumes "w∈W" "T∈Pow S" "supset_pseudominimal_in (𝒫.⊇(w +o ⟨T⟩)) X"
shows "∃s∈S-T. X = w +o ⟨S-{s}⟩"
proof-
from assms obtain v s where vs: "v∈W" "s∈S" "X = v +o ⟨S-{s}⟩"
using special_cosets_has_bottom special_cosetsI[of T w]
supset_has_bottom_pseudominimal_in_below_in
special_coset_pseudominimals
by force
from assms(3) have X: "X ⊇ w +o ⟨T⟩"
using supset_pseudominimal_inD1 by fast
with vs(3) have 1: "X = w +o ⟨S-{s}⟩"
using genby_lcoset_subgroup_imp_eq_reps[of w T v "S-{s}"] by fast
with X assms have "T ⊆ S-{s}"
using special_cosetsI special_coset_subset_rev_mono[of T "S-{s}"]
by fastforce
with vs(2) show ?thesis using 1 by fast
qed
lemma exclude_one_is_pseudominimal:
assumes "w∈W" "t∈S"
shows "supset_pseudominimal_in 𝒫 (w +o ⟨S-{t}⟩)"
proof (rule supset_pseudominimal_inI, rule special_cosetsI)
show "w ∈ W" by fact
from assms have "w +o ⟨S - {t}⟩ ≠ W"
using genby_lcoset_el_reduce[of w] lcoset_eq_reps[of w _ W]
inj_onD[OF special_subgroup_inj, of "S-{t}" S]
by auto
thus "w +o ⟨S - {t}⟩ ≠ supset_bottom 𝒫"
using special_cosets_bottom by fast
next
fix X assume X: "X∈𝒫" "w +o ⟨S - {t}⟩ ⊂ X"
with assms(1) have "X ∈ (⋃R∈(Pow S).⊇(S-{t}). {w +o ⟨R⟩})"
using subst[OF special_cosets_below_in, of w "S-{t}" "λA. X∈A"] by fast
from this obtain R where R: "R ∈ (Pow S).⊇(S-{t})" "X = w +o ⟨R⟩" by auto
from R(2) X(2) have "R ≠ S-{t}" by fast
with R(1) have "R=S" by auto
with assms(1) R(2) show "X = supset_bottom 𝒫"
using genby_lcoset_el_reduce special_cosets_bottom by fast
qed fast
lemma exclude_one_is_pseudominimal_in_below_in:
"⟦ w∈W; T∈Pow S; s∈S-T ⟧ ⟹
supset_pseudominimal_in (𝒫.⊇(w +o ⟨T⟩)) (w +o ⟨S-{s}⟩)"
using special_cosets_has_bottom special_cosetsI
exclude_one_is_pseudominimal[of w s]
genby_mono[of T "S-{s}"]
supset_has_bottom_pseudominimal_in_below_inI[
of 𝒫 "w +o ⟨T⟩" "w +o ⟨S-{s}⟩"
]
by auto
lemma glb_special_subset_coset:
assumes wTT': "w∈ W" "T ∈ Pow S" "T' ∈ Pow S"
defines U: "U ≡ T ∪ T' ∪ reduced_letter_set S w"
shows "supset_glbound_in_of 𝒫 ⟨T⟩ (w +o ⟨T'⟩) ⟨U⟩"
proof (rule supset_glbound_in_ofI)
from wTT'(2,3) U show "⟨U⟩ ∈ 𝒫"
using reduced_letter_set_subset[of S] special_subgroup_special_coset by simp
show "supset_lbound_of ⟨T⟩ (w +o ⟨T'⟩) ⟨U⟩"
proof (rule supset_lbound_ofI)
from U show "⟨T⟩ ⊆ ⟨U⟩" using genby_mono[of T U] by fast
show "w +o ⟨T'⟩ ⊆ ⟨U⟩"
proof
fix x assume "x ∈ w +o ⟨T'⟩"
with wTT'(3) obtain y where y: "y ∈ ⟨T'⟩" "x = w + y"
using elt_set_plus_def[of w] by auto
with wTT'(1) U show "x ∈ ⟨U⟩"
using in_genby_S_reduced_letter_set genby_mono[of _ U]
genby_mono[of T' U] genby_add_closed[of w U y]
by auto
qed
qed
next
fix X assume X: "X∈𝒫" "supset_lbound_of ⟨T⟩ (w +o ⟨T'⟩) X"
from X(1) obtain v R where vR: "R∈Pow S" "X = v +o ⟨R⟩"
using special_cosets_def by auto
from X(2) have X': "X ⊇ ⟨T⟩" "X ⊇ w +o ⟨T'⟩"
using supset_lbound_of_def[of _ _ X] by auto
from X'(1) vR(2) have R: "X = ⟨R⟩"
using genby_0_closed genby_lcoset_el_reduce0 by fast
with X'(2) have w: "w∈⟨R⟩" using genby_0_closed lcoset_refl by fast
have "T' ⊆ R"
proof (
rule special_subgroup_genby_rev_mono, rule wTT'(3), rule vR(1), rule subsetI
)
fix x assume "x ∈ ⟨T'⟩"
with X'(2) R show "x ∈ ⟨R⟩"
using elt_set_plus_def[of w "⟨T'⟩"] w genby_uminus_add_closed[of "w" R "w+x"]
by auto
qed
with X'(1) wTT'(2) vR(1) show "⟨U⟩⊆X"
using special_subgroup_genby_rev_mono[of T R] w smallest_genby U R
genby_mono[of _ R]
by simp
qed
lemma glb_special_subset_coset_ex:
assumes "w∈ W" "T ∈ Pow S" "T' ∈ Pow S"
shows "∃B. supset_glbound_in_of 𝒫 ⟨T⟩ (w +o ⟨T'⟩) B"
using glb_special_subset_coset[OF assms]
by fast
lemma special_cosets_have_glbs:
assumes "X∈𝒫" "Y∈𝒫"
shows "∃B. supset_glbound_in_of 𝒫 X Y B"
proof-
from assms obtain wx Tx wy Ty
where X: "wx ∈ W" "Tx ∈ Pow S" "X = wx +o ⟨Tx⟩"
and Y: "wy ∈ W" "Ty ∈ Pow S" "Y = wy +o ⟨Ty⟩"
using special_cosets_def
by auto
from X(1,2) Y(1,2) obtain A
where A: "supset_glbound_in_of 𝒫 ⟨Tx⟩ ((-wx+wy) +o ⟨Ty⟩) A"
using genby_uminus_add_closed[of wx] glb_special_subset_coset_ex by fastforce
from X(1,3) Y(3) have "supset_glbound_in_of 𝒫 X Y (wx +o A)"
using supset_glbound_in_of_lcoset_shift[OF A, of wx]
by (auto simp add: set_plus_rearrange2 special_cosets_lcoset_shift)
thus ?thesis by fast
qed
end
subsection ‹Coxeter systems›
subsubsection ‹Locale definition and transfer from the associated free group›
text ‹
Now we consider groups generated by elements of order two with an additional assumption to ensure
that the natural correspondence between the group @{term W} and the group presentation on the
generating set @{term S} and its relations is bijective. Below, such groups will be shown to
satisfy the deletion condition.
›
locale CoxeterSystem = PreCoxeterSystem S
for S :: "'w::group_add set"
+ assumes induced_id_inj: "inj_on induced_id G"
lemma (in PreCoxeterSystem) CoxeterSystemI:
assumes "⋀g. g∈G ⟹ induced_id g = 0 ⟹ g=0"
shows "CoxeterSystem S"
proof
from assms have "GroupIso G induced_id"
using GroupWithGeneratorsRelators_S_R
GroupWithGeneratorsRelators.induced_id_hom_surj(1)
by (fast intro: GroupHom.isoI)
thus "inj_on induced_id G" using GroupIso.inj_on by fast
qed
context CoxeterSystem
begin
abbreviation "inv_induced_id ≡ GroupPresentation.inv_induced_id S R"
lemma GroupPresentation_S_R: "GroupPresentation S R"
by (
intro_locales, rule GroupWithGeneratorsRelators_S_R,
unfold_locales, rule induced_id_inj
)
lemmas inv_induced_id_sum_list =
GroupPresentation.inv_induced_id_sum_list_S[OF GroupPresentation_S_R]
end
subsubsection ‹The deletion condition is necessary›
text ‹
Call an element of @{term W} a reflection if it is a conjugate of a generating element (and so
is also of order two). Here we use the action of words over @{term S} on such reflections to show
that Coxeter systems satisfy the deletion condition.
›
context CoxeterSystem
begin
abbreviation "induced_signed_lconjperm ≡
GroupByPresentationInducedFun.induced_hom S P signed_lconjpermutation"
definition flipped_reflections :: "'w ⇒ 'w set"
where "flipped_reflections w ≡
{t∈ℋ. induced_signed_lconjperm (inv_induced_id (-w)) →
(t,True) = (rconjby w t, False)}"
lemma induced_signed_lconjperm_inv_induced_id_sum_list:
"ss ∈ lists S ⟹ induced_signed_lconjperm (inv_induced_id (sum_list ss)) =
sum_list (map signed_lconjpermutation ss)"
by (simp add:
inv_induced_id_sum_list Abs_freelist_in_FreeGroup
GroupByPresentationInducedFun.induced_hom_Abs_freelist_conv_sum_list[
OF GroupByPresentationInducedFun_S_R_signed_lconjaction
]
)
lemma induced_signed_eq_lconjpermutation:
"ss ∈ lists S ⟹
permutation (induced_signed_lconjperm (inv_induced_id (sum_list ss))) =
signed_list_lconjaction ss"
proof (induct ss)
case Nil
have "permutation (induced_signed_lconjperm (inv_induced_id (sum_list []))) = id"
using induced_signed_lconjperm_inv_induced_id_sum_list[of "[]"]
zero_permutation.rep_eq
by simp
thus ?case by fastforce
next
case (Cons s ss)
from Cons(2)
have "induced_signed_lconjperm (inv_induced_id (sum_list (s#ss))) =
signed_lconjpermutation s + sum_list (map signed_lconjpermutation ss)"
using induced_signed_lconjperm_inv_induced_id_sum_list[of "s#ss"]
by simp
with Cons(2) have
"permutation (induced_signed_lconjperm (inv_induced_id (sum_list (s#ss)))) =
permutation (signed_lconjpermutation s) ∘
permutation (induced_signed_lconjperm (inv_induced_id (sum_list ss)))"
using plus_permutation.rep_eq induced_signed_lconjperm_inv_induced_id_sum_list
by simp
with Cons show ?case
using bij_signed_lconjaction[of s] Abs_permutation_inverse by fastforce
qed
lemma flipped_reflections_odd_lconjseq:
assumes "ss∈lists S"
shows "flipped_reflections (sum_list ss) = {t∈ℋ. odd (count_list (lconjseq ss) t)}"
proof (rule seteqI)
fix t assume "t ∈ flipped_reflections (sum_list ss)"
moreover with assms
have "snd (signed_list_lconjaction (rev ss) (t,True)) = False"
using flipped_reflections_def genset_order2_add uminus_sum_list_order2
induced_signed_eq_lconjpermutation[of "rev ss"]
by force
ultimately show "t ∈ {t∈ℋ. odd (count_list (lconjseq ss) t)}"
using assms flipped_reflections_def genset_order2_add
signed_list_lconjaction_snd[of "rev ss"]
by auto
next
fix t assume t: "t ∈ {t∈ℋ. odd (count_list (lconjseq ss) t)}"
with assms
have "signed_list_lconjaction (rev ss) (t,True) =
(rconjby (sum_list ss) t, False)"
using genset_order2_add signed_list_lconjaction_snd[of "rev ss"]
signed_list_lconjaction_fst[of "rev ss"]
uminus_sum_list_order2[of ss, THEN sym]
by (auto intro: prod_eqI)
with t assms show "t ∈ flipped_reflections (sum_list ss)"
using induced_signed_eq_lconjpermutation[of "rev ss"] genset_order2_add
uminus_sum_list_order2 flipped_reflections_def
by fastforce
qed
lemma flipped_reflections_in_lconjseq:
"ss∈lists S ⟹ flipped_reflections (sum_list ss) ⊆ set (lconjseq ss)"
using flipped_reflections_odd_lconjseq odd_n0 count_notin[of _ "lconjseq ss"]
by fastforce
lemma flipped_reflections_distinct_lconjseq_eq_lconjseq:
assumes "ss∈lists S" "distinct (lconjseq ss)"
shows "flipped_reflections (sum_list ss) = set (lconjseq ss)"
proof
from assms(1) show "flipped_reflections (sum_list ss) ⊆ set (lconjseq ss)"
using flipped_reflections_in_lconjseq by fast
show "flipped_reflections (sum_list ss) ⊇ set (lconjseq ss)"
proof
fix t assume "t ∈ set (lconjseq ss)"
moreover with assms(2) have "count_list (lconjseq ss) t = 1"
by (simp add: distinct_count_list)
ultimately show "t ∈ flipped_reflections (sum_list ss)"
using assms(1) flipped_reflections_odd_lconjseq lconjseq_reflections
by fastforce
qed
qed
lemma flipped_reflections_reduced_eq_lconjseq:
"S_reduced ss ⟹ flipped_reflections (sum_list ss) = set (lconjseq ss)"
using reduced_word_for_lists[of S] S_reduced_imp_distinct_lconjseq
flipped_reflections_distinct_lconjseq_eq_lconjseq
by fast
lemma card_flipped_reflections:
assumes "w∈W"
shows "card (flipped_reflections w) = S_length w"
proof-
define ss where "ss = arg_min length (word_for S w)"
with assms have "S_reduced_for w ss"
using genby_S_reduced_word_for_arg_min by simp
thus ?thesis
using reduced_word_for_sum_list flipped_reflections_reduced_eq_lconjseq
S_reduced_imp_distinct_lconjseq distinct_card length_lconjseq[of ss]
reduced_word_for_length
by fastforce
qed
end
sublocale CoxeterSystem < PreCoxeterSystemWithDeletion
proof
fix ss assume ss: "ss ∈ lists S" "¬ S_reduced ss"
define w where "w = sum_list ss"
with ss(1)
have "distinct (lconjseq ss) ⟹ card (flipped_reflections w) = length ss"
by (simp add:
flipped_reflections_distinct_lconjseq_eq_lconjseq distinct_card
length_lconjseq)
moreover from w_def ss have "length ss > S_length w" using word_length_lt by fast
moreover from w_def ss(1) have "card (flipped_reflections w) = S_length w"
using special_subgroup_eq_sum_list card_flipped_reflections by fast
ultimately have "¬ distinct (lconjseq ss)" by auto
with w_def ss
show "∃a b as bs cs. ss = as @ [a] @ bs @ [b] @ cs ∧
sum_list ss = sum_list (as @ bs @ cs)"
using deletion'
by fast
qed
subsubsection ‹The deletion condition is sufficient›
text ‹
Now we come full circle and show that a pair consisting of a group and a generating set of
order-two elements that satisfies the deletion condition affords a presentation that makes it a
Coxeter system.
›
context PreCoxeterSystemWithDeletion
begin
lemma reducible_by_flipping:
"ss ∈ lists S ⟹ ¬ S_reduced ss ⟹
∃xss as t bs. flip_altsublist_chain (ss # xss @ [as@[t,t]@bs])"
proof (induct ss)
case (Cons s ss)
show ?case
proof (cases "S_reduced ss")
case True
define w where "w = sum_list ss"
with True have ss_red_w: "reduced_word_for S w ss" by fast
moreover from Cons(2) have "s∈S" by simp
ultimately obtain as bs where asbs: "reduced_word_for S w (s#as@bs)"
using Cons(3) exchange by fast
show ?thesis
proof (cases "w=0")
case True with asbs show ?thesis
using reduced_word_for_0_imp_nil by fast
next
case False
from this obtain xss where "flip_altsublist_chain (ss # xss @ [s#as@bs])"
using ss_red_w asbs reduced_word_problem by fast
hence "flip_altsublist_chain (
(s#ss) # map ((#) s) xss @ [[]@[s,s]@(as@bs)]
)"
using flip_altsublist_chain_map_Cons_grow by fastforce
thus ?thesis by fast
qed
next
case False
with Cons(1,2) obtain xss as t bs
where "flip_altsublist_chain (
(s#ss) # map ((#) s) xss @ [(s#as)@[t,t]@bs]
)"
using flip_altsublist_chain_map_Cons_grow
by fastforce
thus ?thesis by fast
qed
qed (simp add: nil_reduced_word_for_0)
lemma freeliftid_kernel':
"ss ∈ lists S ⟹ sum_list ss = 0 ⟹ Abs_freelist ss ∈ Q"
proof (induct ss rule: length_induct)
fix ss
assume step: "∀ts. length ts < length ss ⟶ ts ∈ lists S ⟶
sum_list ts = 0 ⟶ Abs_freelist ts ∈ Q"
and set_up: "ss ∈ lists S" "sum_list ss = 0"
show "Abs_freelist ss ∈ Q"
proof (cases "ss=[]")
case True thus ?thesis
using genby_0_closed[of "⋃w∈FreeGroup S. lconjby w ` P'"]
by (auto simp add: zero_freeword.abs_eq)
next
case False
with set_up obtain xss as t bs
where xss: "flip_altsublist_chain (ss # xss @ [as@[t,t]@bs])"
using sum_list_zero_nreduced reducible_by_flipping[of ss]
by fast
with set_up
have astbs: "length (as@[t,t]@bs) = length ss"
"as@[t,t]@bs ∈ lists S"
"sum_list (as@[t,t]@bs) = 0"
using flip_altsublist_chain_length[of ss xss "as@[t,t]@bs"]
flip_altsublist_chain_sum_list[of ss xss "as@[t,t]@bs"]
flip_altsublist_chain_lists[of ss xss "as@[t,t]@bs"]
by auto
have listsS: "as ∈ lists S" "t∈S" "bs∈lists S" using astbs(2) by auto
have "sum_list as + (t + t + sum_list bs) = 0"
using astbs(3) by (simp add: add.assoc)
hence "sum_list (as@bs) = 0"
using listsS(2) by (simp add: genset_order2_add)
moreover have "length (as@bs) < length ss" using astbs(1) by simp
moreover have "as@bs ∈ lists S" using listsS(1,3) by simp
ultimately have "Abs_freelist (as@bs) ∈ Q" using step by fast
hence "Abs_freelist as + pair_relator_freeword t t +
(- Abs_freelist as + (Abs_freelist as + Abs_freelist bs)) ∈ Q"
using listsS(1,2) lconjby_Abs_freelist_relator_freeword[of t t as]
genby_add_closed
by (simp add: Abs_freelist_append[THEN sym] add.assoc[THEN sym])
hence "Abs_freelist as + Abs_freelist [t,t] + Abs_freelist bs ∈ Q"
using listsS(2) by (simp add: S_relator_freeword Abs_freeletter_add)
thus ?thesis
using Abs_freelist_append_append[of as "[t,t]" bs]
rev_flip_altsublist_chain[OF xss]
flip_altsublist_chain_G_in_Q[of "as@[t,t]@bs" "rev xss" ss]
by simp
qed
qed
lemma freeliftid_kernel:
assumes "c ∈ FreeGroup S" "freeliftid c = 0"
shows "c∈Q"
proof-
from assms(2) have "freeliftid (Abs_freeword (freeword c)) = 0"
by (simp add: freeword_inverse)
with assms(1) have "sum_list (map fst (freeword c)) = 0"
using FreeGroup_def freeword freeliftid_Abs_freeword_conv_sum_list by fastforce
with assms(1) show ?thesis
using FreeGroup_def freeliftid_kernel'[of "map fst (freeword c)"]
Q_freelist_freeword
by fastforce
qed
lemma induced_id_kernel:
"c ∈ FreeGroup S ⟹ induced_id (⌈FreeGroup S|c|Q⌉) = 0 ⟹ c∈Q"
by (simp add:
freeliftid_kernel
GroupByPresentationInducedFun.induced_hom_equality[
OF GroupByPresentationInducedFun_S_P_id
]
)
theorem CoxeterSystem: "CoxeterSystem S"
proof (