Documentation

TauCeti.Algebra.TypeAHeckeAlgebra.Embedding

The finite type-A Hecke algebras embed in the infinite one #

The map TauCeti.TypeAHeckeAlgebra.toInfinite R q n from the Hecke algebra on n strands to the infinite type-A Hecke algebra, T i ↦ T i, has image the stage of the first n strands. This file proves that it is injective, over every commutative ring R and for every unit q. Hence the finite presentation is isomorphic to the stage (TauCeti.TypeAHeckeAlgebra.stageEquiv), the stage is a free module with basis the images of the elements T_w, and the tower maps are injective.

The proof extends Iwahori's regular representation to the infinite algebra. For a Coxeter system of type A_∞ on a group W' (TauCeti.coxeterMatrixAInfty), the left regular operators CoxeterSystem.heckeLeftMul on W' →₀ R satisfy the defining relations of the infinite algebra, which gives TauCeti.InfiniteTypeAHeckeAlgebra.regularRep. A Coxeter group W of type A_(n-1) maps to W' by s i ↦ s' i (CoxeterSystem.parabolicHom), and this map is injective and preserves lengths, because a standard parabolic subgroup is the Coxeter group of the restricted Coxeter matrix. So a reduced word for w : W stays reduced in W', and the image of T_w in the infinite algebra sends the basis vector of 1 to the basis vector of the image of w (TauCeti.TypeAHeckeAlgebra.regularRep_toInfinite_Tw_apply_single_one). These vectors are linearly independent, and the elements T_w form a basis of the finite algebra, so toInfinite is injective.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.InfiniteTypeAHeckeAlgebra.regularRep {R : Type u_1} [CommRing R] (q : Rˣ) {W' : Type u_2} [Group W'] (cs' : CoxeterSystem coxeterMatrixAInfty W') :
InfiniteTypeAHeckeAlgebra R q →ₐ[R] Module.End R (W' →₀ R)

The regular representation of the infinite type-A Hecke algebra on the free module W' →₀ R over a Coxeter group of type A_∞: the generator T i acts by the left regular operator CoxeterSystem.heckeLeftMul with quadratic coefficient q - q⁻¹.

Instances For
    source
    @[simp]
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.regularRep_T {R : Type u_1} [CommRing R] {q : Rˣ} {W' : Type u_2} [Group W'] (cs' : CoxeterSystem coxeterMatrixAInfty W') (i : ℕ) :
    (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
    @[simp]
    theorem TauCeti.TypeAHeckeAlgebra.regularRep_toInfinite_Tw_apply_single_one {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} {W : Type u_2} {W' : Type u_3} [Group W] [Group W'] (cs : CoxeterSystem (CoxeterMatrix.A (n - 1)) W) (cs' : CoxeterSystem coxeterMatrixAInfty W') (w : W) :
    ((InfiniteTypeAHeckeAlgebra.regularRep q cs') ((toInfinite R q n) (Tw q cs w))) (Finsupp.single 1 1) = Finsupp.single ((cs.parabolicHom cs' ⋯) w) 1

    The image of T_w in the infinite type-A Hecke algebra takes, in the regular representation of the infinite algebra, the basis vector of 1 to the basis vector of the image of w under the inclusion CoxeterSystem.parabolicHom of Coxeter groups of types A_(n-1) and A_∞.

    source
    theorem TauCeti.TypeAHeckeAlgebra.toInfinite_injective (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) :
    Function.Injective ⇑(toInfinite R q n)

    The Hecke algebra on n strands embeds in the infinite type-A Hecke algebra, over every commutative ring and for every unit parameter.

    source
    noncomputable def TauCeti.TypeAHeckeAlgebra.stageEquiv (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) :
    TypeAHeckeAlgebra R q n ≃ₐ[R] ↥(InfiniteTypeAHeckeAlgebra.stage R q n)

    The finite presentation is isomorphic to the stage: the Hecke algebra on n strands is isomorphic to the stage of the first n strands of the infinite type-A Hecke algebra, by the map T i ↦ T i.

    Instances For
      source
      @[simp]
      theorem TauCeti.TypeAHeckeAlgebra.coe_stageEquiv_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (x : TypeAHeckeAlgebra R q n) :
      ↑((stageEquiv R q n) x) = (toInfinite R q n) x

      The isomorphism TauCeti.TypeAHeckeAlgebra.stageEquiv is the map toInfinite.

      source
      @[simp]
      theorem TauCeti.TypeAHeckeAlgebra.toInfinite_stageEquiv_symm_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (x : ↥(InfiniteTypeAHeckeAlgebra.stage R q n)) :
      (toInfinite R q n) ((stageEquiv R q n).symm x) = ↑x

      The inverse of TauCeti.TypeAHeckeAlgebra.stageEquiv is a section of toInfinite.

      source
      theorem TauCeti.TypeAHeckeAlgebra.linearIndependent_toInfinite_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 fun (w : W) => (toInfinite R q n) (Tw q cs w)

      The images in the infinite type-A Hecke algebra of the elements T_w of the Hecke algebra on n strands are linearly independent.

      source
      theorem TauCeti.TypeAHeckeAlgebra.strandIncl_injective (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) :
      Function.Injective ⇑(strandIncl R q n)

      The tower map from n to n + 1 strands is injective.

      source
      instance TauCeti.InfiniteTypeAHeckeAlgebra.instFreeSubtypeMemSubalgebraStage {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} :
      Module.Free R ↥(stage R q n)

      The stage of the first n strands is a free module: the images of the elements T_w of the Hecke algebra on n strands form a basis.

      source
      theorem TauCeti.InfiniteTypeAHeckeAlgebra.finrank_stage_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 ↥(stage R q n) = Nat.card W

      Over a nontrivial commutative ring, the rank of the stage of the first n strands is the order of the Coxeter group W of type A_(n-1).

      source
      instance TauCeti.InfiniteTypeAHeckeAlgebra.instFiniteSubtypeMemSubalgebraStage {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} :
      Module.Finite R ↥(stage R q n)

      The stage of the first n strands is a finitely generated module: the images of the elements T_w, for w in the symmetric group on n letters, form a finite basis.

      source
      theorem TauCeti.InfiniteTypeAHeckeAlgebra.finrank_stage {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} [Nontrivial R] :
      Module.finrank R ↥(stage R q n) = n.factorial

      Over a nontrivial commutative ring, the stage of the first n strands has rank n!.