The coset basis of a stage over the previous one

Let Hₙ be the stage of the first n strands of the infinite type-A Hecke algebra (TauCeti.InfiniteTypeAHeckeAlgebra.stage). This file proves that the next stage Hₙ₊₁ is a free left Hₙ-module of rank n + 1, with basis the descending products

cosetRep q n m = T (n - 1) * T (n - 2) * ⋯ * T m, for m = 0, …, n,

of the generators (the empty product 1 for m = n). They are the elements T_w attached to the minimal-length representatives w = s (n - 1) ⋯ s m of the cosets of the symmetric group on n letters in the symmetric group on n + 1 letters, although that identification is not needed here. Concretely, every element of Hₙ₊₁ is uniquely a sum ∑ m, a m * cosetRep q n m with coefficients a m in Hₙ (TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv), and the coefficients depend Hₙ-linearly on the element (TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_symm_mul). This is the left-module form of the decomposition Hₙ₊₂ = Hₙ₊₁ + Hₙ₊₁ Tₙ Hₙ₊₁ (TauCeti.InfiniteTypeAHeckeAlgebra.toSubmodule_stage_add_two). These coordinates are the ones in which Jones computes the Ocneanu trace recursively, one strand at a time.

The reversal anti-automorphism TauCeti.InfiniteTypeAHeckeAlgebra.reverse, which fixes every generator and reverses products, carries this left basis to a right one: Hₙ₊₁ is also a free right Hₙ-module of rank n + 1, with basis the ascending products reverse q (cosetRep q n m) = T m * ⋯ * T (n - 1) (TauCeti.InfiniteTypeAHeckeAlgebra.reverse_cosetRep, TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight). This is the form in which Hₙ₊₁ is a right Hₙ-module for induction Hₙ₊₁ ⊗[Hₙ] M.

Main definitions

• TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep: the descending product T (n - 1) * ⋯ * T m.
• TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv: the R-linear isomorphism from Fin (n + 1) → Hₙ to Hₙ₊₁ sending a to ∑ m, a m * cosetRep q n m.
• TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight: the R-linear isomorphism from Fin (n + 1) → Hₙ to Hₙ₊₁ sending a to ∑ m, reverse q (cosetRep q n m) * a m.

Main results

• TauCeti.InfiniteTypeAHeckeAlgebra.coe_cosetEquiv_apply: the formula for cosetEquiv.
• TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_smul and TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_symm_mul: cosetEquiv is Hₙ-linear for left multiplication, so the representatives form a basis of Hₙ₊₁ as a left Hₙ-module.
• TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_symm_inclusion: an element b of Hₙ has coordinate b at the representative cosetRep q n n = 1, and coordinate zero at every other index.
• TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight_op_smul and TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight_symm_mul: cosetEquivRight is Hₙ-linear for right multiplication, so the reversed representatives form a basis of Hₙ₊₁ as a right Hₙ-module; TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight_symm_inclusion is the counterpart of cosetEquiv_symm_inclusion.

References

• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388, Section 4.
• C. Kassel and V. Turaev, Braid Groups, Springer GTM 247 (2008), Section 4.2.

def TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep {R : Type u_1} [CommRing R] (q : Rˣ) (n m : ℕ) : InfiniteTypeAHeckeAlgebra R q

The descending product T (n - 1) * T (n - 2) * ⋯ * T m of the generators from T (n - 1) down to T m, which is 1 when n ≤ m. For m ≤ n it is the element T_w of the minimal-length representative w = s (n - 1) ⋯ s m of a coset of the symmetric group on n letters in the symmetric group on n + 1 letters.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_of_le {R : Type u_1} [CommRing R] {q : Rˣ} {n m : ℕ} (h : n ≤ m) : cosetRep q n m = 1

The descending product from T (n - 1) down to T m is empty when n ≤ m.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_self {R : Type u_1} [CommRing R] {q : Rˣ} (n : ℕ) : cosetRep q n n = 1

The trivial representative is 1.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_succ {R : Type u_1} [CommRing R] {q : Rˣ} {n m : ℕ} (h : m ≤ n) : cosetRep q (n + 1) m = T q n * cosetRep q n m

Raising the top of the descending product adds a generator on the left.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_succ_mul_T {R : Type u_1} [CommRing R] {q : Rˣ} {n m : ℕ} (h : m < n) : cosetRep q n (m + 1) * T q m = cosetRep q n m

Lowering the bottom of the descending product adds a generator on the right.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_mem_stage {R : Type u_1} [CommRing R] {q : Rˣ} (n m : ℕ) : cosetRep q n m ∈ stage R q (n + 1)

The descending product from T (n - 1) lies in the stage of the first n + 1 strands.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_mul_T_of_add_one_lt {R : Type u_1} [CommRing R] {q : Rˣ} {n m i : ℕ} (h : i + 1 < m) : cosetRep q n m * T q i = T q i * cosetRep q n m

A generator far below the descending product commutes past it.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_mul_T_self {R : Type u_1} [CommRing R] {q : Rˣ} {n m : ℕ} (h : m < n) : cosetRep q n m * T q m = (↑q - ↑q⁻¹) • cosetRep q n m + cosetRep q n (m + 1)

For m < n, multiplying the descending product on the right by its lowest generator T m gives (q - q⁻¹) • cosetRep q n m + cosetRep q n (m + 1).

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_mul_T_succ {R : Type u_1} [CommRing R] {q : Rˣ} {n m j : ℕ} (hm : m ≤ j) (hj : j + 2 ≤ n) : cosetRep q n m * T q (j + 1) = T q j * cosetRep q n m

A generator T (j + 1) strictly inside the descending product moves to its left as T j, by the braid relation.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.shift_cosetRep {R : Type u_1} [CommRing R] {q : Rˣ} (k n m : ℕ) : (shift R q k) (cosetRep q n m) = cosetRep q (n + k) (m + k)

The strand shift by k of the descending product from T (n - 1) down to T m is the descending product from T (n + k - 1) down to T (m + k).

theorem TauCeti.InfiniteTypeAHeckeAlgebra.isUnit_mk_cosetRep {R : Type u_1} [CommRing R] {q : Rˣ} (n m : ℕ) : IsUnit ⟨cosetRep q n m, ⋯⟩

The descending product from T (n - 1) is a unit of the stage of the first n + 1 strands.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetRep_mul_cosetRep_mul_T_zero {R : Type u_1} [CommRing R] {q : Rˣ} (b : ℕ) : cosetRep q b 0 * cosetRep q (b + 1) 1 * T q 0 = T q b * (cosetRep q b 0 * cosetRep q (b + 1) 1)

Moving two strands past b strands carries the crossing T 0 of the two strands to the crossing T b.

noncomputable def TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : (Fin (n + 1) → ↥(stage R q n)) ≃ₗ[R] ↥(stage R q (n + 1))

The coset basis. The stage of the first n + 1 strands is a free left module over the stage of the first n strands with basis the descending products cosetRep q n m, m = 0, …, n: the R-linear map sending coefficients a : Fin (n + 1) → Hₙ to ∑ m, a m * cosetRep q n m is an isomorphism onto Hₙ₊₁.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.coe_cosetEquiv_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (a : Fin (n + 1) → ↥(stage R q n)) : ↑((cosetEquiv R q n) a) = ∑ m : Fin (n + 1), ↑(a m) * cosetRep q n ↑m

The coset isomorphism sends coefficients a to ∑ m, a m * cosetRep q n m.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (a : Fin (n + 1) → ↥(stage R q n)) : (cosetEquiv R q n) a = ∑ m : Fin (n + 1), (Subalgebra.inclusion ⋯) (a m) * ⟨cosetRep q n ↑m, ⋯⟩

The coset isomorphism sends coefficients a to ∑ m, a m * cosetRep q n m, computed in the stage of the first n + 1 strands.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_smul {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : ↥(stage R q n)) (a : Fin (n + 1) → ↥(stage R q n)) : (cosetEquiv R q n) (b • a) = (Subalgebra.inclusion ⋯) b * (cosetEquiv R q n) a

The coset isomorphism is linear for left multiplication by the stage of the first n strands.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_symm_mul {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : ↥(stage R q n)) (x : ↥(stage R q (n + 1))) : (cosetEquiv R q n).symm ((Subalgebra.inclusion ⋯) b * x) = b • (cosetEquiv R q n).symm x

The coefficients of an element of the stage n + 1 along the representatives cosetRep q n m are linear for left multiplication by the stage n.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_symm_inclusion {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : ↥(stage R q n)) : (cosetEquiv R q n).symm ((Subalgebra.inclusion ⋯) b) = Pi.single (Fin.last n) b

An element of the stage n is its own coefficient at the trivial representative cosetRep q n n = 1, and has no other coefficients.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv_symm_inclusion_mul_cosetRep {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (m : Fin (n + 1)) (b : ↥(stage R q n)) : (cosetEquiv R q n).symm ((Subalgebra.inclusion ⋯) b * ⟨cosetRep q n ↑m, ⋯⟩) = Pi.single m b

The product of an element b of the stage n with the representative cosetRep q n m has coefficient b at m, and no other coefficients.

The right coset basis is the image of the left one under the reversal anti-automorphism reverse, which fixes the generators, reverses products and preserves the stages.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.reverse_cosetRep {R : Type u_1} [CommRing R] {q : Rˣ} (n m : ℕ) : (reverse q) (cosetRep q n m) = (List.map (T q) (List.Ico m n)).prod

The reversal of the descending product T (n - 1) * ⋯ * T m is the ascending product T m * ⋯ * T (n - 1).

noncomputable def TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight (R : Type u_1) [CommRing R] (q : Rˣ) (n : ℕ) : (Fin (n + 1) → ↥(stage R q n)) ≃ₗ[R] ↥(stage R q (n + 1))

The right coset basis. The stage of the first n + 1 strands is a free right module over the stage of the first n strands with basis the ascending products reverse q (cosetRep q n m) = T m * ⋯ * T (n - 1), m = 0, …, n: the R-linear map sending coefficients a : Fin (n + 1) → Hₙ to ∑ m, reverse q (cosetRep q n m) * a m is an isomorphism onto Hₙ₊₁.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.coe_cosetEquivRight_apply {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (a : Fin (n + 1) → ↥(stage R q n)) : ↑((cosetEquivRight R q n) a) = ∑ m : Fin (n + 1), (reverse q) (cosetRep q n ↑m) * ↑(a m)

The right coset isomorphism sends coefficients a to ∑ m, reverse q (cosetRep q n m) * a m.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight_op_smul {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : ↥(stage R q n)) (a : Fin (n + 1) → ↥(stage R q n)) : (cosetEquivRight R q n) (MulOpposite.op b • a) = (cosetEquivRight R q n) a * (Subalgebra.inclusion ⋯) b

The right coset isomorphism is linear for right multiplication by the stage of the first n strands.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight_symm_mul {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (x : ↥(stage R q (n + 1))) (b : ↥(stage R q n)) : (cosetEquivRight R q n).symm (x * (Subalgebra.inclusion ⋯) b) = MulOpposite.op b • (cosetEquivRight R q n).symm x

The coefficients of an element of the stage n + 1 along the representatives reverse q (cosetRep q n m) are linear for right multiplication by the stage n.

@[simp]

theorem TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquivRight_symm_inclusion {R : Type u_1} [CommRing R] {q : Rˣ} {n : ℕ} (b : ↥(stage R q n)) : (cosetEquivRight R q n).symm ((Subalgebra.inclusion ⋯) b) = Pi.single (Fin.last n) b

An element of the stage n is its own coefficient at the trivial representative reverse q (cosetRep q n n) = 1, and has no other coefficients.