def SymmetricCoxeter.adjTransposition (n : ℕ) (i : Fin n) : Equiv.Perm (Fin (n + 1))

The adjacent transposition $\alpha_i = (i, i+1) \in S_{n+1}$.

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

Two swaps sharing a common first index multiply to a $3$-cycle, hence $(\sigma\tau)^3 = 1$.

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

Adjacent swaps (sharing the middle element) satisfy $(\operatorname{swap}(a,b) \operatorname{swap}(b,c))^3 = 1$.

theorem SymmetricCoxeter.succ_eq_castSucc_of_val_succ {n : ℕ} {i j : Fin n} (h : ↑i + 1 = ↑j) : i.succ = j.castSucc

If $i+1 = j$ as naturals then $\operatorname{succ}(i) = \operatorname{castSucc}(j)$ in $\operatorname{Fin}(n+1)$.

theorem SymmetricCoxeter.adjTransposition_coxeter_rel (n : ℕ) (i j : Fin n) : (adjTransposition n i * adjTransposition n j) ^ (CoxeterMatrix.A n).M i j = 1

Adjacent transpositions satisfy the Coxeter relation $(\alpha_i \alpha_j)^{m_{ij}} = 1$ for the type-$A$ Coxeter matrix.

theorem SymmetricCoxeter.adjTransposition_lift_rels (n : ℕ) (r : FreeGroup (Fin n)) : r ∈ (CoxeterMatrix.A n).relationsSet → (FreeGroup.lift (adjTransposition n)) r = 1

The free-group lift of adjTransposition sends every type-$A$ relation to the identity.

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

Canonical homomorphism $W(A_{n-1}) \to S_{n+1}$ from the type-$A$ Coxeter group to the symmetric group, sending generators to adjacent transpositions.

theorem SymmetricCoxeter.coxeterToPermHom_generator (n : ℕ) (i : Fin n) : (coxeterToPermHom n) ((CoxeterMatrix.A n).simple i) = adjTransposition n i

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

theorem SymmetricCoxeter.coxeterToPermHom_surjective (n : ℕ) : Function.Surjective ⇑(coxeterToPermHom n)

coxeterToPermHom is surjective: adjacent transpositions generate $S_{n+1}$.

theorem SymmetricCoxeter.coxeterToPermHom_injective (n : ℕ) : Function.Injective ⇑(coxeterToPermHom n)

coxeterToPermHom is injective, completing the isomorphism $W(A_{n-1}) \cong S_{n+1}$.

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

Group isomorphism $S_{n+1} \cong W(A_{n-1})$, the inverse of coxeterToPermHom.

theorem SymmetricCoxeter.permCoxeterMulEquiv_adjTransposition (n : ℕ) (i : Fin n) : (permCoxeterMulEquiv n) (adjTransposition n i) = (CoxeterMatrix.A n).simple i

The inverse isomorphism sends the $i$-th adjacent transposition to the $i$-th simple generator.

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

The type-$A_{n-1}$ Coxeter system on the symmetric group $S_{n+1}$.