Markov traces on the infinite type-A Hecke algebra

A Markov trace with parameter z : R on the infinite type-A Hecke algebra TauCeti.InfiniteTypeAHeckeAlgebra R q is an R-linear functional τ with

• τ 1 = 1,
• τ (x * y) = τ (y * x), and
• the Markov rule τ (x * T n) = z * τ x for x in the stage of the first n + 1 strands: the generator T n adds the new strand n + 1.

Since the infinite algebra is the union of its stages, such a functional is the same as a family of compatible normalized traces on the stages. Ocneanu's theorem (Jones, Theorem 5.1) asserts that there is exactly one Markov trace for every z, the Ocneanu trace. This file proves the uniqueness half, and the multiplicativity of every Markov trace on disjoint blocks of strands; existence is proved in TauCeti.Algebra.TypeAHeckeAlgebra.OcneanuTrace from the coset basis of the stages. Both results follow from the decomposition Hₙ₊₂ = Hₙ₊₁ + Hₙ₊₁ Tₙ Hₙ₊₁ of the stages (TauCeti.InfiniteTypeAHeckeAlgebra.toSubmodule_stage_add_two), along which the Markov rule computes τ (a * T n * b) = z * τ (b * a).

The characters T i ↦ q and T i ↦ -q⁻¹ are Markov traces with parameters q and -q⁻¹, so by uniqueness they are the Ocneanu traces for these two values of z.

Main definitions

• TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace: the predicate that a linear functional is a Markov trace with parameter z.

Main results

• TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_mul_T_mul: the recursive rule τ (a * T n * b) = z * τ (b * a).
• TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.unique: there is at most one Markov trace with a given parameter.
• TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_mul_shift: block multiplicativity, τ (x * shift a y) = τ x * τ y for x in the stage of the first a strands.
• TauCeti.InfiniteTypeAHeckeAlgebra.isMarkovTrace_indexCharacter and TauCeti.InfiniteTypeAHeckeAlgebra.isMarkovTrace_signCharacter: the two characters are Markov traces.

References

• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335–388, Section 5 (Theorem 5.1 and its proof).

structure TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace {R : Type u_1} [CommRing R] {q : Rˣ} (z : R) (τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R) : Prop

A Markov trace with parameter z on the infinite type-A Hecke algebra: an R-linear functional which is normalized, tracial, and satisfies the Markov rule τ (x * T n) = z * τ x for every x in the stage of the first n + 1 strands.

• map_one : τ 1 = 1

  A Markov trace is normalized.

• map_mul_comm (x y : InfiniteTypeAHeckeAlgebra R q) : τ (x * y) = τ (y * x)

  A Markov trace is tracial.

• map_mul_T {n : ℕ} {x : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q (n + 1)) : τ (x * T q n) = z * τ x

  The Markov rule: multiplying by the generator that adds a new last strand multiplies the trace by z.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_algebraMap {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) (r : R) : τ ((algebraMap R (InfiniteTypeAHeckeAlgebra R q)) r) = r

A Markov trace takes the scalar r to r.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_mul_T_mul {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) {n : ℕ} {a b : InfiniteTypeAHeckeAlgebra R q} (ha : a ∈ stage R q (n + 1)) (hb : b ∈ stage R q (n + 1)) : τ (a * T q n * b) = z * τ (b * a)

The recursive rule for a Markov trace: for a and b in the stage of the first n + 1 strands, τ (a * T n * b) = z * τ (b * a).

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_mul_val_inv_unitT {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) {n : ℕ} {x : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q (n + 1)) : τ (x * ↑(unitT q n)⁻¹) = (z - (↑q - ↑q⁻¹)) * τ x

The Markov rule for the inverse of the generator adding a new last strand: since (T n)⁻¹ = T n - (q - q⁻¹), it multiplies the trace by z - (q - q⁻¹).

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_braidHom_stabilize {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) {n : ℕ} (b : BraidGroup (n + 1)) : τ ↑((braidHom R q (n + 2)) (BraidGroup.strandIncl b * BraidGroup.sigma (Fin.last n))) = z * τ ↑((braidHom R q (n + 1)) b)

Positive stabilization has constant z, independently of the strand count.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_braidHom_stabilizeInv {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) {n : ℕ} (b : BraidGroup (n + 1)) : τ ↑((braidHom R q (n + 2)) (BraidGroup.strandIncl b * (BraidGroup.sigma (Fin.last n))⁻¹)) = (z - (↑q - ↑q⁻¹)) * τ ↑((braidHom R q (n + 1)) b)

Negative stabilization has constant z - (q - q⁻¹), dictated by the Hecke relation.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.unique {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ τ' : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) (hτ' : IsMarkovTrace z τ') : τ = τ'

Uniqueness of the Ocneanu trace. Two Markov traces with the same parameter are equal.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.map_mul_shift {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} {τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R} (hτ : IsMarkovTrace z τ) {a : ℕ} {x : InfiniteTypeAHeckeAlgebra R q} (hx : x ∈ stage R q a) (y : InfiniteTypeAHeckeAlgebra R q) : τ (x * (shift R q a) y) = τ x * τ y

Block multiplicativity. A Markov trace is multiplicative on disjoint blocks of strands: for x in the stage of the first a strands and any y, whose shift by a lives on the strands from a on, τ (x * shift a y) = τ x * τ y. By TauCeti.InfiniteTypeAHeckeAlgebra.coe_blockIncl_tmul, this is the multiplicativity of τ along the disjoint block map TauCeti.InfiniteTypeAHeckeAlgebra.blockIncl.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.isMarkovTrace_indexCharacter {R : Type u_1} [CommRing R] {q : Rˣ} : IsMarkovTrace (↑q) (indexCharacter R q).toLinearMap

The index character T i ↦ q is a Markov trace with parameter q.

theorem TauCeti.InfiniteTypeAHeckeAlgebra.isMarkovTrace_signCharacter {R : Type u_1} [CommRing R] {q : Rˣ} : IsMarkovTrace (-↑q⁻¹) (signCharacter R q).toLinearMap

The sign character T i ↦ -q⁻¹ is a Markov trace with parameter -q⁻¹.