theorem CoxeterSystemFromDeletion.deletionCanonicalHom_map_word_prod {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) : let M := deletionCoxeterMatrix gen hgen_inv hgen_ne; have φ := deletionCanonicalHom gen hgen_inv hgen_ne; φ (List.map M.simple word).prod = (List.map gen word).prod

Compatibility of the canonical homomorphism with word products: $\varphi$ sends the abstract product of a word in simple generators to the concrete product of the same word under $\mathtt{gen}$.

theorem CoxeterSystemFromDeletion.deletionCanonicalHom_injective {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) (hgen_surj : Subgroup.closure (Set.range gen) = ⊤) (hDel : SatisfiesDeletionConditionGen gen) : Function.Injective ⇑(deletionCanonicalHom gen hgen_inv hgen_ne)

Injectivity of the canonical homomorphism: if the family $\mathtt{gen}$ satisfies the deletion condition, generates $W$, and consists of involutions with no length-2 collapses, then the abstract Coxeter group surjects isomorphically onto $W$.

noncomputable def CoxeterSystemFromDeletion.deletion_implies_coxeter_system {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) (hgen_surj : Subgroup.closure (Set.range gen) = ⊤) (hDel : SatisfiesDeletionConditionGen gen) : CoxeterSystem (deletionCoxeterMatrix gen hgen_inv hgen_ne) W

Main theorem: a pair $(W, \mathtt{gen})$ satisfying the deletion condition, together with generators that are involutions with no length-$2$ relations, forms a Coxeter system for the canonically associated Coxeter matrix.