Documentation

TauCeti.KnotTheory.Burau.OneSubVecMulVec

Braid-group homomorphisms from the matrices 1 - u ⊗ v #

This file constructs a braid-group homomorphism into GL from a family of rank-one perturbations of the identity 1 - vecMulVec (u i) (v i), indexed by the elementary braids, whose pairings have the values occurring in the Burau representation. The calculus of a single such matrix, or of a pair of them, is in TauCeti/LinearAlgebra/Matrix/OneSubVecMulVec.lean; the braid relation in the form indexed by adjacent elementary braids is here, since it is the generator adjacency of Fin (n - 1) that it is phrased in.

Main definitions #

Main results #

source
theorem TauCeti.KnotTheory.one_sub_vecMulVec_braid_of_adjacent {R : Type u_1} {α : Type u_2} {n : ℕ} [CommRing R] [Fintype α] [DecidableEq α] (t : R) (u v : Fin (n - 1) → α → R) (hself : ∀ (i : Fin (n - 1)), v i ⬝ᵥ u i = t + 1) (hforward : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v i ⬝ᵥ u j = -t) (hreverse : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v j ⬝ᵥ u i = -1) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) :
(1 - Matrix.vecMulVec (u i) (v i)) * (1 - Matrix.vecMulVec (u j) (v j)) * (1 - Matrix.vecMulVec (u i) (v i)) = (1 - Matrix.vecMulVec (u j) (v j)) * (1 - Matrix.vecMulVec (u i) (v i)) * (1 - Matrix.vecMulVec (u j) (v j))

The braid relation for two members of a family of rank-one perturbations of the identity indexed by adjacent elementary braids, in the symmetric form: the two possible adjacency orders are covered at once.

source
def TauCeti.KnotTheory.braidHomOfOneSubVecMulVec {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (n : ℕ) (t : Rˣ) (u v : Fin (n - 1) → α → R) (hself : ∀ (i : Fin (n - 1)), v i ⬝ᵥ u i = ↑t + 1) (hcomm : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → v i ⬝ᵥ u j = 0) (hforward : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v i ⬝ᵥ u j = -↑t) (hreverse : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v j ⬝ᵥ u i = -1) :
BraidGroup n →* GL α R

The braid-group homomorphism into GL associated to a family of rank-one perturbations of the identity with the Burau pairings.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.KnotTheory.braidHomOfOneSubVecMulVec_sigma {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (n : ℕ) (t : Rˣ) (u v : Fin (n - 1) → α → R) (hself : ∀ (i : Fin (n - 1)), v i ⬝ᵥ u i = ↑t + 1) (hcomm : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → v i ⬝ᵥ u j = 0) (hforward : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v i ⬝ᵥ u j = -↑t) (hreverse : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v j ⬝ᵥ u i = -1) (i : Fin (n - 1)) :
    (braidHomOfOneSubVecMulVec n t u v hself ⋯ ⋯ ⋯) (BraidGroup.sigma i) = oneSubVecMulVecGL t (u i) (v i) ⋯

    Such a braid-group homomorphism takes an elementary braid to its corresponding unit.

    source
    theorem TauCeti.KnotTheory.det_braidHomOfOneSubVecMulVec {R : Type u_1} {α : Type u_2} [CommRing R] [Fintype α] [DecidableEq α] (n : ℕ) (t : Rˣ) (u v : Fin (n - 1) → α → R) (hself : ∀ (i : Fin (n - 1)), v i ⬝ᵥ u i = ↑t + 1) (hcomm : ∀ {i j : Fin (n - 1)}, ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i → v i ⬝ᵥ u j = 0) (hforward : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v i ⬝ᵥ u j = -↑t) (hreverse : ∀ {i j : Fin (n - 1)}, ↑i + 1 = ↑j → v j ⬝ᵥ u i = -1) (b : BraidGroup n) :
    Matrix.GeneralLinearGroup.det ((braidHomOfOneSubVecMulVec n t u v hself ⋯ ⋯ ⋯) b) = (-t) ^ Multiplicative.toAdd ((ArtinGroup.exponentSum (CoxeterMatrix.A (n - 1))) b)

    The determinant character of a braid-group homomorphism by rank-one perturbations of the identity with the Burau pairings.