Documentation

TauCeti.Algebra.TypeAHeckeAlgebra.OcneanuTrace

Existence of the Ocneanu trace #

For every commutative ring R, unit q : Rˣ and parameter z : R, this file constructs the Ocneanu trace TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace R q z on the infinite type-A Hecke algebra: the 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. Together with the uniqueness theorem TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.unique, this is Ocneanu's theorem: for every z there is exactly one Markov trace with parameter z (TauCeti.InfiniteTypeAHeckeAlgebra.existsUnique_isMarkovTrace). No positivity is asserted.

The trace is built one strand at a time, following Jones. Write Hₙ for the stage of the first n strands. By the coset basis theorem (TauCeti.InfiniteTypeAHeckeAlgebra.cosetEquiv), every element of Hₙ₊₂ is uniquely a sum ∑ m, a m * cosetRep q (n + 1) m with coefficients in Hₙ₊₁, where cosetRep q (n + 1) m = T n * cosetRep q n m for m ≤ n and the last representative is 1. A trace φ on Hₙ₊₁ extends to Hₙ₊₂ by sending this sum to φ (a (n + 1)) + z * ∑ (m ≤ n), φ (cosetRep q n m * a m), so that a * T n * b ↦ z * φ (b * a) for a, b in Hₙ₊₁. That the extension is again a trace is checked on the decomposition Hₙ₊₂ = Hₙ₊₁ + Hₙ₊₁ Tₙ Hₙ₊₁ (TauCeti.InfiniteTypeAHeckeAlgebra.toSubmodule_stage_add_two), using the same decomposition of Hₙ₊₁ one level down, the quadratic relation and the braid relation. The stage traces are compatible, so they glue to a functional on the union of the stages.

Main definitions #

Main results #

References #

Extending a trace from one stage to the next #

The extension of the extension of a trace is a trace #

The traces on the stages #

The Ocneanu trace #

source
noncomputable def TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace (R : Type u_1) [CommRing R] (q : Rˣ) (z : R) :
InfiniteTypeAHeckeAlgebra R q →ₗ[R] R

The Ocneanu trace with parameter z: the unique normalized trace on the infinite type-A Hecke algebra satisfying the Markov rule τ (x * T n) = z * τ x for x in the stage of the first n + 1 strands (TauCeti.InfiniteTypeAHeckeAlgebra.isMarkovTrace_ocneanuTrace and TauCeti.InfiniteTypeAHeckeAlgebra.IsMarkovTrace.eq_ocneanuTrace).

Instances For
    source
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.isMarkovTrace_ocneanuTrace {R : Type u_1} [CommRing R] {q : Rˣ} (z : R) :
    IsMarkovTrace z (ocneanuTrace R q z)

    Existence of the Ocneanu trace. The Ocneanu trace is a Markov trace with parameter z.

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

    Ocneanu's theorem. Every Markov trace with parameter z is the Ocneanu trace.

    source
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.existsUnique_isMarkovTrace {R : Type u_1} [CommRing R] {q : Rˣ} (z : R) :
    ∃! τ : InfiniteTypeAHeckeAlgebra R q →ₗ[R] R, IsMarkovTrace z τ

    Ocneanu's theorem. For every parameter z there is exactly one Markov trace with parameter z.

    source
    @[simp]
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace_one {R : Type u_1} [CommRing R] {q : Rˣ} (z : R) :
    (ocneanuTrace R q z) 1 = 1

    The Ocneanu trace is normalized.

    source
    @[simp]
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace_T {R : Type u_1} [CommRing R] {q : Rˣ} (z : R) (i : ℕ) :
    (ocneanuTrace R q z) (T q i) = z

    Every generator has trace z.

    source
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace_val_inv_unitT {R : Type u_1} [CommRing R] {q : Rˣ} (z : R) (i : ℕ) :
    (ocneanuTrace R q z) ↑(unitT q i)⁻¹ = z - (↑q - ↑q⁻¹)

    The inverse of every generator has trace z - (q - q⁻¹).

    source
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace_eq_indexCharacter {R : Type u_1} [CommRing R] {q : Rˣ} :
    ocneanuTrace R q ↑q = (indexCharacter R q).toLinearMap

    At z = q the Ocneanu trace is the index character T i ↦ q.

    source
    theorem TauCeti.InfiniteTypeAHeckeAlgebra.ocneanuTrace_eq_signCharacter {R : Type u_1} [CommRing R] {q : Rˣ} :
    ocneanuTrace R q (-↑q⁻¹) = (signCharacter R q).toLinearMap

    At z = -q⁻¹ the Ocneanu trace is the sign character T i ↦ -q⁻¹.

    source
    theorem TauCeti.TypeAHeckeAlgebra.eq_ocneanuTrace_toInfinite {R : Type u_1} [CommRing R] {q : Rˣ} {z : R} (φ : (n : ℕ) → TypeAHeckeAlgebra R q n →ₗ[R] R) (h_one : (φ 0) 1 = 1) (h_incl : ∀ (n : ℕ) (x : TypeAHeckeAlgebra R q n), (φ (n + 1)) ((strandIncl R q n) x) = (φ n) x) (h_comm : ∀ (n : ℕ) (x y : TypeAHeckeAlgebra R q n), (φ n) (x * y) = (φ n) (y * x)) (h_markov : ∀ (n : ℕ) (x : TypeAHeckeAlgebra R q (n + 1)), (φ (n + 2)) ((strandIncl R q (n + 1)) x * T q (Fin.last n)) = z * (φ (n + 1)) x) (n : ℕ) (x : TypeAHeckeAlgebra R q n) :
    (φ n) x = (InfiniteTypeAHeckeAlgebra.ocneanuTrace R q z) ((toInfinite R q n) x)

    Finite Markov towers are restrictions of the Ocneanu trace. A family of linear functionals φ n on the Hecke algebras on n strands which is normalized on zero strands, compatible with the tower maps, tracial at each level, and satisfies the Markov rule φ (n + 2) (strandIncl R q (n + 1) x * T q (Fin.last n)) = z * φ (n + 1) x for the last generator, is the Ocneanu trace with parameter z restricted along toInfinite.