The Markov trace on the Temperley-Lieb algebra

A Markov trace on the tower of Temperley-Lieb algebras TemperleyLieb R δ n is a family of linear functionals tr with tr (x * y) = tr (y * x) that is compatible with adding a strand: tr (strandIncl x) = δ * tr x, and tr (strandIncl x * e (Fin.last n)) = tr x. Composed with the Jones representation of the braid group it is the braid route to the Kauffman bracket and the Jones polynomial: the trace property gives invariance under conjugation of braids, and the two compatibilities give invariance under the Markov stabilization move. This file constructs such a trace, TauCeti.TemperleyLieb.markovTrace, for every loop value of the form δ = -(q + q⁻¹) with q a unit, normalized by tr 1 = δ ^ n.

The construction is the spin (vertex) model. The algebra on n strands acts on functions of n spins s : Fin n → Bool: the generator e i acts as spinGenerator q j k on the strands j = i, k = i + 1, the identity on the other strands tensored with the rank-one matrix cup ⊗ cap on these two, where the cup vector spinCup q and the cap covector spinCap q are supported on the two antiparallel pairs of spins:

• cup (true, false) = -q, cup (false, true) = 1;
• cap (true, false) = 1, cap (false, true) = -q⁻¹.

These matrices satisfy the three families of Temperley-Lieb relations, which is what makes TauCeti.TemperleyLieb.spinRep an algebra map: the quadratic relation, since closing a loop gives cap · cup = -(q + q⁻¹) = δ; the adjacent zigzag relations, since the two zigzag contractions of a cup with a cap are the identity; and the distant commutation relation, since generator matrices on disjoint pairs of strands commute. The trace is the weighted matrix trace tr x = trace (diagonal (spinWeight q) * spinRep x) with spin weights -q for true and -q⁻¹ for false. Every generator preserves the multiset of spins it touches, so the weight matrix commutes with the representation and the weighted trace is a trace. The weights sum to δ, which gives tr (strandIncl x) = δ * tr x, and the weighted partial trace of cup ⊗ cap over its second strand, with that strand weighted by markovWeight q, is the identity, which gives the Markov property.

Main definitions

• TauCeti.TemperleyLieb.spinGenerator: the matrix of a generator in the spin model.
• TauCeti.TemperleyLieb.spinRep: the spin representation of the Temperley-Lieb algebra.
• TauCeti.TemperleyLieb.spinWeight: the weight of a spin configuration.
• Matrix.extendLast: a matrix on m spins acting on m + 1 spins, as the identity on the last one: the Kronecker product 1 ⊗ₖ X, reindexed along Fin.snocEquiv.
• TauCeti.TemperleyLieb.markovTrace: the Markov trace.

Main results

• TauCeti.TemperleyLieb.markovTrace_one: the trace of the identity on n strands is δ ^ n.
• TauCeti.TemperleyLieb.markovTrace_mul_comm: the trace property.
• TauCeti.TemperleyLieb.markovTrace_strandIncl: adding a straight strand multiplies the trace by δ.
• TauCeti.TemperleyLieb.markovTrace_strandIncl_mul_e_last: the Markov property, capping the added strand with the previous one does not change the trace.

References

• V. F. R. Jones, Hecke algebra representations of braid groups and link polynomials, Ann. of Math. 126 (1987), 335-388 (the Markov trace on the Temperley-Lieb algebras).
• V. G. Turaev, The Yang-Baxter equation and invariants of links, Invent. Math. 92 (1988), 527-553 (link invariants from a weighted trace of a vertex model).
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395-407.

def TauCeti.TemperleyLieb.spinCup {R : Type u_1} [CommRing R] (q : Rˣ) : Bool → Bool → R

The cup vector of the spin model: the weight of a pair of spins at the two feet of a cup. It is supported on the antiparallel pairs, with cup (true, false) = -q and cup (false, true) = 1.

Equations

• TauCeti.TemperleyLieb.spinCup q true false = -↑q
• TauCeti.TemperleyLieb.spinCup q false true = 1
• TauCeti.TemperleyLieb.spinCup q x✝¹ x✝ = 0

def TauCeti.TemperleyLieb.spinCap {R : Type u_1} [CommRing R] (q : Rˣ) : Bool → Bool → R

The cap covector of the spin model: the weight of a pair of spins at the two feet of a cap. It is supported on the antiparallel pairs, with cap (true, false) = 1 and cap (false, true) = -q⁻¹.

Equations

• TauCeti.TemperleyLieb.spinCap q true false = 1
• TauCeti.TemperleyLieb.spinCap q false true = -↑q⁻¹
• TauCeti.TemperleyLieb.spinCap q x✝¹ x✝ = 0

def TauCeti.TemperleyLieb.markovWeight {R : Type u_1} [CommRing R] (q : Rˣ) : Bool → R

The weight of a single spin in the Markov trace: -q for true and -q⁻¹ for false. The two weights sum to the loop value -(q + q⁻¹).

Equations

• TauCeti.TemperleyLieb.markovWeight q true = -↑q
• TauCeti.TemperleyLieb.markovWeight q false = -↑q⁻¹

@[simp]

theorem TauCeti.TemperleyLieb.spinCup_true_false {R : Type u_1} [CommRing R] (q : Rˣ) : spinCup q true false = -↑q

@[simp]

theorem TauCeti.TemperleyLieb.spinCup_false_true {R : Type u_1} [CommRing R] (q : Rˣ) : spinCup q false true = 1

@[simp]

theorem TauCeti.TemperleyLieb.spinCup_self {R : Type u_1} [CommRing R] (q : Rˣ) (x : Bool) : spinCup q x x = 0

The cup vanishes on parallel spins.

@[simp]

theorem TauCeti.TemperleyLieb.spinCap_true_false {R : Type u_1} [CommRing R] (q : Rˣ) : spinCap q true false = 1

@[simp]

theorem TauCeti.TemperleyLieb.spinCap_false_true {R : Type u_1} [CommRing R] (q : Rˣ) : spinCap q false true = -↑q⁻¹

@[simp]

theorem TauCeti.TemperleyLieb.spinCap_self {R : Type u_1} [CommRing R] (q : Rˣ) (x : Bool) : spinCap q x x = 0

The cap vanishes on parallel spins.

@[simp]

theorem TauCeti.TemperleyLieb.markovWeight_true {R : Type u_1} [CommRing R] (q : Rˣ) : markovWeight q true = -↑q

@[simp]

theorem TauCeti.TemperleyLieb.markovWeight_false {R : Type u_1} [CommRing R] (q : Rˣ) : markovWeight q false = -↑q⁻¹

theorem TauCeti.TemperleyLieb.sum_markovWeight {R : Type u_1} [CommRing R] (q : Rˣ) : ∑ b : Bool, markovWeight q b = -(↑q + ↑q⁻¹)

The spin weights sum to the loop value.

def TauCeti.TemperleyLieb.spinGenerator {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (j k : Fin n) : Matrix (Fin n → Bool) (Fin n → Bool) R

The matrix of a Temperley-Lieb generator in the spin model on n strands: the identity on the strands other than j and k, tensored with the rank-one matrix cup ⊗ cap on the strands j and k. Its entry at the spin configurations s and t is cup (s j, s k) * cap (t j, t k) when s and t agree off j and k, and 0 otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.TemperleyLieb.spinGenerator_apply {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (j k : Fin n) (s t : Fin n → Bool) : spinGenerator q j k s t = if ∀ l ∉ {j, k}, s l = t l then spinCup q (s j) (s k) * spinCap q (t j) (t k) else 0

theorem TauCeti.TemperleyLieb.spinGenerator_mul_apply {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k : Fin n} (hjk : j ≠ k) (X : Matrix (Fin n → Bool) (Fin n → Bool) R) (s u : Fin n → Bool) : (spinGenerator q j k * X) s u = spinCup q (s j) (s k) * ∑ b : Bool, ∑ c : Bool, spinCap q b c * X (Function.update (Function.update s j b) k c) u

Left multiplication by a generator matrix caps the strands j and k of the row index: the row s of the product is cup (s j, s k) times the cap-weighted sum of the rows of X at the configurations obtained from s by resetting the spins on j and k.

theorem TauCeti.TemperleyLieb.spinGenerator_update_update_apply {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k : Fin n} (hjk : j ≠ k) (s u : Fin n → Bool) (b c : Bool) : spinGenerator q j k (Function.update (Function.update s j b) k c) u = if ∀ l ∉ {j, k}, s l = u l then spinCup q b c * spinCap q (u j) (u k) else 0

A generator matrix does not see the row spins on the strands it caps, except through the cup.

theorem TauCeti.TemperleyLieb.spinGenerator_mul_self {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k : Fin n} (hjk : j ≠ k) : spinGenerator q j k * spinGenerator q j k = -(↑q + ↑q⁻¹) • spinGenerator q j k

Closing a loop multiplies a generator matrix by the loop value -(q + q⁻¹).

theorem TauCeti.TemperleyLieb.spinGenerator_zigzag_left {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k l : Fin n} (hjk : j ≠ k) (hkl : k ≠ l) (hjl : j ≠ l) : spinGenerator q j k * spinGenerator q k l * spinGenerator q j k = spinGenerator q j k

The zigzag relation for two generator matrices sharing the strand k, with the first one on the left.

theorem TauCeti.TemperleyLieb.spinGenerator_zigzag_right {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k l : Fin n} (hjk : j ≠ k) (hkl : k ≠ l) (hjl : j ≠ l) : spinGenerator q k l * spinGenerator q j k * spinGenerator q k l = spinGenerator q k l

The zigzag relation for two generator matrices sharing the strand k, with the second one on the left.

theorem TauCeti.TemperleyLieb.spinGenerator_mul_spinGenerator_comm {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k l m : Fin n} (hjk : j ≠ k) (hlm : l ≠ m) (hjl : j ≠ l) (hjm : j ≠ m) (hkl : k ≠ l) (hkm : k ≠ m) : spinGenerator q j k * spinGenerator q l m = spinGenerator q l m * spinGenerator q j k

Generator matrices on disjoint pairs of strands commute.

def TauCeti.TemperleyLieb.spinRep {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) : TemperleyLieb R δ n →ₐ[R] Matrix (Fin n → Bool) (Fin n → Bool) R

The spin representation of the Temperley-Lieb algebra on n strands with loop value δ = -(q + q⁻¹): the generator e i acts by the generator matrix on the strands i and i + 1.

Equations

• TauCeti.TemperleyLieb.spinRep q hδ = TauCeti.TemperleyLieb.lift (fun (i : Fin (n - 1)) => TauCeti.TemperleyLieb.spinGenerator q ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TemperleyLieb.spinRep_e {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (i : Fin (n - 1)) : (spinRep q hδ) (e δ i) = spinGenerator q ⟨↑i, ⋯⟩ ⟨↑i + 1, ⋯⟩

The spin representation sends the generator e i to the generator matrix on the strands i and i + 1.

def TauCeti.TemperleyLieb.spinWeight {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (s : Fin n → Bool) : R

The weight of a spin configuration in the Markov trace: the product of the weights of its spins.

Equations

• TauCeti.TemperleyLieb.spinWeight q s = ∏ l : Fin n, TauCeti.TemperleyLieb.markovWeight q (s l)

theorem TauCeti.TemperleyLieb.spinWeight_eq_of_forall_notMem {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {j k : Fin n} {s t : Fin n → Bool} (h : ∀ l ∉ {j, k}, s l = t l) (hs : s j ≠ s k) (ht : t j ≠ t k) : spinWeight q s = spinWeight q t

Two configurations that agree away from the strands j and k and are antiparallel on them have the same weight: each carries one spin true and one spin false on these two strands.

theorem TauCeti.TemperleyLieb.diagonal_spinWeight_mul_spinGenerator {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} (j k : Fin n) : Matrix.diagonal (spinWeight q) * spinGenerator q j k = spinGenerator q j k * Matrix.diagonal (spinWeight q)

A generator matrix commutes with the weight matrix: it only exchanges the two antiparallel configurations of the strands it caps.

theorem TauCeti.TemperleyLieb.commute_diagonal_spinWeight_spinRep {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (x : TemperleyLieb R δ n) : Commute (Matrix.diagonal (spinWeight q)) ((spinRep q hδ) x)

The image of the spin representation commutes with the weight matrix.

@[simp]

theorem TauCeti.TemperleyLieb.spinWeight_snoc {R : Type u_1} [CommRing R] (q : Rˣ) {m : ℕ} (s : Fin m → Bool) (c : Bool) : spinWeight q (Fin.snoc s c) = spinWeight q s * markovWeight q c

The weight of a configuration with one more spin.

@[simp]

theorem TauCeti.TemperleyLieb.spinGenerator_castSucc {R : Type u_1} [CommRing R] (q : Rˣ) {m : ℕ} (j k : Fin m) : spinGenerator q j.castSucc k.castSucc = Matrix.extendLast (spinGenerator q j k)

A generator matrix on strands that do not include the last one is extended from fewer strands.

theorem TauCeti.TemperleyLieb.trace_diagonal_spinWeight_mul_extendLast {R : Type u_1} [CommRing R] (q : Rˣ) {m : ℕ} (X : Matrix (Fin m → Bool) (Fin m → Bool) R) : (Matrix.diagonal (spinWeight q) * Matrix.extendLast X).trace = (∑ c : Bool, markovWeight q c) * (Matrix.diagonal (spinWeight q) * X).trace

Weighted trace of an extended matrix: the added strand contributes the sum of the spin weights.

theorem TauCeti.TemperleyLieb.trace_diagonal_spinWeight_mul_extendLast_mul_spinGenerator {R : Type u_1} [CommRing R] (q : Rˣ) {m : ℕ} (X : Matrix (Fin (m + 1) → Bool) (Fin (m + 1) → Bool) R) : (Matrix.diagonal (spinWeight q) * (Matrix.extendLast X * spinGenerator q (Fin.last m).castSucc (Fin.last (m + 1)))).trace = (Matrix.diagonal (spinWeight q) * X).trace

The weighted partial trace over the added strand of an extended matrix composed with the generator matrix capping the added strand with the previous one recovers the weighted trace of the original matrix.

def TauCeti.TemperleyLieb.markovTrace {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) : TemperleyLieb R δ n →ₗ[R] R

The Markov trace on the Temperley-Lieb algebra on n strands with loop value δ = -(q + q⁻¹): the trace of the spin representation weighted by TauCeti.TemperleyLieb.spinWeight. It is normalized by markovTrace q hδ 1 = δ ^ n, one factor of δ for each of the n loops in the closure of the identity diagram.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.TemperleyLieb.markovTrace_apply {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (x : TemperleyLieb R δ n) : (markovTrace q hδ) x = (Matrix.diagonal (spinWeight q) * (spinRep q hδ) x).trace

The Markov trace is the weighted trace of the spin representation.

@[simp]

theorem TauCeti.TemperleyLieb.markovTrace_one {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) : (markovTrace q hδ) 1 = δ ^ n

The Markov trace of the identity on n strands, whose closure is n loops, is δ ^ n.

theorem TauCeti.TemperleyLieb.markovTrace_mul_comm {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (x y : TemperleyLieb R δ n) : (markovTrace q hδ) (x * y) = (markovTrace q hδ) (y * x)

The trace property of the Markov trace.

@[simp]

theorem TauCeti.TemperleyLieb.spinRep_strandIncl {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (x : TemperleyLieb R δ (n + 1)) : (spinRep q hδ) (strandIncl x) = Matrix.extendLast ((spinRep q hδ) x)

The spin representation intertwines adding a straight strand with extendLast.

@[simp]

theorem TauCeti.TemperleyLieb.markovTrace_strandIncl {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (x : TemperleyLieb R δ (n + 1)) : (markovTrace q hδ) (strandIncl x) = δ * (markovTrace q hδ) x

Adding a straight strand multiplies the Markov trace by the loop value: the new strand closes up to one more loop.

@[simp]

theorem TauCeti.TemperleyLieb.markovTrace_strandIncl_mul_e_last {R : Type u_1} [CommRing R] (q : Rˣ) {n : ℕ} {δ : R} (hδ : δ = -(↑q + ↑q⁻¹)) (x : TemperleyLieb R δ (n + 1)) : (markovTrace q hδ) (strandIncl x * e δ (Fin.last n)) = (markovTrace q hδ) x

The Markov property: capping the added last strand with the previous one does not change the Markov trace, the closure of the cap being isotopic to a straight strand.