The regular operators of an Iwahori–Hecke algebra

Let cs : CoxeterSystem M W be a Coxeter system and c an element of a commutative semiring R. On the free R-module W →₀ R, with basis vectors e w = Finsupp.single w 1, this file defines for every simple reflection s = cs.simple i the two operators

• CoxeterSystem.heckeLeftMul cs c i, with e w ↦ e (s * w) if ℓ (s * w) > ℓ w and e w ↦ c • e w + e (s * w) if ℓ (s * w) < ℓ w, and
• CoxeterSystem.heckeRightMul cs c i, the same rule for w * s.

These are left and right multiplication by the generator T s in the regular representation of the Iwahori–Hecke algebra with quadratic relation T s ^ 2 = c • T s + 1, written in the basis T w. They are the device by which one proves that the T w are linearly independent: the operators can be written down without knowing the algebra, and they satisfy its defining relations.

The key point is that left and right operators commute (CoxeterSystem.commute_heckeLeftMul_heckeRightMul); the one non-formal case of this is the length lemma CoxeterSystem.simple_mul_eq_mul_simple_of_length_eq. Consequently an operator commuting with all right operators is determined by its value on e 1 (CoxeterSystem.ext_of_commute_heckeRightMul). Since a product of left operators along a reduced word sends e 1 to the basis vector of the element it spells (CoxeterSystem.prod_map_heckeLeftMul_apply_single_one), and braid words are reduced, the left operators satisfy the braid relations (CoxeterSystem.prod_map_heckeLeftMul_braidWord). Together with the quadratic relation (CoxeterSystem.heckeLeftMul_mul_self) these are the relations of the Iwahori–Hecke algebra.

Main definitions

• CoxeterSystem.heckeLeftMul, CoxeterSystem.heckeRightMul: the left and right regular operators of a simple reflection.

Main results

• CoxeterSystem.commute_heckeLeftMul_heckeRightMul: left and right operators commute.
• CoxeterSystem.heckeLeftMul_mul_self: the quadratic relation.
• CoxeterSystem.ext_of_commute_heckeRightMul: an operator commuting with the right operators is determined by its value on e 1.
• CoxeterSystem.prod_map_heckeLeftMul_apply_single_one: left operators along a reduced word.
• CoxeterSystem.prod_map_heckeLeftMul_braidWord: the braid relations.

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), Chapter 7, whose construction of the generic algebra this follows.

noncomputable def CoxeterSystem.heckeLeftMul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) (i : B) : Module.End R (W →₀ R)

Left multiplication by the Hecke generator T (s i) in the basis T w, with quadratic relation T (s i) ^ 2 = c • T (s i) + 1: the basis vector of w goes to that of s i * w when i is not a left descent of w, and to c times itself plus that of s i * w when it is.

noncomputable def CoxeterSystem.heckeRightMul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) (i : B) : Module.End R (W →₀ R)

Right multiplication by the Hecke generator T (s i) in the basis T w, with quadratic relation T (s i) ^ 2 = c • T (s i) + 1: the basis vector of w goes to that of w * s i when i is not a right descent of w, and to c times itself plus that of w * s i when it is.

@[simp]

theorem CoxeterSystem.heckeLeftMul_single_of_not_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {R : Type u_3} [CommSemiring R] {c : R} {w : W} {i : B} (h : ¬cs.IsLeftDescent w i) (r : R) : (cs.heckeLeftMul c i) (Finsupp.single w r) = Finsupp.single (cs.simple i * w) r

Left multiplication, length increase.

@[simp]

theorem CoxeterSystem.heckeLeftMul_single_of_isLeftDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {R : Type u_3} [CommSemiring R] {c : R} {w : W} {i : B} (h : cs.IsLeftDescent w i) (r : R) : (cs.heckeLeftMul c i) (Finsupp.single w r) = c • Finsupp.single w r + Finsupp.single (cs.simple i * w) r

Left multiplication, length decrease.

@[simp]

theorem CoxeterSystem.heckeRightMul_single_of_not_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {R : Type u_3} [CommSemiring R] {c : R} {w : W} {i : B} (h : ¬cs.IsRightDescent w i) (r : R) : (cs.heckeRightMul c i) (Finsupp.single w r) = Finsupp.single (w * cs.simple i) r

Right multiplication, length increase.

@[simp]

theorem CoxeterSystem.heckeRightMul_single_of_isRightDescent {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {R : Type u_3} [CommSemiring R] {c : R} {w : W} {i : B} (h : cs.IsRightDescent w i) (r : R) : (cs.heckeRightMul c i) (Finsupp.single w r) = c • Finsupp.single w r + Finsupp.single (w * cs.simple i) r

Right multiplication, length decrease.

theorem CoxeterSystem.heckeLeftMul_mul_self {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) (i : B) : cs.heckeLeftMul c i * cs.heckeLeftMul c i = c • cs.heckeLeftMul c i + 1

The quadratic relation for the left operators: heckeLeftMul cs c i ^ 2 = c • heckeLeftMul cs c i + 1.

theorem CoxeterSystem.heckeRightMul_mul_self {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) (i : B) : cs.heckeRightMul c i * cs.heckeRightMul c i = c • cs.heckeRightMul c i + 1

The quadratic relation for the right operators: heckeRightMul cs c i ^ 2 = c • heckeRightMul cs c i + 1.

theorem CoxeterSystem.commute_heckeLeftMul_heckeRightMul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) (i j : B) : Commute (cs.heckeLeftMul c i) (cs.heckeRightMul c j)

Left and right operators commute: heckeLeftMul cs c i and heckeRightMul cs c j commute for all i and j.

theorem CoxeterSystem.ext_of_commute_heckeRightMul {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] {c : R} {f g : Module.End R (W →₀ R)} (hf : ∀ (j : B), Commute f (cs.heckeRightMul c j)) (hg : ∀ (j : B), Commute g (cs.heckeRightMul c j)) (h : f (Finsupp.single 1 1) = g (Finsupp.single 1 1)) : f = g

An operator commuting with the right operators is determined by its value on e 1.

theorem CoxeterSystem.prod_map_heckeLeftMul_apply_single_one {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) {ω : List B} (hω : cs.IsReduced ω) : (List.map (cs.heckeLeftMul c) ω).prod (Finsupp.single 1 1) = Finsupp.single (cs.wordProd ω) 1

Left operators along a reduced word ω send e 1 to the basis vector of the element ω spells.

theorem CoxeterSystem.prod_map_heckeLeftMul_braidWord {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {R : Type u_3} [CommSemiring R] (c : R) (i i' : B) : (List.map (cs.heckeLeftMul c) (braidWord M i i')).prod = (List.map (cs.heckeLeftMul c) (braidWord M i' i)).prod

The braid relations for the left operators: the two braid words at (i, i') give the same operator.