def SymGroupCoxeter.adjTransp (n : ℕ) (i : Fin n) : Equiv.Perm (Fin (n + 1))

The simple transposition $\alpha_i = (i, i+1) \in S_{n+1}$ realizing the $i$-th generator of type $A_{n-1}$ (Section 9.6).

theorem SymGroupCoxeter.swap_mul_swap_cube_eq_one {α : 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

The braid relation $(\alpha\beta)^3 = 1$ for two swaps sharing a common element.

theorem SymGroupCoxeter.swap_mul_swap_cube_eq_one' {α : 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 version of swap_mul_swap_cube_eq_one: $(\beta\alpha)^3 = 1$.

theorem SymGroupCoxeter.adjTransp_isLiftable (n : ℕ) : (CoxeterMatrix.A n).IsLiftable (adjTransp n)

Adjacent transpositions satisfy the type-$A$ Coxeter relations: $(\alpha_i \alpha_j)^{m_{ij}} = 1$, including the braid relation $(\alpha_j \alpha_{j+1})^3 = 1$.

theorem SymGroupCoxeter.adjTransp_generates (n : ℕ) : Submonoid.closure (Set.range (adjTransp n)) = ⊤

Adjacent transpositions generate the entire symmetric group $S_{n+1}$ as a submonoid.

theorem SymGroupCoxeter.adjTransp_relations_satisfied (n : ℕ) (r : FreeGroup (Fin n)) (hr : r ∈ (CoxeterMatrix.A n).relationsSet) : (FreeGroup.lift (adjTransp n)) r = 1

Every type-$A$ Coxeter relation evaluates to $1$ under the assignment to adjacent transpositions.

noncomputable def SymGroupCoxeter.toPermHom (n : ℕ) : (CoxeterMatrix.A n).Group →* Equiv.Perm (Fin (n + 1))

The canonical homomorphism from the abstract type-$A$ Coxeter group to $S_{n+1}$ sending each Coxeter generator to the corresponding adjacent transposition.

@[simp]

theorem SymGroupCoxeter.toPermHom_simple (n : ℕ) (i : Fin n) : (toPermHom n) ((CoxeterMatrix.A n).simple i) = adjTransp n i

toPermHom sends the $i$-th simple Coxeter generator to the $i$-th adjacent transposition.

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

Group isomorphism $S_{n+1} \cong W(A_{n-1})$, the type-$A_{n-1}$ Coxeter group.

noncomputable def SymGroupCoxeter.symGroup_coxeterSystem (n : ℕ) : CoxeterSystem (CoxeterMatrix.A n) (Equiv.Perm (Fin (n + 1)))

The canonical type-$A$ Coxeter system structure on $S_{n+1}$.

theorem SymGroupCoxeter.symGroup_coxeterSystem_simple (n : ℕ) (i : Fin n) : (symGroup_coxeterSystem n).simple i = adjTransp n i

Under the canonical Coxeter system, the $i$-th simple generator is the $i$-th adjacent transposition.

theorem SymGroupCoxeter.symGroup_isCoxeterGroup (n : ℕ) : IsCoxeterGroup (Equiv.Perm (Fin (n + 1)))

The symmetric group $S_{n+1}$ is a Coxeter group, witnessed by the type-$A_{n-1}$ structure.