theorem swap_mul_swap_cube {α : Type u_1} [DecidableEq α] {a b c : α} (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : (Equiv.swap a b * Equiv.swap b c) ^ 3 = 1

Braid relation: $(\operatorname{swap}(a,b) \cdot \operatorname{swap}(b,c))^3 = 1$ for distinct $a,b,c$.

theorem swap_mul_swap_cube' {α : Type u_1} [DecidableEq α] {a b c : α} (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : (Equiv.swap b c * Equiv.swap a b) ^ 3 = 1

Reversed braid relation: $(\operatorname{swap}(b,c) \cdot \operatorname{swap}(a,b))^3 = 1$.

theorem adjTransp_isLiftable (n : ℕ) : (CoxeterMatrix.A n).IsLiftable fun (i : Fin n) => Equiv.swap i.castSucc i.succ

The assignment $i \mapsto \operatorname{swap}(\operatorname{castSucc} i, \operatorname{succ} i)$ satisfies the type-$A$ Coxeter relations.

theorem typeA_relations_satisfied (n : ℕ) (r : FreeGroup (Fin n)) : r ∈ (CoxeterMatrix.A n).relationsSet → (FreeGroup.lift fun (i : Fin n) => Equiv.swap i.castSucc i.succ) r = 1

The type-$A$ Coxeter relations evaluate to $1$ under the assignment to adjacent transpositions.

theorem typeA_coxeterGroup_mk_le (n : ℕ) : Cardinal.mk (CoxeterMatrix.A n).Group ≤ ↑(n + 1).factorial

Upper bound on the cardinality of the type-$A_{n-1}$ Coxeter group: $|W(A_{n-1})| \le (n+1)!$.

theorem typeA_coxeterGroup_finite (n : ℕ) : Finite (CoxeterMatrix.A n).Group

The type-$A_{n-1}$ Coxeter group is finite.

theorem typeA_coxeterGroup_card_le (n : ℕ) : Nat.card (CoxeterMatrix.A n).Group ≤ (n + 1).factorial

$|W(A_{n-1})| \le (n+1)!$ as a natural number bound.

theorem typeA_toPermHom_surjective (n : ℕ) (h : ∀ r ∈ (CoxeterMatrix.A n).relationsSet, (FreeGroup.lift fun (i : Fin n) => Equiv.swap i.castSucc i.succ) r = 1) : Function.Surjective ⇑(PresentedGroup.toGroup h)

The presented-group hom $W(A_{n-1}) \to S_{n+1}$ via adjacent transpositions is surjective.

theorem typeA_coxeterGroup_card_eq_factorial (n : ℕ) : Nat.card (CoxeterMatrix.A n).Group = (n + 1).factorial

Exact cardinality: $|W(A_{n-1})| = (n+1)!$, matching $|S_{n+1}|$.

theorem typeA_coxeterGroup_toPermHom_injective (n : ℕ) (h : ∀ r ∈ (CoxeterMatrix.A n).relationsSet, (FreeGroup.lift fun (i : Fin n) => Equiv.swap i.castSucc i.succ) r = 1) : Function.Injective ⇑(PresentedGroup.toGroup h)

Injectivity of the presented-group hom $W(A_{n-1}) \to S_{n+1}$, deduced from matching cardinalities.

noncomputable def typeA_mulEquiv (n : ℕ) : (CoxeterMatrix.A n).Group ≃* Equiv.Perm (Fin (n + 1))

Group isomorphism $W(A_{n-1}) \cong S_{n+1}$.

noncomputable def typeA_symGroup_mulEquiv (n : ℕ) : Equiv.Perm (Fin (n + 1)) ≃* (CoxeterMatrix.A n).Group

Reverse isomorphism $S_{n+1} \cong W(A_{n-1})$.

theorem typeA_symGroup_mulEquiv_apply (n : ℕ) (i : Fin n) : (typeA_symGroup_mulEquiv n).symm (PresentedGroup.of i) = Equiv.swap i.castSucc i.succ

Under the symmetric-group/Coxeter-group isomorphism, the $i$-th Coxeter generator corresponds to the adjacent transposition swapping $i$ and $i+1$.

theorem typeA_card_eq (n : ℕ) : Nat.card (CoxeterMatrix.A n).Group = (n + 1).factorial

Short alias for the cardinality formula $|W(A_{n-1})| = (n+1)!$.