Documentation

TauCeti.Algebra.TypeAHeckeAlgebra.Basis

The basis theorem for the type-A Hecke algebra #

Let cs be a Coxeter system of type A_(n-1) on a group W. The elements T_w, w : W, of the Hecke algebra TypeAHeckeAlgebra R q n (TauCeti.TypeAHeckeAlgebra.Tw) span it; this file proves that they are linearly independent over every commutative ring R and every unit q, so that they form a basis TauCeti.TypeAHeckeAlgebra.basisTw.

The proof is Iwahori's. The left regular operators CoxeterSystem.heckeLeftMul on the free module W →₀ R, with quadratic coefficient q - q⁻¹, satisfy the defining relations of the Hecke algebra, which gives the regular representation TauCeti.TypeAHeckeAlgebra.regularRep. It sends T_w to an operator taking the basis vector of 1 to that of w, so evaluating at the basis vector of 1 is a linear map sending the family T_w to the standard basis of W →₀ R. That evaluation is then the coordinate map of the basis (TauCeti.TypeAHeckeAlgebra.basisTw_repr_apply), and the regular representation is faithful.

The Coxeter system is an arbitrary one of type A_(n-1). For the abstract Coxeter group (CoxeterMatrix.A (n - 1)).Group this shows that the Hecke algebra is a free module; for a concrete finite model of the Coxeter group, such as the symmetric group on n letters, the rank is the order of that group (TauCeti.TypeAHeckeAlgebra.finrank_eq_natCard).

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.TypeAHeckeAlgebra.regularRep {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) :
TypeAHeckeAlgebra R q n →ₐ[R] Module.End R (W →₀ R)

The regular representation of the type-A Hecke algebra on the free module W →₀ R: the generator T i acts by the left regular operator CoxeterSystem.heckeLeftMul with quadratic coefficient q - q⁻¹, sending the basis vector of w to that of s i * w when i is not a left descent of w, and to (q - q⁻¹) times itself plus that of s i * w when it is.

Instances For
    source
    @[simp]
    theorem TauCeti.TypeAHeckeAlgebra.regularRep_T {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)) :
    (regularRep q cs) (T q i) = cs.heckeLeftMul (↑q - ↑q⁻¹) i

    The regular representation takes the generator T i to the left regular operator of the simple reflection s i.

    source
    theorem TauCeti.TypeAHeckeAlgebra.commute_regularRep_heckeRightMul {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (x : TypeAHeckeAlgebra R q n) (i : Fin (n - 1)) :
    Commute ((regularRep q cs) x) (cs.heckeRightMul (↑q - ↑q⁻¹) i)

    The regular representation commutes with every right regular Hecke operator.

    source
    @[simp]
    theorem TauCeti.TypeAHeckeAlgebra.regularRep_Tw_apply_single_one {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (w : W) :
    ((regularRep q cs) (Tw q cs w)) (Finsupp.single 1 1) = Finsupp.single w 1

    In the regular representation, T_w takes the basis vector of 1 to that of w.

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

    The elements T_w are linearly independent over every commutative ring and for every unit parameter.

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

    The basis theorem: the elements T_w, w : W, form a basis of the type-A Hecke algebra over every commutative ring and for every unit parameter.

    Instances For
      source
      @[simp]
      theorem TauCeti.TypeAHeckeAlgebra.coe_basisTw {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) :
      ⇑(basisTw q cs) = Tw q cs

      The basis vectors of TauCeti.TypeAHeckeAlgebra.basisTw are the elements T_w.

      source
      theorem TauCeti.TypeAHeckeAlgebra.basisTw_repr_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (x : TypeAHeckeAlgebra R q n) :
      (basisTw q cs).repr x = ((regularRep q cs) x) (Finsupp.single 1 1)

      The coordinates of x in the basis T_w are the image under the regular representation of x of the basis vector of 1.

      source
      theorem TauCeti.TypeAHeckeAlgebra.basisTw_repr_T_mul {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)) (x : TypeAHeckeAlgebra R q n) (w : W) :
      ((basisTw q cs).repr (T q i * x)) w = (if cs.IsLeftDescent w i then (↑q - ↑q⁻¹) * ((basisTw q cs).repr x) w else 0) + ((basisTw q cs).repr x) (cs.simple i * w)

      The coefficient of T_w after left multiplication by a simple generator.

      source
      theorem TauCeti.TypeAHeckeAlgebra.basisTw_repr_mul_T {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (x : TypeAHeckeAlgebra R q n) (i : Fin (n - 1)) (w : W) :
      ((basisTw q cs).repr (x * T q i)) w = (if cs.IsRightDescent w i then (↑q - ↑q⁻¹) * ((basisTw q cs).repr x) w else 0) + ((basisTw q cs).repr x) (w * cs.simple i)

      The coefficient of T_w after right multiplication by a simple generator.

      source
      theorem TauCeti.TypeAHeckeAlgebra.regularRep_injective {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) :
      Function.Injective ⇑(regularRep q cs)

      The regular representation is faithful.

      source
      instance TauCeti.TypeAHeckeAlgebra.instFree {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} :
      Module.Free R (TypeAHeckeAlgebra R q n)

      The type-A Hecke algebra is a free module, with basis the elements T_w of the abstract Coxeter group of type A_(n-1).

      source
      theorem TauCeti.TypeAHeckeAlgebra.finrank_eq_natCard {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} [Group W] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) [Nontrivial R] :
      Module.finrank R (TypeAHeckeAlgebra R q n) = Nat.card W

      Over a nontrivial commutative ring, the rank of the type-A Hecke algebra is the order of the Coxeter group W of type A_(n-1). (When W is infinite, both sides are 0 by convention.)