theorem CoxeterSystemFromDeletion.gen_injective_of_involution_ne {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hgen_ne : ∀ (s t : B), s ≠ t → gen s * gen t ≠ 1) : Function.Injective gen

A family of involutions $\mathtt{gen}$ with $\mathtt{gen}\,s \cdot \mathtt{gen}\,t \ne 1$ for $s \ne t$ is necessarily injective.

theorem CoxeterSystemFromDeletion.cycling_rotation_gives_lucky_or_Ltype {B : Type u_3} {W : Type u_4} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hgen_ne : ∀ (s t : B), s ≠ t → gen s * gen t ≠ 1) (hDel : SatisfiesDeletionConditionGen gen) (word : List B) (hw : (List.map gen word).prod = 1) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 2) : have M := deletionCoxeterMatrix gen hgen_inv hgen_ne; (∃ (word' : List B), word'.length < word.length ∧ (List.map gen word).prod = (List.map gen word').prod ∧ (List.map M.simple word).prod = (List.map M.simple word').prod) ∨ ∀ (k : ℕ), consecProd (wordCyclicGen gen word (2 * m) hlen ⋯) k m = wordCyclicGen gen word (2 * m) hlen ⋯ (k + 2) * wordCyclicGen gen word (2 * m) hlen ⋯ (k + 1) * consecProd (wordCyclicGen gen word (2 * m) hlen ⋯) (k + 2) (m - 2)

Cyclic rotation dichotomy: for a length-$2m$ word with trivial product ($m \ge 2$), either there is a strictly shorter word with the same product in both $W$ and the abstract Coxeter group (the "lucky" case), or the cyclic generators satisfy the $L$-type identity governing alternation.

theorem CoxeterSystemFromDeletion.cycling_dichotomy {B : Type u_3} {W : Type u_4} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hgen_ne : ∀ (s t : B), s ≠ t → gen s * gen t ≠ 1) (hDel : SatisfiesDeletionConditionGen gen) (word : List B) (hw : (List.map gen word).prod = 1) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 2) : have M := deletionCoxeterMatrix gen hgen_inv hgen_ne; (∃ (word' : List B), word'.length < word.length ∧ (List.map gen word).prod = (List.map gen word').prod ∧ (List.map M.simple word).prod = (List.map M.simple word').prod) ∨ ∀ (k : ℕ) (hk : k + 2 < word.length), word.get ⟨k, ⋯⟩ = word.get ⟨k + 2, hk⟩

Cleaner version of the cyclic dichotomy: either we can shorten the word in the relevant senses, or the word is two-step periodic, i.e. of alternating form $s t s t \cdots$.

theorem CoxeterSystemFromDeletion.alternating_word_prod_eq_pow {B : Type u_1} {G : Type u_3} [Group G] (f : B → G) (s t : B) (m : ℕ) (word : List B) (x✝ : word.length = 2 * m) (x✝¹ : m ≥ 1) : (∀ (k : ℕ) (hk : k + 2 < word.length), word.get ⟨k, ⋯⟩ = word.get ⟨k + 2, hk⟩) → word.get ⟨0, ⋯⟩ = s → word.get ⟨1, ⋯⟩ = t → (List.map f word).prod = (f s * f t) ^ m

If a word of length $2m$ is two-step periodic with first two letters $s, t$, then its image-product under any $f : B \to G$ equals $(f(s) \cdot f(t))^m$.

theorem CoxeterSystemFromDeletion.alternating_word_trivial_in_coxeter {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hgen_ne : ∀ (s t : B), s ≠ t → gen s * gen t ≠ 1) (word : List B) (hw : (List.map gen word).prod = 1) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 1) (halt : ∀ (k : ℕ) (hk : k + 2 < word.length), word.get ⟨k, ⋯⟩ = word.get ⟨k + 2, hk⟩) : have M := deletionCoxeterMatrix gen hgen_inv hgen_ne; (List.map M.simple word).prod = 1

An alternating word with trivial product under $\mathtt{gen}$ also has trivial product under the canonical simple-generator map of the deletion Coxeter matrix.

theorem CoxeterSystemFromDeletion.word_relation_trivial_in_coxeter_group {B : Type u_3} {W : Type u_4} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hgen_ne : ∀ (s t : B), s ≠ t → gen s * gen t ≠ 1) (hDel : SatisfiesDeletionConditionGen gen) : have M := deletionCoxeterMatrix gen hgen_inv hgen_ne; ∀ (word : List B), (List.map gen word).prod = 1 → (List.map M.simple word).prod = 1

Key theorem: every word relation in $W$ already holds in the abstract Coxeter group generated by $B$ with the deletion Coxeter matrix. This is what allows the canonical homomorphism to be injective.