Reduced-word elements of the type-A Hecke algebra

Let cs be a Coxeter system of type A_(n-1) on a group W, so that its simple reflections are indexed by the generators T i, i : Fin (n - 1), of the Hecke algebra TypeAHeckeAlgebra R q n on n strands. For w : W the element TypeAHeckeAlgebra.Tw cs w, usually written T_w, is the product T i₁ * ⋯ * T iₖ along any reduced expression w = s i₁ ⋯ s iₖ. By Matsumoto's theorem (TauCeti.matsumoto) this does not depend on the reduced expression, because the generators T i satisfy the braid relations of the type-A Coxeter matrix.

The elements T_w multiply by the length rule: T_v * T_w = T_(v * w) when lengths add, and multiplication by a generator T i on either side follows the length-increase/length-decrease rule,

• T i * T_w = T_(s i * w) if ℓ (s i * w) = ℓ w + 1, and
• T i * T_w = (q - q⁻¹) • T_w + T_(s i * w) if ℓ (s i * w) < ℓ w,

with the mirror statements on the right. Consequently the elements T_w span the Hecke algebra as an R-module. The Coxeter system is an arbitrary one of type A_(n-1), so these statements apply to the abstract Coxeter group (CoxeterMatrix.A (n - 1)).Group and to any concrete model of it, such as the symmetric group on n letters.

Main definitions

• TauCeti.TypeAHeckeAlgebra.Tw: the element T_w attached to w : W.

Main results

• TauCeti.TypeAHeckeAlgebra.Tw_wordProd: T_w is the product of the generators along any reduced expression of w.
• TauCeti.TypeAHeckeAlgebra.Tw_mul_Tw: T_v * T_w = T_(v * w) when ℓ (v * w) = ℓ v + ℓ w.
• TauCeti.TypeAHeckeAlgebra.T_mul_Tw_of_not_isLeftDescent, TauCeti.TypeAHeckeAlgebra.T_mul_Tw_of_isLeftDescent, TauCeti.TypeAHeckeAlgebra.Tw_mul_T_of_not_isRightDescent and TauCeti.TypeAHeckeAlgebra.Tw_mul_T_of_isRightDescent: multiplication by a generator.
• TauCeti.TypeAHeckeAlgebra.mul_mem_span_image_Tw: the subalgebra generated by the T i, i ∈ J, preserves the span of the T_w, w ∈ S, when S is stable under the s i, i ∈ J.
• TauCeti.TypeAHeckeAlgebra.span_range_Tw: the elements T_w span the Hecke algebra.

References

• N. Iwahori, On the structure of a Hecke ring of a Chevalley group over a finite field, J. Fac. Sci. Univ. Tokyo Sect. I 10 (1964), 215–236.
• J. E. Humphreys, Reflection Groups and Coxeter Groups, CUP (1990), Section 7.1.
• M. Geck and G. Pfeiffer, Characters of Finite Coxeter Groups and Iwahori-Hecke Algebras, OUP (2000), Section 4.4.

theorem TauCeti.TypeAHeckeAlgebra.prod_map_T_braidWord {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (i j : Fin (n - 1)) : (List.map (T q) (CoxeterSystem.braidWord (CoxeterMatrix.A (n - 1)) i j)).prod = (List.map (T q) (CoxeterSystem.braidWord (CoxeterMatrix.A (n - 1)) j i)).prod

The Hecke generators satisfy every braid relation of the type-A Coxeter matrix: for all i and j, the two alternating words in T i and T j whose length is the Coxeter-matrix entry at (i, j) have the same product.

noncomputable def TauCeti.TypeAHeckeAlgebra.Tw {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (w : W) : TypeAHeckeAlgebra R q n

The element T_w of the type-A Hecke algebra attached to an element w of a Coxeter system of type A_(n-1): the product of the generators T i along a reduced expression of w. It is the reduced-word lift of Matsumoto's theorem (TauCeti.existsUnique_reducedWordLift), so it does not depend on the reduced expression (TauCeti.TypeAHeckeAlgebra.Tw_wordProd).

theorem TauCeti.TypeAHeckeAlgebra.Tw_wordProd {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {ω : List (Fin (n - 1))} (hω : cs.IsReduced ω) : Tw q cs (cs.wordProd ω) = (List.map (T q) ω).prod

T_w is the product of the generators along any reduced expression of w.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.Tw_one {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) : Tw q cs 1 = 1

The element T_w attached to the identity is 1.

@[simp]

theorem TauCeti.TypeAHeckeAlgebra.Tw_simple {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (i : Fin (n - 1)) : Tw q cs (cs.simple i) = T q i

The element T_w attached to a simple reflection is the corresponding generator.

theorem TauCeti.TypeAHeckeAlgebra.isUnit_Tw {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (w : W) : IsUnit (Tw q cs w)

Each element T_w is invertible.

theorem TauCeti.TypeAHeckeAlgebra.Tw_mul_Tw {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {v w : W} (h : cs.length (v * w) = cs.length v + cs.length w) : Tw q cs v * Tw q cs w = Tw q cs (v * w)

Length additivity. If ℓ (v * w) = ℓ v + ℓ w, then T_v * T_w = T_(v * w).

theorem TauCeti.TypeAHeckeAlgebra.T_mul_Tw_of_not_isLeftDescent {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {w : W} {i : Fin (n - 1)} (h : ¬cs.IsLeftDescent w i) : T q i * Tw q cs w = Tw q cs (cs.simple i * w)

Left multiplication, length increase. If s i * w is longer than w, then T i * T_w = T_(s i * w).

theorem TauCeti.TypeAHeckeAlgebra.Tw_mul_T_of_not_isRightDescent {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {w : W} {i : Fin (n - 1)} (h : ¬cs.IsRightDescent w i) : Tw q cs w * T q i = Tw q cs (w * cs.simple i)

Right multiplication, length increase. If w * s i is longer than w, then T_w * T i = T_(w * s i).

theorem TauCeti.TypeAHeckeAlgebra.T_mul_Tw_of_isLeftDescent {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {w : W} {i : Fin (n - 1)} (h : cs.IsLeftDescent w i) : T q i * Tw q cs w = (↑q - ↑q⁻¹) • Tw q cs w + Tw q cs (cs.simple i * w)

Left multiplication, length decrease. If s i * w is shorter than w, then T i * T_w = (q - q⁻¹) • T_w + T_(s i * w).

theorem TauCeti.TypeAHeckeAlgebra.Tw_mul_T_of_isRightDescent {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {w : W} {i : Fin (n - 1)} (h : cs.IsRightDescent w i) : Tw q cs w * T q i = (↑q - ↑q⁻¹) • Tw q cs w + Tw q cs (w * cs.simple i)

Right multiplication, length decrease. If w * s i is shorter than w, then T_w * T i = (q - q⁻¹) • T_w + T_(w * s i).

theorem TauCeti.TypeAHeckeAlgebra.mul_mem_span_image_Tw {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) {J : Set (Fin (n - 1))} {S : Set W} (hS : ∀ i ∈ J, ∀ w ∈ S, cs.simple i * w ∈ S) {x y : TypeAHeckeAlgebra R q n} (hx : x ∈ Algebra.adjoin R (T q '' J)) (hy : y ∈ Submodule.span R (Tw q cs '' S)) : x * y ∈ Submodule.span R (Tw q cs '' S)

Let S ⊆ W be closed under left multiplication by the simple reflections s i, i ∈ J. Then the subalgebra generated by the generators T i, i ∈ J, multiplies the span of the elements T_w, w ∈ S, into itself.

theorem TauCeti.TypeAHeckeAlgebra.span_range_Tw {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) : Submodule.span R (Set.range (Tw q cs)) = ⊤

The elements T_w span the type-A Hecke algebra as an R-module.