Documentation

TauCeti.Algebra.TypeAHeckeAlgebra.SignedCheckedR

The signed checked R-matrix on word spaces #

Let ι be a linearly ordered alphabet in which every letter is designated positive or negative (by a decidable predicate pos), and let s be an element of a commutative ring R; put Q = s ^ 2, so that in the positive-real setting s = √Q. The signed checked R-matrix acts on two strands j and k of a basis word w of the word space (Fin n → ι) →₀ R, depending only on the letters a = w j and b = w k:

On a two-letter block {a ⊗ b, b ⊗ a} with a < b its matrix is [[Q - 1, -s], [-s, 0]]. Write X = TauCeti.signedCheckedR pos s j k. It satisfies the quadratic relation (X - Q) (X + 1) = 0, so over a field its eigenvalues lie among Q and -1; operators on disjoint pairs of strands commute; and operators on two pairs sharing a strand satisfy the braid relation. These identities hold for every s, so the adjacent operators satisfy the defining relations of the type-A Hecke algebra in the normalization gᵢ = s Tᵢ, (gᵢ - Q) (gᵢ + 1) = 0. When s is a unit they are invertible and define a braid group representation TauCeti.signedCheckedRep, and the rescaled operators s⁻¹ • X satisfy the quadratic relation T * T = (s - s⁻¹) • T + 1 in the convention (Tᵢ - s) (Tᵢ + s⁻¹) = 0.

The matrix of the operator in the word basis is symmetric, the algebraic form of its self-adjointness for real s on the Hilbert space with this orthonormal basis. The atomic tensor models of Markov traces on the Hecke algebras with a positive real parameter are built from these operators, on ordered alphabets of positive and negative letters that also carry weights.

If every letter is positive, reversing the order of the alphabet turns the operator into a rescaled Jimbo R-matrix at the parameter -s: X = (-s) • T_{-s} on ιᵒᵈ (TauCeti.signedCheckedR_eq_jimboGenerator). Negative letters have no such description; signed alphabets of this kind arise from the vector representation of the quantum supergroup U_q(gl(m|n)).

Main definitions #

Main results #

References #

noncomputable def TauCeti.signedCheckedR {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) (j k : Fin n) :
Module.End R ((Fin n → ι) →₀ R)

The signed checked R-matrix acting on the strands j and k of the word space (Fin n → ι) →₀ R, with Q = s ^ 2. On a basis word w it multiplies w by Q if w j = w k is positive and by -1 if it is negative; it sends w to (Q - 1) • w - s • w' if w j < w k, and to -(s • w') if w k < w j, where w' exchanges the letters at j and k.

Instances For
    @[simp]
    theorem TauCeti.signedCheckedR_single_one {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) (j k : Fin n) (w : Fin n → ι) :
    (signedCheckedR pos s j k) (Finsupp.single w 1) = if w j = w k then (if pos (w j) then s ^ 2 else -1) • Finsupp.single w 1 else if w j < w k then (s ^ 2 - 1) • Finsupp.single w 1 - s • Finsupp.single (w ∘ ⇑(Equiv.swap j k)) 1 else -(s • Finsupp.single (w ∘ ⇑(Equiv.swap j k)) 1)

    The value of the signed checked R-matrix on a basis word.

    theorem TauCeti.signedCheckedR_single_update_update {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) {j k : Fin n} (hjk : j ≠ k) (w : Fin n → ι) (x y : ι) :

    The value of the signed checked R-matrix on the strands j and k on a basis word whose letters at j and k are x and y.

    theorem TauCeti.signedCheckedR_mul_self {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) (j k : Fin n) :
    signedCheckedR pos s j k * signedCheckedR pos s j k = (s ^ 2 - 1) • signedCheckedR pos s j k + s ^ 2 • 1

    The quadratic relation X * X = (Q - 1) • X + Q • 1, Q = s ^ 2, of the signed checked R-matrix, that is (X - Q) (X + 1) = 0; over a field its eigenvalues lie among Q and -1.

    theorem TauCeti.signedCheckedR_mul_comm {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) {j k l m : Fin n} (h : [j, k, l, m].Nodup) :
    signedCheckedR pos s j k * signedCheckedR pos s l m = signedCheckedR pos s l m * signedCheckedR pos s j k

    Signed checked R-matrices on disjoint pairs of strands commute.

    theorem TauCeti.signedCheckedR_braid {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) {j k l : Fin n} (hjk : j ≠ k) (hkl : k ≠ l) (hjl : j ≠ l) :
    signedCheckedR pos s j k * signedCheckedR pos s k l * signedCheckedR pos s j k = signedCheckedR pos s k l * signedCheckedR pos s j k * signedCheckedR pos s k l

    The braid relation for signed checked R-matrices on two pairs of strands sharing the strand k, the Yang-Baxter equation for the signed checked R-matrix.

    theorem TauCeti.signedCheckedR_single_apply_comm {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) (j k : Fin n) (v w : Fin n → ι) :
    ((signedCheckedR pos s j k) (Finsupp.single w 1)) v = ((signedCheckedR pos s j k) (Finsupp.single v 1)) w

    The matrix of the signed checked R-matrix in the word basis is symmetric: the coefficient of v in the image of w is the coefficient of w in the image of v. For real s this is the self-adjointness of the operator for the inner product in which the words are orthonormal.

    theorem TauCeti.signedCheckedR_apply {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) (j k : Fin n) (v : (Fin n → ι) →₀ R) (u : Fin n → ι) :
    ((signedCheckedR pos s j k) v) u = if u j = u k then (if pos (u j) then s ^ 2 else -1) * v u else if u j < u k then (s ^ 2 - 1) * v u - s * v (u ∘ ⇑(Equiv.swap j k)) else -(s * v (u ∘ ⇑(Equiv.swap j k)))

    The coefficient of a word u in the image of an arbitrary vector v under the signed checked R-matrix. Since the matrix is symmetric, it only involves the coefficients of v at u and at the word u ∘ Equiv.swap j k exchanging the letters at j and k.

    theorem TauCeti.signedCheckedR_comp_lmapDomain {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n m : ℕ} (s : R) {f : Fin m → Fin n} (E : (Fin m → ι) → Fin n → ι) (hE : ∀ (u : Fin m → ι) (i : Fin m), E u (f i) = u i) (j k : Fin m) (hswap : ∀ (u : Fin m → ι), E u ∘ ⇑(Equiv.swap (f j) (f k)) = E (u ∘ ⇑(Equiv.swap j k))) :

    Locality of the signed checked R-matrix. Let E embed the words on m strands into the words on n strands along the strand map f, so that E u carries the letter u i at the strand f i, and suppose that E intertwines the exchange of the strands j and k with that of f j and f k. Then E intertwines the signed checked R-matrix on the strands j and k with the one on the strands f j and f k.

    theorem TauCeti.signedCheckedR_comp_lmapDomain_snoc {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : R) (j k : Fin n) (a : ι) :
    (signedCheckedR pos s j.castSucc k.castSucc ∘ₗ Finsupp.lmapDomain R R fun (w : Fin n → ι) => Fin.snoc w a) = (Finsupp.lmapDomain R R fun (w : Fin n → ι) => Fin.snoc w a) ∘ₗ signedCheckedR pos s j k

    Appending a letter intertwines the signed checked R-matrix on two strands with the one on the same two strands of the longer words.

    theorem TauCeti.signedCheckedR_castAdd_comp_lmapDomain_append {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n m : ℕ} (s : R) (j k : Fin m) (v : Fin n → ι) :
    (signedCheckedR pos s (Fin.castAdd n j) (Fin.castAdd n k) ∘ₗ Finsupp.lmapDomain R R fun (u : Fin m → ι) => Fin.append u v) = (Finsupp.lmapDomain R R fun (u : Fin m → ι) => Fin.append u v) ∘ₗ signedCheckedR pos s j k

    Appending a word of n letters on the right intertwines the signed checked R-matrix on two strands with the one on the same two strands of the longer words.

    theorem TauCeti.signedCheckedR_natAdd_comp_lmapDomain_append {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n m : ℕ} (s : R) (j k : Fin n) (u : Fin m → ι) :
    (signedCheckedR pos s (Fin.natAdd m j) (Fin.natAdd m k) ∘ₗ Finsupp.lmapDomain R R fun (v : Fin n → ι) => Fin.append u v) = (Finsupp.lmapDomain R R fun (v : Fin n → ι) => Fin.append u v) ∘ₗ signedCheckedR pos s j k

    Prepending a word of m letters on the left intertwines the signed checked R-matrix on two strands with the one on the corresponding two strands of the longer words.

    theorem TauCeti.commute_productDensity_signedCheckedR {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (p : ι → R) (s : R) (j k : Fin n) :

    The product density commutes with the signed checked R-matrix on any two strands, which only permutes the letters of a word.

    theorem TauCeti.signedCheckedR_mul_smul_add {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (j k : Fin n) :
    signedCheckedR pos (↑s) j k * ↑s⁻¹ ^ 2 • (signedCheckedR pos (↑s) j k + (1 - ↑s ^ 2) • 1) = 1

    The signed checked R-matrix is invertible when s is a unit, with right inverse s⁻¹ ^ 2 • (X + (1 - Q) • 1).

    theorem TauCeti.smul_add_mul_signedCheckedR {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (j k : Fin n) :
    ↑s⁻¹ ^ 2 • (signedCheckedR pos (↑s) j k + (1 - ↑s ^ 2) • 1) * signedCheckedR pos (↑s) j k = 1

    The signed checked R-matrix is invertible when s is a unit, with left inverse s⁻¹ ^ 2 • (X + (1 - Q) • 1).

    theorem TauCeti.inv_smul_signedCheckedR_mul_self {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (j k : Fin n) :
    ↑s⁻¹ • signedCheckedR pos (↑s) j k * ↑s⁻¹ • signedCheckedR pos (↑s) j k = (↑s - ↑s⁻¹) • ↑s⁻¹ • signedCheckedR pos (↑s) j k + 1

    The Hecke normalization. For a unit s, the rescaled operator T = s⁻¹ • X satisfies the type-A Hecke quadratic relation T * T = (s - s⁻¹) • T + 1, equivalently (T - s) * (T + s⁻¹) = 0.

    noncomputable def TauCeti.signedCheckedRUnit {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (i : Fin (n - 1)) :
    (Module.End R ((Fin n → ι) →₀ R))ˣ

    The signed checked R-matrix on the two strands crossed by the elementary braid σ i, as a unit, with inverse s⁻¹ ^ 2 • (X + (1 - Q) • 1).

    Instances For
      @[simp]
      theorem TauCeti.signedCheckedRUnit_val {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (i : Fin (n - 1)) :

      The value of the unit TauCeti.signedCheckedRUnit.

      @[simp]
      theorem TauCeti.signedCheckedRUnit_inv_val {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (i : Fin (n - 1)) :
      ↑(signedCheckedRUnit pos s i)⁻¹ = ↑s⁻¹ ^ 2 • (signedCheckedR pos (↑s) (BraidGroup.strand i) (BraidGroup.strandSucc i) + (1 - ↑s ^ 2) • 1)

      The value of the inverse of the unit TauCeti.signedCheckedRUnit.

      noncomputable def TauCeti.signedCheckedRep {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) :
      BraidGroup n →* (Module.End R ((Fin n → ι) →₀ R))ˣ

      The signed checked representation of the braid group on the word space (Fin n → ι) →₀ R: the elementary braid σ i acts by the signed checked R-matrix on the strands i and i + 1.

      Instances For
        @[simp]
        theorem TauCeti.signedCheckedRep_sigma {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (i : Fin (n - 1)) :

        The signed checked representation takes the elementary braid σ i to the signed checked R-matrix on the strands i and i + 1.

        theorem TauCeti.signedCheckedR_eq_jimboGenerator {R : Type u_1} [CommRing R] {ι : Type u_2} [LinearOrder ι] (pos : ι → Prop) [DecidablePred pos] {n : ℕ} (s : Rˣ) (hpos : ∀ (a : ι), pos a) (j k : Fin n) :

        Comparison with the Jimbo R-matrix. If every letter is positive, the signed checked R-matrix is the Jimbo R-matrix at the parameter -s, rescaled by -s, on the alphabet with the reversed order: it is the conjugate of (-s) • T_{-s} on (Fin n → ιᵒᵈ) →₀ R by the relabelling of words along ι ≃ ιᵒᵈ.