The Temperley-Lieb algebra

The Temperley-Lieb algebra TemperleyLieb R δ n on n strands, over a commutative semiring R and with loop value δ : R, is the associative unital R-algebra on generators e 0, …, e (n - 2) subject to

• e i * e i = δ • e i,
• e i * e j * e i = e i when the two generators share a strand, that is |i - j| = 1, and
• e i * e j = e j * e i when they are disjoint, that is |i - j| ≥ 2.

Geometrically e i is the planar tangle that caps off the strands i and i + 1 at the top and at the bottom, the first relation records that closing a loop multiplies by δ, and the second records the isotopy that straightens a zig-zag.

The algebra is built here as a quotient of the free algebra by the relations, which is what makes the universal property TauCeti.TemperleyLieb.lift available: an assignment of the generators satisfying the three relations extends uniquely to an algebra map out of TemperleyLieb R δ n. That universal property is the whole point of the construction.

Indexing convention

TemperleyLieb R δ n is indexed by the number n of strands, so its generators are indexed by Fin (n - 1). In particular TemperleyLieb R δ 0 and TemperleyLieb R δ 1 are the base ring R (TauCeti.TemperleyLieb.algEquivOfLeOne), and the adjacency relation is vacuous for n ≤ 2.

Non-degeneracy

A presentation is only worth having if it does not collapse. Two theorems here rule that out: the base ring embeds (TauCeti.TemperleyLieb.algebraMap_injective, from the augmentation killing every generator), the generator of the two-strand algebra is nonzero over a nontrivial base ring (TauCeti.TemperleyLieb.e_ne_zero_two, from an explicit two-dimensional representation). The latter assumes [Nontrivial R], as it must: over the zero ring the whole algebra is zero.

That e i ≠ 0 for every n over a nontrivial base ring — indeed that TemperleyLieb R δ n is free of rank the Catalan number catalan n on the planar-matching diagrams, so that TL_1 has basis 1 and TL_2 has basis 1, e 0 — is the fundamental structure theorem of the algebra, and it is not proved here: it needs the diagram basis, which is a separate construction. The two-strand case above is the part of it that the presentation alone can see.

Main definitions

• TauCeti.TemperleyLieb.Rel: the three defining relations, as a relation on the free algebra.
• TauCeti.TemperleyLieb: the Temperley-Lieb algebra on n strands with loop value δ.
• TauCeti.TemperleyLieb.e: the generators.
• TauCeti.TemperleyLieb.lift: the universal property.
• TauCeti.TemperleyLieb.strandIncl: the inclusion adding a straight last strand.
• TauCeti.TemperleyLieb.aug: the augmentation killing every generator.
• TauCeti.TemperleyLieb.algEquivOfLeOne: the algebra on at most one strand is the base ring.
• TauCeti.TemperleyLieb.crossing: the Kauffman-bracket expansion α • 1 + β • e i of a crossing.

Main results

• TauCeti.TemperleyLieb.e_mul_self, TauCeti.TemperleyLieb.e_mul_e_mul_e and TauCeti.TemperleyLieb.commute_e: the three defining relations.
• TauCeti.TemperleyLieb.lift_e and TauCeti.TemperleyLieb.hom_ext: the computation rule and uniqueness half of the universal property.
• TauCeti.TemperleyLieb.adjoin_range_e: the generators generate.
• TauCeti.TemperleyLieb.algebraMap_injective: the base ring embeds.
• TauCeti.TemperleyLieb.crossing_mul_crossing_swap_eq_one and TauCeti.TemperleyLieb.crossing_braid: a crossing is invertible and crossings satisfy the braid relation under their respective scalar hypotheses.
• TauCeti.TemperleyLieb.e_ne_zero_two: non-degeneracy on two strands.

References

• H. N. V. Temperley, E. H. Lieb, Relations between the "percolation" and "colouring" problem …, Proc. Roy. Soc. London Ser. A 322 (1971), 251-280.
• V. F. R. Jones, A polynomial invariant for knots via von Neumann algebras, Bull. Amer. Math. Soc. 12 (1985), 103-111.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 3 (the Kauffman bracket and Jones polynomial).
• L. H. Kauffman, State models and the Jones polynomial, Topology 26 (1987), 395-407.
• The quotient presentation and universal-property API follow the construction pattern in Mathlib.LinearAlgebra.CliffordAlgebra.Basic.

inductive TauCeti.TemperleyLieb.Rel (R : Type u_1) (δ : R) (n : ℕ) [CommSemiring R] : FreeAlgebra R (Fin (n - 1)) → FreeAlgebra R (Fin (n - 1)) → Prop

The defining relations of the Temperley-Lieb algebra on n strands with loop value δ, as a relation on the free algebra over the generators Fin (n - 1): a generator is idempotent up to δ, two generators sharing a strand satisfy e i * e j * e i = e i, and two disjoint generators commute.

• mul_self {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (i : Fin (n - 1)) : Rel R δ n (FreeAlgebra.ι R i * FreeAlgebra.ι R i) (δ • FreeAlgebra.ι R i)
• adjacent {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : Rel R δ n (FreeAlgebra.ι R i * FreeAlgebra.ι R j * FreeAlgebra.ι R i) (FreeAlgebra.ι R i)
• distant {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : Rel R δ n (FreeAlgebra.ι R i * FreeAlgebra.ι R j) (FreeAlgebra.ι R j * FreeAlgebra.ι R i)

def TauCeti.TemperleyLieb (R : Type u_1) (δ : R) (n : ℕ) [CommSemiring R] : Type u_1

The Temperley-Lieb algebra on n strands over R with loop value δ: the free R-algebra on Fin (n - 1) modulo TauCeti.TemperleyLieb.Rel.

Equations

• TauCeti.TemperleyLieb R δ n = RingQuot (TauCeti.TemperleyLieb.Rel R δ n)

@[instance_reducible]

instance TauCeti.instSemiringTemperleyLieb (R : Type u_1) (δ : R) (n : ℕ) [CommSemiring R] : Semiring (TemperleyLieb R δ n)

Equations

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

@[instance_reducible]

instance TauCeti.instRingTemperleyLieb {S : Type u_2} [CommRing S] (ε : S) (m : ℕ) : Ring (TemperleyLieb S ε m)

Equations

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

@[instance_reducible]

instance TauCeti.instAlgebraTemperleyLieb (R : Type u_1) (δ : R) (n : ℕ) [CommSemiring R] : Algebra R (TemperleyLieb R δ n)

Equations

• TauCeti.instAlgebraTemperleyLieb R δ n = { smul := TauCeti.instAlgebraTemperleyLieb._aux_1 R δ n, algebraMap := TauCeti.instAlgebraTemperleyLieb._aux_3 R δ n, commutes' := ⋯, smul_def' := ⋯ }

def TauCeti.TemperleyLieb.mkAlgHom (R : Type u_1) (δ : R) (n : ℕ) [CommSemiring R] : FreeAlgebra R (Fin (n - 1)) →ₐ[R] TemperleyLieb R δ n

The quotient map from the free algebra to the Temperley-Lieb algebra.

Equations

• TauCeti.TemperleyLieb.mkAlgHom R δ n = RingQuot.mkAlgHom R (TauCeti.TemperleyLieb.Rel R δ n)

def TauCeti.TemperleyLieb.e {R : Type u_1} (δ : R) {n : ℕ} [CommSemiring R] (i : Fin (n - 1)) : TemperleyLieb R δ n

The generator e i of the Temperley-Lieb algebra, the planar tangle capping off the strands i and i + 1 at the top and at the bottom.

Equations

• TauCeti.TemperleyLieb.e δ i = (TauCeti.TemperleyLieb.mkAlgHom R δ n) (FreeAlgebra.ι R i)

@[simp]

theorem TauCeti.TemperleyLieb.mkAlgHom_ι {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (i : Fin (n - 1)) : (mkAlgHom R δ n) (FreeAlgebra.ι R i) = e δ i

The quotient map takes each free-algebra generator to the corresponding Temperley-Lieb generator.

theorem TauCeti.TemperleyLieb.mkAlgHom_surjective {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] : Function.Surjective ⇑(mkAlgHom R δ n)

Every element of the Temperley-Lieb algebra is represented by a free-algebra element.

theorem TauCeti.TemperleyLieb.mkAlgHom_rel {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {x y : FreeAlgebra R (Fin (n - 1))} (h : Rel R δ n x y) : (mkAlgHom R δ n) x = (mkAlgHom R δ n) y

Related elements of the free algebra have the same image in the Temperley-Lieb algebra.

@[simp]

theorem TauCeti.TemperleyLieb.e_mul_self {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (i : Fin (n - 1)) : e δ i * e δ i = δ • e δ i

A generator is idempotent up to the loop value: closing a loop multiplies by δ.

theorem TauCeti.TemperleyLieb.e_mul_e_mul_e {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : e δ i * e δ j * e δ i = e δ i

Two generators sharing a strand straighten a zig-zag.

theorem TauCeti.TemperleyLieb.commute_e {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : Commute (e δ i) (e δ j)

Two disjoint generators commute.

def TauCeti.TemperleyLieb.lift {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (f : Fin (n - 1) → A) (hself : ∀ (i : Fin (n - 1)), f i * f i = δ • f i) (hadj : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → f i * f j * f i = f i) (hdist : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → f i * f j = f j * f i) : TemperleyLieb R δ n →ₐ[R] A

The universal property of the Temperley-Lieb presentation: a family in an R-algebra satisfying the three defining relations extends to an algebra map out of TemperleyLieb R δ n.

Equations

• TauCeti.TemperleyLieb.lift f hself hadj hdist = (RingQuot.liftAlgHom R) ⟨(FreeAlgebra.lift R) f, ⋯⟩

@[simp]

theorem TauCeti.TemperleyLieb.lift_e {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] (f : Fin (n - 1) → A) (hself : ∀ (i : Fin (n - 1)), f i * f i = δ • f i) (hadj : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → f i * f j * f i = f i) (hdist : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → f i * f j = f j * f i) (i : Fin (n - 1)) : (lift f hself hadj hdist) (e δ i) = f i

The algebra map built by TauCeti.TemperleyLieb.lift takes each generator to its prescribed value.

theorem TauCeti.TemperleyLieb.hom_ext {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {F G : TemperleyLieb R δ n →ₐ[R] A} (h : ∀ (i : Fin (n - 1)), F (e δ i) = G (e δ i)) : F = G

Two algebra maps out of the Temperley-Lieb algebra agreeing on the generators are equal.

theorem TauCeti.TemperleyLieb.hom_ext_iff {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {A : Type u_2} [Semiring A] [Algebra R A] {F G : TemperleyLieb R δ n →ₐ[R] A} : F = G ↔ ∀ (i : Fin (n - 1)), F (e δ i) = G (e δ i)

theorem TauCeti.TemperleyLieb.adjoin_range_e {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] : Algebra.adjoin R (Set.range (e δ)) = ⊤

The generators generate.

def TauCeti.TemperleyLieb.strandIncl {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] : TemperleyLieb R δ (n + 1) →ₐ[R] TemperleyLieb R δ (n + 2)

The algebra map from TemperleyLieb R δ (n + 1) to TemperleyLieb R δ (n + 2) that adds a last strand and leaves it straight: each generator is sent to the generator of the same index, and the new strand is never capped. This is the inclusion along which the Markov property of a trace is stated.

Equations

• TauCeti.TemperleyLieb.strandIncl = TauCeti.TemperleyLieb.lift (fun (i : Fin n) => TauCeti.TemperleyLieb.e δ i.castSucc) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TemperleyLieb.strandIncl_e {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (i : Fin n) : strandIncl (e δ i) = e δ i.castSucc

The strand inclusion sends each generator to the generator of the same index.

def TauCeti.TemperleyLieb.aug {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] : TemperleyLieb R δ n →ₐ[R] R

The augmentation of the Temperley-Lieb algebra, killing every generator. It is a retraction of the structure map, so it witnesses that the presentation does not collapse the base ring.

Equations

• TauCeti.TemperleyLieb.aug = TauCeti.TemperleyLieb.lift (fun (x : Fin (n - 1)) => 0) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TemperleyLieb.aug_e {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (i : Fin (n - 1)) : aug (e δ i) = 0

The augmentation kills every generator.

theorem TauCeti.TemperleyLieb.algebraMap_injective {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] : Function.Injective ⇑(algebraMap R (TemperleyLieb R δ n))

The base ring embeds into the Temperley-Lieb algebra.

instance TauCeti.TemperleyLieb.instNontrivial {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] [Nontrivial R] : Nontrivial (TemperleyLieb R δ n)

def TauCeti.TemperleyLieb.algEquivOfLeOne {R : Type u_1} (δ : R) {n : ℕ} [CommSemiring R] (h : n ≤ 1) : TemperleyLieb R δ n ≃ₐ[R] R

On at most one strand there are no generators, so the Temperley-Lieb algebra is the base ring. This matches the triviality of TauCeti.BraidGroup 0 and TauCeti.BraidGroup 1.

Equations

• TauCeti.TemperleyLieb.algEquivOfLeOne δ h = AlgEquiv.ofAlgHom TauCeti.TemperleyLieb.aug (Algebra.ofId R (TauCeti.TemperleyLieb R δ n)) ⋯ ⋯

@[simp]

theorem TauCeti.TemperleyLieb.algEquivOfLeOne_apply {R : Type u_1} (δ : R) {n : ℕ} [CommSemiring R] (h : n ≤ 1) (x : TemperleyLieb R δ n) : (algEquivOfLeOne δ h) x = aug x

On at most one strand, the forward map of algEquivOfLeOne is the augmentation.

@[simp]

theorem TauCeti.TemperleyLieb.algEquivOfLeOne_symm_apply {R : Type u_1} (δ : R) {n : ℕ} [CommSemiring R] (h : n ≤ 1) (r : R) : (algEquivOfLeOne δ h).symm r = (algebraMap R (TemperleyLieb R δ n)) r

On at most one strand, the inverse of algEquivOfLeOne is the algebra structure map.

def TauCeti.TemperleyLieb.twoStrandRep {R : Type u_1} (δ : R) [CommSemiring R] : TemperleyLieb R δ 2 →ₐ[R] Matrix (Fin 2) (Fin 2) R

A two-dimensional representation of the two-strand Temperley-Lieb algebra. On two strands there is a single generator and the adjacency and distance relations are vacuous, so the sole condition to check is that the matrix be idempotent up to δ.

Equations

• TauCeti.TemperleyLieb.twoStrandRep δ = TauCeti.TemperleyLieb.lift (fun (x : Fin (2 - 1)) => TauCeti.TemperleyLieb.twoStrandMatrix✝ δ) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.TemperleyLieb.twoStrandRep_e {R : Type u_1} (δ : R) [CommSemiring R] (i : Fin (2 - 1)) : (twoStrandRep δ) (e δ i) = !![0, 0; 1, δ]

The two-dimensional representation takes the single generator to the two-strand matrix.

theorem TauCeti.TemperleyLieb.e_ne_zero_two {R : Type u_1} {δ : R} [CommSemiring R] [Nontrivial R] (i : Fin (2 - 1)) : e δ i ≠ 0

The generator of the two-strand Temperley-Lieb algebra is nonzero: the presentation does not collapse.

def TauCeti.TemperleyLieb.crossing {R : Type u_1} (δ : R) {n : ℕ} [CommSemiring R] (α β : R) (i : Fin (n - 1)) : TemperleyLieb R δ n

The Kauffman-bracket expansion α • 1 + β • e i of a crossing: α times the identity tangle plus β times the tangle that caps off the two strands.

Equations

• TauCeti.TemperleyLieb.crossing δ α β i = α • 1 + β • TauCeti.TemperleyLieb.e δ i

@[simp]

theorem TauCeti.TemperleyLieb.crossing_def {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (α β : R) (i : Fin (n - 1)) : crossing δ α β i = α • 1 + β • e δ i

A crossing is the indicated linear combination of the identity and one generator.

theorem TauCeti.TemperleyLieb.crossing_mul_crossing {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (x y z w : R) (i j : Fin (n - 1)) : crossing δ x y i * crossing δ z w j = (x * z) • 1 + (x * w) • e δ j + (y * z) • e δ i + (y * w) • (e δ i * e δ j)

The product of two crossings, expanded in the four terms 1, e i, e j, e i * e j.

theorem TauCeti.TemperleyLieb.crossing_mul_crossing_comm {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] (x y z w : R) {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : crossing δ x y i * crossing δ z w j = crossing δ z w j * crossing δ x y i

Crossings with arbitrary coefficients on disjoint pairs of strands commute.

theorem TauCeti.TemperleyLieb.crossing_mul_crossing_swap_eq_one_of_polynomial {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {α β : R} (hαβ : α * β = 1) (hpoly : α ^ 2 + α * β * δ + β ^ 2 = 0) (i : Fin (n - 1)) : crossing δ α β i * crossing δ β α i = 1

Swapping the two coefficients inverts a crossing when the coefficients are inverse and obey the indicated polynomial relation with the loop value.

theorem TauCeti.TemperleyLieb.crossing_mul_crossing_mul_crossing {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {α β : R} {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : crossing δ α β i * crossing δ α β j * crossing δ α β i = α ^ 3 • 1 + (2 * α ^ 2 * β + α * β ^ 2 * δ + β ^ 3) • e δ i + (α ^ 2 * β) • e δ j + (α * β ^ 2) • (e δ i * e δ j) + (α * β ^ 2) • (e δ j * e δ i)

The triple product of crossings on two adjacent pairs of strands, reduced using the Temperley-Lieb relations to a linear combination of five standard monomials.

theorem TauCeti.TemperleyLieb.crossing_braid {R : Type u_1} {δ : R} {n : ℕ} [CommSemiring R] {β α : R} (hpoly : β * (α ^ 2 + α * β * δ + β ^ 2) = 0) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : crossing δ α β i * crossing δ α β j * crossing δ α β i = crossing δ α β j * crossing δ α β i * crossing δ α β j

Crossings on two strands sharing a strand satisfy the braid relation when their coefficients obey the natural polynomial relation.

theorem TauCeti.TemperleyLieb.crossing_mul_crossing_swap_eq_one {R : Type u_1} {δ : R} {n : ℕ} [CommRing R] {α β : R} (hαβ : α * β = 1) (hδ : δ = -(α ^ 2 + β ^ 2)) (i : Fin (n - 1)) : crossing δ α β i * crossing δ β α i = 1

Swapping the two coefficients inverts a crossing, provided the coefficients are inverse to one another and the loop value is -(α ^ 2 + β ^ 2).