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 (* context PreCoxeterSystem *) 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 (* context PreCoxeterSystem *) 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 (* context PreCoxeterSystem *) 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] same_length_eq_append[of altnts "xs@[x]" cs ys] 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 (* context PreCoxeterSystem *) 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] ― ‹This lemma represents one direction in the word problem: if a word in generators can be transformed into another by a sequence of manipulations, each of which consists of replacing a half-relator subword by its reversal, then the two words sum to the same element of @{term W}.› 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 (* context PreCoxeterSystem *) 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)" ― ‹the set of reflections› 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 (* context PreCoxeterSystem *) 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 (* context PreCoxeterSystemWithDeletion *) 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 (* context PreCoxeterSystemWithDeletion *) 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 (* context PreCoxeterSystemWithDeletion *) 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 (* context PreCoxeterSystemWithDeletion *) 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 (* context PreCoxeterSystemWithDeletion *) 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 (* context CoxeterSystem *) 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 (* context CoxeterSystem *) 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 (rule CoxeterSystemI) fix x assume x: "x∈G" "induced_id x = 0" from x(1) obtain c where "c ∈ FreeGroup S" "x = (⌈FreeGroup S|c|Q⌉)" using Group.quotient_group_UN FreeGroup_Group by fast with x(2) show "x=0" using induced_id_kernel Group.quotient_identity_rule[OF FreeGroup_Group] GroupByPresentation.Q_subgroup_FreeS[OF GroupByPresentation_S_P] GroupByPresentation.normal_Q[OF GroupByPresentation_S_P] by auto qed end (* context PreCoxeterSystemWithDeletion *) subsubsection ‹The Coxeter system associated to a thin chamber complex with many foldings› text ‹ We now show that the fundamental automorphisms in a thin chamber complex with many foldings satisfy the deletion condition, and hence form a Coxeter system. › context ThinChamberComplexManyFoldings begin lemma not_reduced_word_not_min_gallery: assumes "ss ∈ lists S" "¬ reduced_word S ss" shows "¬ min_gallery (map (λw. w`→C0) (sums ss))" proof (cases ss rule: list_cases_Cons_snoc) case Nil with assms(2) show ?thesis using nil_reduced_word_for_0 by auto next case (Single s) with assms show ?thesis using zero_notin_S reduced_word_singleton[of s S] by fastforce next case (Cons_snoc s ts t) have ss: "ss = s#ts@[t]" by fact define Ms where "Ms = map (λw. w`→C0) (map ((+) s) (sums ts))" with ss have C0_ms_ss_C0: "map (λw. w`→C0) (sums ss) = C0 # Ms @ [sum_list ss `→ C0]" by (simp add: sums_snoc zero_permutation.rep_eq) define rs where "rs = arg_min length (word_for S (sum_list ss))" with assms(1) have rs: "rs ∈ lists S" "sum_list rs = sum_list ss" using arg_min_natI[of "λrs. word_for S (sum_list ss) rs" ss length] by auto show ?thesis proof (cases rs rule: list_cases_Cons_snoc) case Nil hence "sum_list ss `→ C0 = C0" using rs(2) by (fastforce simp add: zero_permutation.rep_eq) with C0_ms_ss_C0 show ?thesis by simp next case (Single r) from Single have "min_gallery [C0,r`→C0]" using rs(1) fundchamber fundchamber_S_chamber fundchamber_S_adjacent fundchamber_S_image_neq_fundchamber by (fastforce intro: min_gallery_adj) with Single C0_ms_ss_C0 Ms_def show ?thesis using rs(2) min_galleryD_min_betw[of C0 Ms "sum_list ss `→ C0" "[]"] min_galleryD_gallery by (fastforce simp add: length_sums) next case (Cons_snoc p qs q) define Ns where "Ns = map (λw. w`→C0) (map ((+) p) (sums qs))" from assms rs_def have "length rs < length ss" using word_length_lt[of ss S] reduced_word_for_length reduced_word_for_arg_min[of ss S] by force with Cons_snoc ss Ms_def Ns_def have "length Ns < length Ms" by (simp add: length_sums) moreover from Ns_def Cons_snoc have "gallery (C0 # Ns @ [sum_list ss `→ C0])" using rs S_list_image_gallery[of rs] by (auto simp add: sums_snoc zero_permutation.rep_eq) ultimately show ?thesis using C0_ms_ss_C0 not_min_galleryI_betw by auto qed qed lemma S_list_not_min_gallery_double_split: assumes "ss ∈ lists S" "ss≠[]" "¬ min_gallery (map (λw. w`→C0) (sums ss))" shows "∃f g as s bs t cs. (f,g)∈foldpairs ∧ sum_list as `→ C0 ∈ f⊢𝒞 ∧ sum_list (as@[s]) `→ C0 ∈ g⊢𝒞 ∧ sum_list (as@[s]@bs) `→ C0 ∈ g⊢𝒞 ∧ sum_list (as@[s]@bs@[t]) `→ C0 ∈ f⊢𝒞 ∧ ss = as@[s]@bs@[t]@cs" proof- define Cs where "Cs = map (λw. w`→C0) (sums ss)" moreover from assms(1) Cs_def have "gallery Cs" using S_list_image_gallery by fastforce moreover from assms(1) Cs_def have "{} ∉ set (wall_crossings Cs)" using S_list_image_crosses_walls by fastforce ultimately obtain f g As A B Bs E F Fs where fg : "(f,g)∈foldpairs" and sep : "A∈f⊢𝒞" "B∈g⊢𝒞" "E∈g⊢𝒞" "F∈f⊢𝒞" and decomp_cases: "Cs = As@[A,B,F]@Fs ∨ Cs = As@[A,B]@Bs@[E,F]@Fs" using assms(3) not_min_gallery_double_split[of Cs] by blast show ?thesis proof (cases "Cs = As@[A,B,F]@Fs") case True define bs :: "'a permutation list" where "bs = []" from True Cs_def obtain as s t cs where "ss = as@[s,t]@cs" "A = sum_list as `→ C0" "B = sum_list (as@[s]) `→ C0" "F = sum_list (as@[s,t]) `→ C0" using pullback_sums_map_middle3[of "λw. w`→C0" ss As A B F Fs] by auto with sep(1,2,4) bs_def have "sum_list as `→ C0 ∈ f⊢𝒞" "sum_list (as@[s]) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs@[t]) `→ C0 ∈ f⊢𝒞" "ss = as@[s]@bs@[t]@cs" by auto with fg show ?thesis by blast next case False with Cs_def decomp_cases obtain as s bs t cs where "ss = as@[s]@bs@[t]@cs" "A = sum_list as `→ C0" "B = sum_list (as@[s]) `→ C0" "E = sum_list (as@[s]@bs) `→ C0" "F = sum_list (as@[s]@bs@[t]) `→ C0" using pullback_sums_map_double_middle2[ of "λw. w`→C0" ss As A B Bs E F Fs ] by auto with sep have "sum_list as `→ C0 ∈ f⊢𝒞" "sum_list (as@[s]) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs@[t]) `→ C0 ∈ f⊢𝒞" "ss = as@[s]@bs@[t]@cs" by auto with fg show ?thesis by blast qed qed lemma fold_end_sum_chain_fg: fixes f g :: "'a⇒'a" defines 𝗌 : "𝗌 ≡ induced_automorph f g" assumes fg : "(f,g) ∈ foldpairs" and as : "as ∈ lists S" and s : "s∈S" and sep: "sum_list as `→ C0 ∈ f⊢𝒞" "sum_list (as@[s]) `→ C0 ∈ g⊢𝒞" shows "bs ∈lists S ⟹ 𝗌 ` sum_list (as@[s]@bs) `→ C0 = sum_list (as@bs) `→ C0" proof- from fg obtain C where C: "OpposedThinChamberComplexFoldings X f g C" using foldpairs_def by fast show "bs ∈lists S ⟹ 𝗌 ` sum_list (as@[s]@bs) `→ C0 = sum_list (as@bs) `→ C0" proof (induct bs rule: rev_induct) case Nil from 𝗌 as s sep C show ?case using sum_list_S_in_W[of as] sum_list_append[of as "[s]"] fundchamber_WS_image_adjacent by (auto simp add: OpposedThinChamberComplexFoldings.indaut_adj_halfchsys_im_fg ) next case (snoc b bs) define bC0 B where "bC0 = b`→C0" and "B = sum_list (as@bs) `→ C0" define y where "y = C0∩bC0" define z z' where "z = 𝗌 ` sum_list (as@[s]@bs) `→ y" and "z' = sum_list (as@bs) `→ y" from snoc B_def have B': "𝗌 ` sum_list (as@[s]@bs) `→ C0 = B" by simp obtain φ where φ: "label_wrt C0 φ" using ex_label_map by fast from bC0_def y_def snoc(2) obtain u where u: "bC0 = insert u y" using fundchamber_S_adjacent[of b] adjacent_sym fundchamber_S_image_neq_fundchamber adjacent_int_decomp[of bC0 C0] by (auto simp add: Int_commute) define v v' where "v = 𝗌 (sum_list (as@[s]@bs) → u)" and "v' = sum_list (as@bs) → u" from bC0_def u v_def z_def v'_def z'_def have ins_vz : "𝗌 ` sum_list (as@[s]@bs@[b]) `→ C0 = insert v z" and ins_vz': "sum_list (as@bs@[b]) `→ C0 = insert v' z'" using image_insert[of "permutation (sum_list (as@[s]@bs))" u y, THEN sym] image_insert[ of 𝗌 "sum_list (as@[s]@bs)→u" "sum_list (as@[s]@bs)`→y", THEN sym] image_insert[of "permutation (sum_list (as@bs))" u y, THEN sym] by (auto simp add: plus_permutation.rep_eq image_comp) from as s snoc(2) have sums: "sum_list (as@[s]@bs) ∈ W" "sum_list (as@bs) ∈ W" "sum_list (as@[s]@bs@[b]) ∈ W" "sum_list (as@bs@[b]) ∈ W" using sum_list_S_in_W[of "as@[s]@bs"] sum_list_S_in_W[of "as@bs"] sum_list_S_in_W[of "as@[s]@bs@[b]"] sum_list_S_in_W[of "as@bs@[b]"] by auto from u bC0_def snoc(2) have u: "u∈⋃X" using fundchamber_S_chamber[of b] chamberD_simplex[of bC0] by auto moreover from as s snoc(2) u have "sum_list (as@[s]@bs) → u ∈ ⋃X" using sums(1) ChamberComplexEndomorphism.vertex_map[OF W_endomorphism] by fastforce ultimately have "φ v = φ v'" using 𝗌 v_def v'_def sums(1,2) W_respects_labels[OF φ, of "sum_list (as@[s]@bs)" u] W_respects_labels[OF φ, of "sum_list (as@bs)" u] OpposedThinChamberComplexFoldings.indaut_resplabels[ OF C φ ] by simp moreover from 𝗌 have "chamber (insert v z)" "chamber (insert v' z')" using sums(3,4) fundchamber_W_image_chamber[of "sum_list (as@[s]@bs@[b])"] OpposedThinChamberComplexFoldings.indaut_chmap[ OF C ] fundchamber_W_image_chamber[of "sum_list (as@bs@[b])"] by (auto simp add: ins_vz[THEN sym] ins_vz'[THEN sym]) moreover from y_def z_def z'_def bC0_def B_def snoc(2) 𝗌 have "z⊲B" "z'⊲B" using B' sums(1,2) fundchamber_S_adjacent[of b] fundchamber_S_image_neq_fundchamber[of b] adjacent_int_facet1[of C0] W_endomorphism[of "sum_list (as@bs)"] W_endomorphism[of "sum_list (as@[s]@bs)"] fundchamber fundchamber_W_image_chamber[of "sum_list (as@[s]@bs)"] ChamberComplexEndomorphism.facet_map[of X] OpposedThinChamberComplexFoldings.indaut_morph[ OF C ] ChamberComplexEndomorphism.facet_map[ of X 𝗌 "sum_list (as@[s]@bs) `→ C0" ] by auto moreover from snoc(2) B_def 𝗌 have "insert v z ≠ B" "insert v' z' ≠ B" using sum_list_append[of "as@[s]@bs" "[b]"] sum_list_append[of "as@bs" "[b]"] fundchamber_next_WS_image_neq[of b "sum_list (as@[s]@bs)"] fundchamber_next_WS_image_neq[of b "sum_list (as@bs)"] OpposedThinChamberComplexFoldings.indaut_aut[ OF C ] ChamberComplexAutomorphism.bij bij_is_inj B' inj_eq_image[ of 𝗌 "sum_list (as@[s]@bs@[b]) `→ C0" "sum_list (as@[s]@bs) `→ C0" ] by (auto simp add: ins_vz[THEN sym] ins_vz'[THEN sym]) ultimately show ?case using B_def sums(2) fundchamber_W_image_chamber[of "sum_list (as@bs)"] label_wrt_eq_on_adjacent_vertex[OF φ, of v v' B z z'] by (auto simp add: ins_vz[THEN sym] ins_vz'[THEN sym]) qed qed lemma fold_end_sum_chain_gf: fixes f g :: "'a⇒'a" defines "𝗌 ≡ induced_automorph f g" assumes fg : "(f,g) ∈ foldpairs" and "as ∈ lists S" "s∈S" "bs ∈lists S" "sum_list as `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]) `→ C0 ∈ f⊢𝒞" shows "𝗌 ` sum_list (as@[s]@bs) `→ C0 = sum_list (as@bs) `→ C0" proof- from fg obtain C where C: "OpposedThinChamberComplexFoldings X f g C" using foldpairs_def by fast from assms show ?thesis using foldpairs_sym fold_end_sum_chain_fg[of g f as s bs] OpposedThinChamberComplexFoldings.induced_automorphism_sym[OF C] by simp qed lemma fold_middle_sum_chain: assumes fg : "(f,g) ∈ foldpairs" and S : "as ∈ lists S" "s∈S" "bs ∈ lists S" "t∈S" "cs ∈lists S" and sep: "sum_list as `→ C0 ∈ f⊢𝒞" "sum_list (as@[s]) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs@[t]) `→ C0 ∈ f⊢𝒞" shows "sum_list (as@[s]@bs@[t]@cs) `→ C0 = sum_list (as@bs@cs) `→ C0" proof- define 𝗌 where "𝗌 = induced_automorph f g" from fg obtain C where "OpposedThinChamberComplexFoldings X f g C" using foldpairs_def by fast then have "id ` sum_list (as@[s]@bs@[t]@cs) `→ C0 = sum_list (as@bs@cs) `→ C0" using 𝗌_def fg S sep fold_end_sum_chain_gf[of f g "as@[s]@bs" t cs] fold_end_sum_chain_fg[of f g as s "bs@cs"] by (simp add: image_comp[THEN sym] OpposedThinChamberComplexFoldings.indaut_order2[ THEN sym] ) thus ?thesis by simp qed lemma S_list_not_min_gallery_deletion: fixes ss :: "'a permutation list" defines w : "w ≡ sum_list ss" assumes ss: "ss∈lists S" "ss≠[]" "¬ min_gallery (map (λw. w`→C0) (sums ss))" shows "∃a b as bs cs. ss = as@[a]@bs@[b]@cs ∧ w = sum_list (as@bs@cs)" proof- from w ss(1) have w_W: "w∈W" using sum_list_S_in_W by fast define Cs where "Cs = map (λw. w`→C0) (sums ss)" from ss obtain f g as s bs t cs where fg : "(f,g)∈foldpairs" and sep : "sum_list as `→ C0 ∈ f⊢𝒞" "sum_list (as@[s]) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs) `→ C0 ∈ g⊢𝒞" "sum_list (as@[s]@bs@[t]) `→ C0 ∈ f⊢𝒞" and decomp: "ss = as@[s]@bs@[t]@cs" using S_list_not_min_gallery_double_split[of ss] by blast from fg sep decomp w ss(1) have "w`→C0 = sum_list (as@bs@cs) `→ C0" using fold_middle_sum_chain by auto with ss(1) decomp have "w = sum_list (as@bs@cs)" using w_W sum_list_S_in_W[of "as@bs@cs"] by (auto intro: inj_onD fundchamber_W_image_inj_on) with decomp show ?thesis by fast qed lemma 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)" using nil_reduced_word_for_0[of S] not_reduced_word_not_min_gallery S_list_not_min_gallery_deletion by fastforce lemma PreCoxeterSystemWithDeletion: "PreCoxeterSystemWithDeletion S" using S_add_order2 deletion by unfold_locales simp lemma CoxeterSystem: "CoxeterSystem S" using PreCoxeterSystemWithDeletion PreCoxeterSystemWithDeletion.CoxeterSystem by fast end (* context ThinChamberComplexManyFoldings *) subsection ‹Coxeter complexes› subsubsection ‹Locale and complex definitions› text ‹ Now we add in the assumption that the generating set is finite, and construct the associated Coxeter complex from the poset of special cosets. › locale CoxeterComplex = CoxeterSystem S for S :: "'w::group_add set" + assumes finite_genset: "finite S" begin definition TheComplex :: "'w set set set" where "TheComplex ≡ ordering.PosetComplex (⊇) (⊃) 𝒫" abbreviation "Σ ≡ TheComplex" end (* context CoxeterComplex *) subsubsection ‹As a simplicial complex› text ‹ Here we record the fact that the Coxeter complex associated to a Coxeter system is a simplicial complex, and note that the poset of special cosets is complex-like. This last fact allows us to reason about the complex by reasoning about the poset, via the poset isomorphism @{const ComplexLikePoset.smap}. › context CoxeterComplex begin lemma simplex_like_special_cosets: assumes "X∈𝒫" shows "supset_simplex_like (𝒫.⊇X)" proof- have image_eq_UN: "⋀f A. f ` A = (⋃x∈A. {f x})" by blast from assms obtain w T where "w∈W" "T ∈ Pow S" "X = w +o ⟨T⟩" using special_cosets_def by auto thus ?thesis using image_eq_UN[where f= "(+o) w ∘ genby"] finite_genset simplex_like_pow_above_in OrderingSetIso.simplex_like_map[ OF special_coset_below_in_supset_ordering_iso, of T w ] special_cosets_below_in by force qed lemma SimplicialComplex_Σ: "SimplicialComplex Σ" unfolding TheComplex_def proof (rule ordering.poset_is_SimplicialComplex) show "ordering (⊇) (⊃)" .. show "∀X∈𝒫. supset_simplex_like (𝒫.⊇X)" using simplex_like_special_cosets by fast qed lemma ComplexLikePoset_special_cosets: "ComplexLikePoset (⊇) (⊃) 𝒫" using simplex_like_special_cosets special_cosets_has_bottom special_cosets_have_glbs by unfold_locales abbreviation "smap ≡ ordering.poset_simplex_map (⊇) (⊃) 𝒫" lemmas smap_def = ordering.poset_simplex_map_def[OF supset_poset, of 𝒫] lemma ordsetmap_smap: "⟦ X∈𝒫; Y∈𝒫; X⊇Y ⟧ ⟹ smap X ⊆ smap Y" using ComplexLikePoset.ordsetmap_smap[OF ComplexLikePoset_special_cosets] smap_def by simp lemma rev_ordsetmap_smap: "⟦ X∈𝒫; Y∈𝒫; smap X ⊆ smap Y ⟧ ⟹ X⊇Y" using ComplexLikePoset.rev_ordsetmap_smap[ OF ComplexLikePoset_special_cosets ] smap_def by simp lemma smap_onto_PosetComplex: "smap ` 𝒫 = Σ" using ComplexLikePoset.smap_onto_PosetComplex[ OF ComplexLikePoset_special_cosets ] smap_def TheComplex_def by simp lemmas simplices_conv_special_cosets = smap_onto_PosetComplex[THEN sym] lemma smap_into_PosetComplex: "X∈𝒫 ⟹ smap X ∈ Σ" using smap_onto_PosetComplex by fast lemma smap_pseudominimal: "w∈W ⟹ s∈S ⟹ smap (w +o ⟨S-{s}⟩) = {w +o ⟨S-{s}⟩}" using smap_def[of "w +o ⟨S-{s}⟩"] special_coset_pseudominimal_in_below_in[of w "S-{s}"] exclude_one_is_pseudominimal_in_below_in[of w "S-{s}"] by auto lemma exclude_one_notin_smap_singleton: "s∈S ⟹ w +o ⟨S-{s}⟩ ∉ smap (w +o ⟨{s}⟩)" using smap_def[of "w +o ⟨{s}⟩"] supset_pseudominimal_inD1[of "𝒫.⊇(w +o ⟨{s}⟩)" "w +o ⟨S-{s}⟩"] special_coset_subset_rev_mono[of "{s}" "S-{s}"] by auto lemma maxsimp_vertices: "w∈W ⟹ s∈S ⟹ w +o ⟨S-{s}⟩ ∈ smap {w}" using special_cosetsI[of "S-{s}"] special_coset_singleton ordsetmap_smap[of "w +o ⟨S-{s}⟩"] smap_pseudominimal by (simp add: genby_lcoset_refl) lemma maxsimp_singleton: assumes "w∈W" shows "SimplicialComplex.maxsimp Σ (smap {w})" proof (rule SimplicialComplex.maxsimpI, rule SimplicialComplex_Σ) from assms show "smap {w} ∈ Σ" using special_coset_singleton smap_into_PosetComplex by fast next fix z assume z: "z∈Σ" "smap {w} ⊆ z" from z(1) obtain X where X: "X∈𝒫" "z = smap X" using simplices_conv_special_cosets by auto with assms z(2) have "X = {w}" using special_coset_singleton rev_ordsetmap_smap special_coset_nempty by fast with X(2) show "z = smap {w}" by fast qed lemma maxsimp_is_singleton: assumes "SimplicialComplex.maxsimp Σ x" shows "∃w∈W. smap {w} = x" proof- from assms obtain X where X: "X∈𝒫" "smap X = x" using SimplicialComplex.maxsimpD_simplex[OF SimplicialComplex_Σ] simplices_conv_special_cosets by auto from X(1) obtain w T where wT: "w∈W" "T∈Pow S" "X = w +o ⟨T⟩" using special_cosets_def by auto from wT(1) have "{w}∈𝒫" using special_coset_singleton by fast moreover with X wT(3) have "x ⊆ smap {w}" using genby_lcoset_refl ordsetmap_smap by fast ultimately show ?thesis using assms wT(1) smap_into_PosetComplex SimplicialComplex.maxsimpD_maximal[OF SimplicialComplex_Σ] by fast qed lemma maxsimp_vertex_conv_special_coset: "w∈W ⟹ X ∈ smap {w} ⟹ ∃s∈S. X = w +o ⟨S-{s}⟩" using smap_def special_coset_pseudominimal_in_below_in[of w "{}"] by (simp add: genby_lcoset_empty) lemma vertices: "w∈W ⟹ s∈S ⟹ w +o ⟨S-{s}⟩ ∈ ⋃Σ" using maxsimp_singleton SimplicialComplex.maxsimpD_simplex[OF SimplicialComplex_Σ] maxsimp_vertices by fast lemma smap0_conv_special_subgroups: "smap 0 = (λs. ⟨S - {s}⟩) ` S" using genby_0_closed maxsimp_vertices maxsimp_vertex_conv_special_coset by force lemma S_bij_betw_chamber0: "bij_betw (λs. ⟨S-{s}⟩) S (smap 0)" unfolding bij_betw_def proof show "inj_on (λs. ⟨S-{s}⟩) S" proof (rule inj_onI) fix s t show "⟦ s∈S; t∈S; ⟨S-{s}⟩ = ⟨S-{t}⟩ ⟧ ⟹ s = t" using inj_onD[OF special_subgroup_inj, of "S-{s}" "S-{t}"] by fast qed qed (rule smap0_conv_special_subgroups[THEN sym]) lemma smap_singleton_conv_W_image: "w∈W ⟹ smap {w} = ((+o) w) ` (smap 0)" using genby_0_closed[of S] maxsimp_vertices[of 0] maxsimp_vertices[of w] maxsimp_vertex_conv_special_coset by force lemma W_lcoset_bij_betw_singletons: assumes "w∈W" shows "bij_betw ((+o) w) (smap 0) (smap {w})" unfolding bij_betw_def proof (rule conjI, rule inj_onI) fix X Y assume XY: "X ∈ smap 0" "Y ∈ smap 0" "w +o X = w +o Y" from XY(1,2) obtain sx sy where "X = ⟨S-{sx}⟩" "Y = ⟨S-{sy}⟩" using maxsimp_vertex_conv_special_coset[of 0 X] maxsimp_vertex_conv_special_coset[of 0 Y] genby_0_closed[of S] by auto with XY(3) show "X=Y" using inj_onD[OF special_coset_inj, of w "S-{sx}" "S-{sy}"] by force qed (rule smap_singleton_conv_W_image[THEN sym], rule assms) lemma facets: assumes "w∈W" "s∈S" shows "smap (w +o ⟨{s}⟩) ⊲ smap {w}" proof ( rule facetrelI, rule exclude_one_notin_smap_singleton, rule assms(2), rule order_antisym ) show "smap {w} ⊆ insert (w +o ⟨S - {s}⟩) (smap (w +o ⟨{s}⟩))" proof fix X assume "X ∈ smap {w}" with assms(1) obtain t where "t∈S" "X = w +o ⟨S-{t}⟩" using maxsimp_vertex_conv_special_coset by fast with assms show "X∈ insert (w +o ⟨S - {s}⟩) (smap (w +o ⟨{s}⟩))" using exclude_one_is_pseudominimal_in_below_in smap_def by (cases "t=s") auto qed from assms show "smap {w} ⊇ insert (w +o ⟨S - {s}⟩) (smap (w +o ⟨{s}⟩))" using genby_lcoset_refl special_cosetsI[of "{s}"] special_coset_singleton ordsetmap_smap maxsimp_vertices by fast qed lemma facets': "w∈W ⟹ s∈S ⟹ smap {w,w+s} ⊲ smap {w}" using facets by (simp add: genset_order2_add genby_lcoset_order2) lemma adjacent: "w∈W ⟹ s∈S ⟹ smap {w+s} ∼ smap {w}" using facets'[of w s] genby_genset_closed genby_add_closed[of w S] facets'[of "w+s" s] by ( auto intro: adjacentI simp add: genset_order2_add add.assoc insert_commute ) lemma singleton_adjacent_0: "s∈S ⟹ smap {s} ∼ smap 0" using genby_genset_closed genby_0_closed facets'[of 0] facets'[of s] by (fastforce intro: adjacentI simp add: genset_order2_add insert_commute) end (* context CoxeterComplex *) subsubsection ‹As a chamber complex› text ‹Now we verify that a Coxeter complex is a chamber complex.› context CoxeterComplex begin abbreviation "chamber ≡ SimplicialComplex.maxsimp Σ" abbreviation "gallery ≡ SimplicialComplex.maxsimpchain Σ" lemmas chamber_singleton = maxsimp_singleton lemmas chamber_vertex_conv_special_coset = maxsimp_vertex_conv_special_coset lemmas chamber_vertices = maxsimp_vertices lemmas chamber_is_singleton = maxsimp_is_singleton lemmas faces = SimplicialComplex.faces [OF SimplicialComplex_Σ] lemmas gallery_def = SimplicialComplex.maxsimpchain_def [OF SimplicialComplex_Σ] lemmas gallery_rev = SimplicialComplex.maxsimpchain_rev [OF SimplicialComplex_Σ] lemmas chamberD_simplex = SimplicialComplex.maxsimpD_simplex[OF SimplicialComplex_Σ] lemmas gallery_CConsI = SimplicialComplex.maxsimpchain_CConsI[OF SimplicialComplex_Σ] lemmas gallery_overlap_join = SimplicialComplex.maxsimpchain_overlap_join[OF SimplicialComplex_Σ] lemma word_gallery_to_0: "ss ≠ [] ⟹ ss∈ lists S ⟹ ∃xs. gallery (smap {sum_list ss} # xs @ [smap 0])" proof (induct ss rule: rev_nonempty_induct) case (single s) hence "gallery (smap {sum_list [s]} # [] @ [smap 0])" using genby_genset_closed genby_0_closed chamber_singleton singleton_adjacent_0 gallery_def by auto thus ?case by fast next case (snoc s ss) from snoc(2,3) obtain xs where "gallery (smap {sum_list ss} # xs @ [smap 0])" by auto moreover from snoc(3) have "chamber (smap {sum_list (ss@[s])})" using special_subgroup_eq_sum_list chamber_singleton by fast ultimately have "gallery (smap {sum_list (ss@[s])} # (smap {sum_list ss} # xs) @ [smap 0])" using snoc(3) special_subgroup_eq_sum_list adjacent[of "sum_list ss" s] by (auto intro: gallery_CConsI) thus ?case by fast qed lemma gallery_to_0: assumes "w∈W" "w≠0" shows "∃xs. gallery (smap {w} # xs @ [smap 0])" proof- from assms(1) obtain ss where ss: "ss∈lists S" "w = sum_list ss" using special_subgroup_eq_sum_list by auto with assms(2) show ?thesis using word_gallery_to_0[of ss] by fastforce qed lemma ChamberComplex_Σ: "ChamberComplex Σ" proof (intro_locales, rule SimplicialComplex_Σ, unfold_locales) fix y assume "y∈Σ" from this obtain X where X: "X∈𝒫" "y = smap X" using simplices_conv_special_cosets by auto from X(1) obtain w T where "w∈W" "X = w +o ⟨T⟩" using special_cosets_def by auto with X show "∃x. chamber x ∧ y ⊆ x" using genby_lcoset_refl special_coset_singleton ordsetmap_smap chamber_singleton by fastforce next fix x y assume xy: "x≠y" "chamber x" "chamber y" from xy(2,3) obtain w w' where ww': "w∈W" "x = smap {w}" "w'∈W" "y = smap {w'}" using chamber_is_singleton by blast show "∃zs. gallery (x # zs @ [y])" proof (cases "w=0" "w'=0" rule: two_cases) case both with xy(1) ww'(2,4) show ?thesis by fast next case one with ww'(2-4) show ?thesis using gallery_to_0 gallery_rev by fastforce next case other with ww'(1,2,4) show ?thesis using gallery_to_0 by auto next case neither from this ww' obtain xs ys where "gallery (x # xs @ [smap 0])" "gallery (smap 0 # ys @ [y])" using gallery_to_0 gallery_rev by force hence "gallery (x # (xs @ smap 0 # ys) @ [y])" using gallery_overlap_join[of "x#xs"] by simp thus ?thesis by fast qed qed lemma card_chamber: "chamber x ⟹ card x = card S" using bij_betw_same_card[OF S_bij_betw_chamber0] chamber_singleton genby_0_closed[of S] ChamberComplex.chamber_card[OF ChamberComplex_Σ, of "smap 0"] by simp lemma vertex_conv_special_coset: "X∈⋃Σ ⟹ ∃w s. w∈W ∧ s∈S ∧ X = w +o ⟨S-{s}⟩" using ChamberComplex.simplex_in_max[OF ChamberComplex_Σ] chamber_is_singleton chamber_vertex_conv_special_coset by fast end (* context CoxeterComplex *) subsubsection ‹The Coxeter complex associated to a thin chamber complex with many foldings› text ‹ Having previously verified that the fundamental automorphisms in a thin chamber complex with many foldings form a Coxeter system, we now record the existence of a chamber complex isomorphism onto the associated Coxeter complex. › context ThinChamberComplexManyFoldings begin lemma CoxeterComplex: "CoxeterComplex S" by ( rule CoxeterComplex.intro, rule CoxeterSystem, unfold_locales, rule finite_S ) abbreviation "Σ ≡ CoxeterComplex.TheComplex S" lemma S_list_not_min_gallery_not_reduced: assumes "ss≠[]" "¬ min_gallery (map (λw. w`→C0) (sums ss))" shows "¬ reduced_word S ss" proof (cases "ss∈lists S") case True obtain a b as bs cs where "ss = as@[a]@bs@[b]@cs" "sum_list ss = sum_list (as@bs@cs)" using S_list_not_min_gallery_deletion [OF True assms] by blast with True show ?thesis using not_reduced_word_for[of "as@bs@cs"] by auto next case False thus ?thesis using reduced_word_for_lists by fast qed lemma reduced_S_list_min_gallery: "ss≠[] ⟹ reduced_word S ss ⟹ min_gallery (map (λw. w`→C0) (sums ss))" using S_list_not_min_gallery_not_reduced by fast lemma fundchamber_vertex_stabilizer1: fixes t defines v: "v ≡ fundantivertex t" assumes tw: "t∈S" "w∈W" "w→v = v" shows "w ∈ ⟨S-{t}⟩" proof- from v tw(1) have v_C0: "v∈C0" using fundantivertex by simp define ss where "ss = arg_min length (word_for S w)" moreover have "reduced_word S ss ⟹ sum_list ss → v = v ⟹ sum_list ss ∈ ⟨S-{t}⟩" proof (induct ss) case (Cons s ss) from Cons(2) have s_S: "s∈S" using reduced_word_for_lists by fastforce from this obtain f g where fg: "(f,g)∈fundfoldpairs" "s = Abs_induced_automorph f g" by auto from fg(1) have opp_fg: "OpposedThinChamberComplexFoldings X f g C0" using fundfoldpairs_def by auto define Cs where "Cs = map (λw. w`→C0) (sums (s#ss))" with Cons(2) have minCs: "min_gallery Cs" using reduced_S_list_min_gallery by fast have sv: "s→v = v" proof (cases ss rule: rev_cases) case Nil with Cons(3) show ?thesis by simp next case (snoc ts t) define Ms Cn where "Ms = map (λw. w`→C0) (map ((+) s) (sums ts))" and "Cn = sum_list (s#ss) `→ C0" with snoc Cs_def have "Cs = C0 # Ms @ [Cn]" by (simp add: sums_snoc zero_permutation.rep_eq) with minCs Cs_def fg have "C0∈f⊢𝒞" "Cn∈g⊢𝒞" using sums_Cons_conv_append_tl[THEN sym, of s ss] wall_crossings_subset_walls_betw[of C0 Ms Cn] fundfoldpairs_def the_wall_betw_adj_fundchamber walls_betw_def OpposedThinChamberComplexFoldings.basech_halfchsys(1)[ OF opp_fg ] OpposedThinChamberComplexFoldings.separated_by_this_wall_fg[ OF opp_fg, of C0 Cn ] by (auto simp add: zero_permutation.rep_eq) moreover from Cons(3) Cn_def have "v∈Cn" using v_C0 by force ultimately show "s→v = v" using v_C0 fg OpposedThinChamberComplexFoldings.indaut_wallvertex[ OF opp_fg ] by (simp add: permutation_conv_induced_automorph) qed moreover from Cons(3) have "0 → sum_list ss → v = s→v" using s_S by (simp add: plus_permutation.rep_eq S_order2_add[THEN sym]) ultimately have "sum_list ss → v = v" by (simp add: zero_permutation.rep_eq) with Cons(1,2) have "sum_list ss ∈ ⟨S-{t}⟩" using reduced_word_Cons_reduce by auto moreover from tw(1) v have "s∈⟨S-{t}⟩" using sv s_S genby_genset_closed[of s "S-{t}"] fundantivertex_unstable by fastforce ultimately show ?case using genby_add_closed by simp qed (simp add: genby_0_closed) ultimately show ?thesis using tw(2,3) reduced_word_for_genby_sym_arg_min[OF S_sym] reduced_word_for_sum_list by fastforce qed lemma fundchamber_vertex_stabilizer2: assumes s: "s∈S" defines v: "v ≡ fundantivertex s" shows "w ∈ ⟨S-{s}⟩ ⟹ w→v = v" proof (erule genby.induct) show "0→v = v" by (simp add: zero_permutation.rep_eq) next fix t assume "t∈S-{s}" moreover with s v have "v∈C0∩t`→C0" using inj_on_eq_iff[OF fundantivertex_inj_on] fundchamber_S_adjacent fundchamber_S_image_neq_fundchamber[THEN not_sym] not_the1[OF adj_antivertex, of C0 "t`→C0" v] fundantivertex unfolding fundantivertex_def by auto ultimately show "t→v = v" using S_fixespointwise_fundchamber_image_int fixespointwiseD by fastforce next fix w w' assume ww': "w→v = v" "w'→v = v" from ww'(2) have "(-w')→v = id v" using plus_permutation.rep_eq[of "-w'" w'] by (auto simp add: zero_permutation.rep_eq[THEN sym]) with ww'(1) show "(w-w')→v = v" using plus_permutation.rep_eq[of w "-w'"] by simp qed lemma label_wrt_special_coset1: assumes "label_wrt C0 φ" "fixespointwise φ C0" "w0∈W" "s∈S" defines "v ≡ fundantivertex s" shows "{w∈W. w → φ (w0→v) = w0→v} = w0 +o ⟨S-{s}⟩" proof- from assms(4,5) have v_C0: "v∈C0" using fundantivertex[of s] by simp show ?thesis proof (rule seteqI) fix w assume "w∈{w∈W. w→(φ (w0→v)) = w0→v}" hence w: "w∈W" "w→(φ (w0→v)) = w0→v" by auto from assms(2,3) have "(-w0 + w) → v = 0→v" using w(2) v_C0 fundchamber chamberD_simplex W_respects_labels[OF assms(1)] plus_permutation.rep_eq[of "-w0" w0] by (fastforce simp add: plus_permutation.rep_eq fixespointwiseD) with assms(3-5) show "w ∈ w0 +o ⟨S-{s}⟩" using w(1) genby_uminus_add_closed[of w0 S w] fundchamber_vertex_stabilizer1 by (force simp add: zero_permutation.rep_eq elt_set_plus_def) next fix w assume w: "w ∈ w0 +o ⟨S-{s}⟩" from this obtain w1 where w1: "w1 ∈ ⟨S-{s}⟩" "w = w0 + w1" using elt_set_plus_def by blast moreover with w assms(3) have w_W: "w∈W" using genby_mono[of "S-{s}" S] genby_add_closed by fastforce ultimately show "w∈{w∈W. w→(φ (w0→v)) = w0→v}" using assms(2-5) v_C0 fundchamber chamberD_simplex W_respects_labels[OF assms(1), of w0 v] fundchamber_vertex_stabilizer2[of s w1] by (fastforce simp add: fixespointwiseD plus_permutation.rep_eq) qed qed lemma label_wrt_special_coset1': assumes "label_wrt C0 φ" "fixespointwise φ C0" "w0∈W" "v∈C0" defines "s ≡ fundantipermutation v" shows "{w∈W. w → φ (w0→v) = w0→v} = w0 +o ⟨S-{s}⟩" using assms fundantipermutation1 fundantivertex_bij_betw bij_betw_f_the_inv_into_f label_wrt_special_coset1[of φ w0 s] by fastforce lemma label_wrt_special_coset2': assumes "label_wrt C0 φ" "fixespointwise φ C0" "w0∈W" "v ∈ w0`→C0" defines "s ≡ fundantipermutation (φ v)" shows "{w∈W. w → φ v = v} = w0 +o ⟨S-{s}⟩" using assms fundchamber chamberD_simplex W_respects_labels label_wrt_special_coset1'[OF assms(1-3)] by (fastforce simp add: fixespointwiseD) (* slow *) lemma label_stab_map_W_fundchamber_image: assumes "label_wrt C0 φ" "fixespointwise φ C0" "w0∈W" defines "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "ψ`(w0`→C0) = CoxeterComplex.smap S {w0}" proof (rule seteqI) from assms show "⋀x. x ∈ CoxeterComplex.smap S {w0} ⟹ x ∈ ψ`(w0`→C0)" using CoxeterComplex.chamber_vertex_conv_special_coset[ OF CoxeterComplex, of w0 ] label_wrt_special_coset1 fundantivertex by fastforce next fix x assume "x∈ ψ`(w0`→C0)" from this obtain v where v: "v∈w0`→C0" "x = ψ v" by fast with assms have "x = w0 +o ⟨S-{fundantipermutation (φ v)}⟩" using label_wrt_special_coset2' by fast moreover from v(1) assms(3) have "v∈⋃X" using fundchamber chamberD_simplex W_endomorphism ChamberComplexEndomorphism.vertex_map by fastforce ultimately show "x ∈ CoxeterComplex.smap S {w0}" using assms(1,3) label_wrt_elt_image fundantipermutation1 CoxeterComplex.chamber_vertices[OF CoxeterComplex] by fastforce qed lemma label_stab_map_chamber_map: assumes φ: "label_wrt C0 φ" "fixespointwise φ C0" and C: "chamber C" defines ψ: "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "CoxeterComplex.chamber S (ψ`C)" proof- from C obtain w where w: "w∈W" "C = w`→C0" using chamber_eq_W_image by fast with φ ψ have "ψ`C = CoxeterComplex.smap S {w}" using label_stab_map_W_fundchamber_image by simp with w(1) show ?thesis using CoxeterComplex.chamber_singleton[OF CoxeterComplex] by simp qed lemma label_stab_map_inj_on_vertices: assumes φ: "label_wrt C0 φ" "fixespointwise φ C0" defines ψ: "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "inj_on ψ (⋃X)" proof (rule inj_onI) fix v1 v2 assume v: "v1∈⋃X" "v2∈⋃X" "ψ v1 = ψ v2" from v(1,2) have φv: "φ v1 ∈ C0" "φ v2 ∈ C0" using label_wrt_elt_image[OF φ(1)] by auto define s1 s2 where "s1 = fundantipermutation (φ v1)" and "s2 = fundantipermutation (φ v2)" from v(1,2) obtain w1 w2 where "w1∈W" "v1∈w1`→C0" "w2∈W" "v2∈w2`→C0" using simplex_in_max chamber_eq_W_image by blast with assms s1_def s2_def have ψv: "ψ v1 = w1 +o ⟨S-{s1}⟩" "ψ v2 = w2 +o ⟨S-{s2}⟩" using label_wrt_special_coset2' by auto with v(3) have "w1 +o ⟨S-{s1}⟩ = w2 +o ⟨S-{s2}⟩" using label_wrt_special_coset2' by auto with s1_def s2_def have "φ v1 = φ v2" using PreCoxeterSystemWithDeletion.special_coset_eq_imp_eq_gensets[ OF PreCoxeterSystemWithDeletion, of "S-{s1}" "S-{s2}" w1 w2 ] φv fundantipermutation1[of "φ v1"] fundantipermutation1[of "φ v2"] bij_betw_f_the_inv_into_f[OF fundantivertex_bij_betw, of "φ v1"] bij_betw_f_the_inv_into_f[OF fundantivertex_bij_betw, of "φ v2"] by fastforce with v(3) ψ show "v1=v2" using ψv(1) genby_0_closed[of "S-{s1}"] lcoset_refl[of "⟨S-{s1}⟩" w1] by fastforce qed lemma label_stab_map_surj_on_vertices: assumes "label_wrt C0 φ" "fixespointwise φ C0" defines "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "ψ`(⋃X) = ⋃Σ" proof (rule seteqI) fix u assume "u ∈ ψ`(⋃X)" from this obtain v where v: "v∈⋃X" "u = ψ v" by fast from v(1) obtain w where "w∈W" "v∈w`→C0" using simplex_in_max chamber_eq_W_image by blast with assms v show "u∈⋃Σ" using label_wrt_special_coset2' label_wrt_elt_image[OF assms(1)] fundantipermutation1 CoxeterComplex.vertices[OF CoxeterComplex] by auto next fix u assume "u∈⋃Σ" from this obtain w s where "w∈W" "s∈S" "u = w +o ⟨S-{s}⟩" using CoxeterComplex.vertex_conv_special_coset[OF CoxeterComplex] by blast with assms show "u ∈ ψ`(⋃X)" using label_wrt_special_coset1 fundantivertex fundchamber chamberD_simplex W_endomorphism ChamberComplexEndomorphism.vertex_map by fast qed lemma label_stab_map_bij_betw_vertices: assumes "label_wrt C0 φ" "fixespointwise φ C0" defines "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "bij_betw ψ (⋃X) (⋃Σ)" unfolding bij_betw_def using assms label_stab_map_inj_on_vertices label_stab_map_surj_on_vertices by auto lemma label_stab_map_bij_betw_W_chambers: assumes "label_wrt C0 φ" "fixespointwise φ C0" "w0∈W" defines "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "bij_betw ψ (w0`→C0) (CoxeterComplex.smap S {w0})" unfolding bij_betw_def proof (rule conjI, rule inj_on_inverseI) define f1 f2 where "f1 = the_inv_into (CoxeterComplex.smap S 0) ((+o) w0)" and "f2 = the_inv_into S (λs. ⟨S-{s}⟩)" define g where "g = ((→) w0) ∘ fundantivertex ∘ f2 ∘ f1" from assms(3) have inj_opw0: "inj_on ((+o) w0) (CoxeterComplex.smap S 0)" using bij_betw_imp_inj_on[OF CoxeterComplex.W_lcoset_bij_betw_singletons] CoxeterComplex by fast have inj_genby_minus_s: "inj_on (λs. ⟨S-{s}⟩) S" using bij_betw_imp_inj_on[OF CoxeterComplex.S_bij_betw_chamber0] CoxeterComplex by fast fix v assume v: "v∈w0`→C0" from this obtain v0 where v0: "v0∈C0" "v = w0→v0" by fast from v0(1) have fap_v0: "fundantipermutation v0 ∈ S" using fundantipermutation1 by auto with assms(3) have v0': "⟨S-{fundantipermutation v0}⟩ ∈ CoxeterComplex.smap S 0" using genby_0_closed[of S] CoxeterComplex.chamber_vertices[OF CoxeterComplex, of 0] by simp from v0 assms have "ψ v = w0 +o ⟨S-{fundantipermutation v0}⟩" using label_wrt_special_coset1' by simp with f1_def assms(3) f2_def v0 g_def show "g (ψ v) = v" using v0' fap_v0 the_inv_into_f_f[OF inj_opw0] the_inv_into_f_f[OF inj_genby_minus_s] bij_betw_f_the_inv_into_f[OF fundantivertex_bij_betw] by simp next from assms show "ψ`(w0`→C0) = CoxeterComplex.smap S {w0}" using label_stab_map_W_fundchamber_image by simp qed lemma label_stab_map_surj_on_simplices: assumes φ: "label_wrt C0 φ" "fixespointwise φ C0" defines ψ: "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "ψ ⊢ X = Σ" proof (rule seteqI) fix y assume "y ∈ ψ ⊢ X" from this obtain x where x: "x∈X" "y = ψ ` x" by fast from x(1) obtain C where "chamber C" "x⊆C" using simplex_in_max by fast with assms x(2) show "y ∈ Σ" using label_stab_map_chamber_map CoxeterComplex.chamberD_simplex[OF CoxeterComplex] CoxeterComplex.faces[OF CoxeterComplex, of "ψ`C" y] by auto next fix y assume "y ∈ Σ" from this obtain z where z: "CoxeterComplex.chamber S z" "y⊆z" using ChamberComplex.simplex_in_max[ OF CoxeterComplex.ChamberComplex_Σ, OF CoxeterComplex ] by fast from z(1) obtain w where w: "w∈W" "z = CoxeterComplex.smap S {w}" using CoxeterComplex.chamber_is_singleton[OF CoxeterComplex] by fast with assms have "bij_betw ψ (w`→C0) z" using label_stab_map_bij_betw_W_chambers by fast hence 1: "bij_betw ((`) ψ) (Pow (w`→C0)) (Pow z)" using bij_betw_imp_bij_betw_Pow by fast define x where x: "x ≡ the_inv_into (Pow (w`→C0)) ((`) ψ) y" with z(2) have "x ⊆ w`→C0" using bij_betw_the_inv_into_onto[OF 1] by auto with w(1) have "x∈X" using faces fundchamber_W_image_chamber chamberD_simplex by fastforce moreover from x z(2) have "y = ψ ` x" using bij_betw_f_the_inv_into_f[OF 1] by simp ultimately show "y ∈ ψ ⊢ X" by fast qed lemma label_stab_map_iso_to_coxeter_complex: assumes "label_wrt C0 φ" "fixespointwise φ C0" defines "ψ ≡ λv. {w∈W. w→(φ v) = v}" shows "ChamberComplexIsomorphism X Σ ψ" proof ( rule ChamberComplexIsomorphism.intro, rule ChamberComplexMorphism.intro ) show "ChamberComplex X" .. show "ChamberComplex Σ" using CoxeterComplex CoxeterComplex.ChamberComplex_Σ by fast from assms show "ChamberComplexMorphism_axioms X Σ ψ" using label_stab_map_chamber_map CoxeterComplex.card_chamber[OF CoxeterComplex] card_S_chamber by unfold_locales auto from assms show "ChamberComplexIsomorphism_axioms X Σ ψ" using label_stab_map_bij_betw_vertices label_stab_map_surj_on_simplices by unfold_locales auto qed lemma ex_iso_to_coxeter_complex': "∃ψ. ChamberComplexIsomorphism X (CoxeterComplex.TheComplex S) ψ" using CoxeterComplex ex_label_retraction label_stab_map_iso_to_coxeter_complex by force lemma ex_iso_to_coxeter_complex: "∃S::'a permutation set. CoxeterComplex S ∧ (∃ψ. ChamberComplexIsomorphism X (CoxeterComplex.TheComplex S) ψ)" using CoxeterComplex ex_iso_to_coxeter_complex' by fast end (* context ThinChamberComplexManyFoldings *) end (* theory *)