theorem CoxeterSystemFromDeletion.orderOf_mul_comm_of_involution {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (s t : B) : orderOf (gen s * gen t) = orderOf (gen t * gen s)

For involutions $\mathtt{gen}\,s$ and $\mathtt{gen}\,t$, the products $(\mathtt{gen}\,s)(\mathtt{gen}\,t)$ and $(\mathtt{gen}\,t)(\mathtt{gen}\,s)$ have the same order, since they are conjugate via $\mathtt{gen}\,s$.

noncomputable def CoxeterSystemFromDeletion.deletionCoxeterMatrix {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) : CoxeterMatrix B

The Coxeter matrix canonically associated to a family of involutions $\mathtt{gen} : B \to W$ with no nontrivial relations $\mathtt{gen}\,s \cdot \mathtt{gen}\,t = 1$ for $s \ne t$: the $(s,t)$-entry is the order of $\mathtt{gen}\,s \cdot \mathtt{gen}\,t$ in $W$.

theorem CoxeterSystemFromDeletion.deletionCoxeterMatrix_isLiftable {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) : (deletionCoxeterMatrix gen hgen_inv hgen_ne).IsLiftable gen

The family $\mathtt{gen}$ satisfies the lifting hypothesis for the canonically associated Coxeter matrix: each pairwise relation $(\mathtt{gen}\,s \cdot \mathtt{gen}\,t)^{m(s,t)} = 1$ holds tautologically by the definition of order.

noncomputable def CoxeterSystemFromDeletion.deletionCanonicalHom {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) : (deletionCoxeterMatrix gen hgen_inv hgen_ne).Group →* W

The canonical group homomorphism from the abstract Coxeter group on $B$ (with the matrix induced by the family $\mathtt{gen}$) to $W$, sending each generator $\mathtt{simple}\,s$ to $\mathtt{gen}\,s$.

theorem CoxeterSystemFromDeletion.deletionCanonicalHom_apply_simple {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) (s : B) : (deletionCanonicalHom gen hgen_inv hgen_ne) ((deletionCoxeterMatrix gen hgen_inv hgen_ne).simple s) = gen s

The canonical homomorphism sends the abstract simple generator $\mathtt{simple}\,s$ to the concrete involution $\mathtt{gen}\,s$.

theorem CoxeterSystemFromDeletion.deletionCanonicalHom_surjective {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) = ⊤) : Function.Surjective ⇑(deletionCanonicalHom gen hgen_inv hgen_ne)

If the image of $\mathtt{gen}$ generates $W$, then the canonical homomorphism from the abstract Coxeter group to $W$ is surjective.

def CoxeterSystemFromDeletion.SatisfiesDeletionConditionGen {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) : Prop

The deletion condition for a family of generators $\mathtt{gen} : B \to W$: whenever a word $\omega$ in $B$ can be shortened (its $\mathtt{gen}$-product equals that of a strictly shorter word), there exist two indices $i < j$ in $\omega$ whose deletion preserves the product.