The reduced Burau representation

The unreduced Burau representation on Rⁿ fixes the row covector (1, t, ..., t ^ (n - 1)). Its kernel is consequently an invariant submodule of rank n - 1; the action on that kernel is the reduced Burau representation. This file constructs the invariant kernel and the reduced representation over an arbitrary commutative ring at an arbitrary unit, both in the canonical tail-coordinate system and in the basis of Burau columns. The latter is named with the suffix BurauCol to distinguish the two coordinate systems.

For a braid on n + 1 strands, the coefficient of the zeroth coordinate in the invariant covector is 1. The kernel is therefore canonically free on the remaining n coordinates: TauCeti.KnotTheory.reducedBurauSpaceEquiv sends x : Fin n → R to the vector whose tail is x and whose zeroth coordinate is the unique value making the weighted coordinate sum vanish. Transporting the kernel action across this equivalence gives TauCeti.KnotTheory.reducedBurau, a representation on Fin n → R ready for matrix and determinant computations.

In the basis of Burau columns burauCol t i = t • e i - e (i + 1), the action of an elementary braid is given by the elementary reduced Burau matrix TauCeti.KnotTheory.reducedBurauColMatrix t i, which is a rank-one perturbation 1 - vecMulVec (Pi.single i 1) (reducedBurauColRow t i). The pairings burauRow R i ⬝ᵥ burauCol t j feed the rank-one calculus of TauCeti/LinearAlgebra/Matrix/OneSubVecMulVec.lean, yielding the braid relations, the inverse, the determinant -t, and the Iwahori-Hecke quadratic relation.

This is the reduced-representation prerequisite for the braid route to the Alexander polynomial in Layer 4 of the geometric-topology roadmap.

Main definitions

• TauCeti.KnotTheory.geometricCovector: the invariant covector with coordinates t ^ i.
• TauCeti.KnotTheory.ReducedBurauSpace: its kernel.
• TauCeti.KnotTheory.reducedBurauSpaceEquiv: the explicit equivalence (Fin n → R) ≃ₗ ReducedBurauSpace (n + 1) t.
• TauCeti.KnotTheory.burauRepresentation: the unreduced matrix representation read as a module representation.
• TauCeti.KnotTheory.reducedBurauSubrepresentation: its restriction to the invariant kernel.
• TauCeti.KnotTheory.reducedBurau: the reduced representation in free coordinates.
• TauCeti.KnotTheory.reducedBurauCol: the reduced matrix homomorphism in the basis of Burau columns.
• TauCeti.KnotTheory.burauColMatrix: the n × (n - 1) matrix of Burau columns.
• TauCeti.KnotTheory.burauCoordMatrix: an explicit left inverse of burauColMatrix at a unit t.
• TauCeti.KnotTheory.reducedBurauColRow: the pairings of one Burau row against all Burau columns.
• TauCeti.KnotTheory.reducedBurauColMatrix: the reduced Burau matrix of an elementary braid.
• TauCeti.KnotTheory.reducedBurauColGL: an elementary reduced Burau matrix in GL (Fin (n - 1)) R.

Main results

• TauCeti.KnotTheory.geom_vecMul_burauColMatrix_eq_zero and TauCeti.KnotTheory.burauColMatrix_mulVec_burauCoordMatrix_mulVec: the Burau columns lie in and span the invariant kernel reducedBurauSpace.
• TauCeti.KnotTheory.burauMatrix_mul_burauColMatrix: the elementary Burau matrix restricts to the elementary reduced Burau matrix on the span of the Burau columns.
• TauCeti.KnotTheory.burau_mul_burauColMatrix: the corresponding intertwining identity for every braid.
• TauCeti.KnotTheory.reducedBurau_apply_burauColMatrix_mulVec: comparison of the Burau-column and tail-coordinate reduced representations.
• TauCeti.KnotTheory.reducedBurauColMatrix_mul_comm and TauCeti.KnotTheory.reducedBurauColMatrix_braid: the two braid relations for the reduced matrices.
• TauCeti.KnotTheory.det_reducedBurauColMatrix: the determinant of an elementary reduced Burau matrix is -t.
• TauCeti.KnotTheory.reducedBurauColMatrix_mul_self: the Iwahori-Hecke quadratic relation.
• TauCeti.KnotTheory.reducedBurauColMatrix_two and the two TauCeti.KnotTheory.reducedBurauColMatrix_three_* theorems: explicit reduced matrices on two and three strands.

References

• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82, Princeton University Press (1974), Chapter 3.
• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapters 1 and 6.

def TauCeti.KnotTheory.geometricCovector {R : Type u_1} [CommSemiring R] (n : ℕ) (t : R) : (Fin n → R) →ₗ[R] R

The Burau-invariant covector on Rⁿ, with coordinates (1, t, ..., t ^ (n - 1)).

Equations

• TauCeti.KnotTheory.geometricCovector n t = (dotProductBilin R R) fun (i : Fin n) => t ^ ↑i

@[simp]

theorem TauCeti.KnotTheory.geometricCovector_apply {R : Type u_1} [CommSemiring R] (n : ℕ) (t : R) (x : Fin n → R) : (geometricCovector n t) x = ∑ i : Fin n, t ^ ↑i * x i

The invariant covector is the weighted sum of the coordinates.

def TauCeti.KnotTheory.reducedBurauSpace {R : Type u_1} [CommSemiring R] (n : ℕ) (t : R) : Submodule R (Fin n → R)

The invariant submodule carrying the reduced Burau representation: the kernel of the geometric covector.

Equations

• TauCeti.KnotTheory.reducedBurauSpace n t = (TauCeti.KnotTheory.geometricCovector n t).ker

@[reducible, inline]

abbrev TauCeti.KnotTheory.ReducedBurauSpace {R : Type u_1} [CommSemiring R] (n : ℕ) (t : R) : Type u_1

The type underlying the invariant submodule reducedBurauSpace n t.

Equations

• TauCeti.KnotTheory.ReducedBurauSpace n t = ↥(TauCeti.KnotTheory.reducedBurauSpace n t)

@[simp]

theorem TauCeti.KnotTheory.mem_reducedBurauSpace_iff {R : Type u_1} [CommSemiring R] (n : ℕ) (t : R) (x : Fin n → R) : x ∈ reducedBurauSpace n t ↔ ∑ i : Fin n, t ^ ↑i * x i = 0

Membership in the reduced Burau space means that the weighted coordinate sum vanishes.

The submodule spanned by the Burau columns

def TauCeti.KnotTheory.burauColMatrix {R : Type u_1} [Ring R] (n : ℕ) (t : R) : Matrix (Fin n) (Fin (n - 1)) R

The n × (n - 1) matrix whose i-th column is the Burau column TauCeti.KnotTheory.burauCol t i. Its image is the submodule of the unreduced Burau representation that carries the reduced one.

Equations

• TauCeti.KnotTheory.burauColMatrix n t = Matrix.of fun (a : Fin n) (i : Fin (n - 1)) => TauCeti.KnotTheory.burauCol t i a

@[simp]

theorem TauCeti.KnotTheory.burauColMatrix_apply {R : Type u_1} [Ring R] (n : ℕ) (t : R) (a : Fin n) (i : Fin (n - 1)) : burauColMatrix n t a i = burauCol t i a

The entries of TauCeti.KnotTheory.burauColMatrix.

theorem TauCeti.KnotTheory.mul_burauColMatrix_apply {R : Type u_1} [Ring R] {n m : ℕ} (M : Matrix (Fin m) (Fin n) R) (t : R) (a : Fin m) (i : Fin (n - 1)) : (M * burauColMatrix n t) a i = M a ⬝ᵥ burauCol t i

Multiplying a matrix into TauCeti.KnotTheory.burauColMatrix pairs its rows with the Burau columns.

theorem TauCeti.KnotTheory.vecMul_burauColMatrix_apply {R : Type u_1} [Ring R] {n : ℕ} (t : R) (v : Fin n → R) (i : Fin (n - 1)) : Matrix.vecMul v (burauColMatrix n t) i = v ⬝ᵥ burauCol t i

Multiplying a row vector into TauCeti.KnotTheory.burauColMatrix pairs it with the Burau columns.

@[simp]

theorem TauCeti.KnotTheory.burauColMatrix_col {R : Type u_1} [Ring R] (n : ℕ) (t : R) (i : Fin (n - 1)) : (burauColMatrix n t).col i = burauCol t i

The i-th column of TauCeti.KnotTheory.burauColMatrix is the i-th Burau column.

theorem TauCeti.KnotTheory.burauColMatrix_mulVec_single {R : Type u_1} [Ring R] (n : ℕ) (t : R) (i : Fin (n - 1)) : (burauColMatrix n t).mulVec (Pi.single i 1) = burauCol t i

TauCeti.KnotTheory.burauColMatrix sends the i-th basis vector to the i-th Burau column.

@[simp]

theorem TauCeti.KnotTheory.geom_vecMul_burauColMatrix_eq_zero {R : Type u_1} [Ring R] (n : ℕ) (t : R) : Matrix.vecMul (fun (k : Fin n) => t ^ ↑k) (burauColMatrix n t) = 0

The Burau columns lie in the kernel of the geometric covector, the invariant submodule of TauCeti.KnotTheory.vecMul_burau_geom.

def TauCeti.KnotTheory.burauCoordMatrix {R : Type u_1} [Ring R] (n : ℕ) (t : Rˣ) : Matrix (Fin (n - 1)) (Fin n) R

The coordinates of a vector of the span of the Burau columns in that basis: the (i, a) entry is t⁻¹ ^ (i + 1 - a) for a ≤ i, and 0 otherwise. This is the explicit left inverse of TauCeti.KnotTheory.burauColMatrix of TauCeti.KnotTheory.burauCoordMatrix_mul_burauColMatrix.

Equations

• TauCeti.KnotTheory.burauCoordMatrix n t = Matrix.of fun (i : Fin (n - 1)) (a : Fin n) => if ↑a ≤ ↑i then ↑t⁻¹ ^ (↑i + 1 - ↑a) else 0

@[simp]

theorem TauCeti.KnotTheory.burauCoordMatrix_apply {R : Type u_1} [Ring R] (n : ℕ) (t : Rˣ) (i : Fin (n - 1)) (a : Fin n) : burauCoordMatrix n t i a = if ↑a ≤ ↑i then ↑t⁻¹ ^ (↑i + 1 - ↑a) else 0

The entries of TauCeti.KnotTheory.burauCoordMatrix.

@[simp]

theorem TauCeti.KnotTheory.burauCoordMatrix_mul_burauColMatrix {R : Type u_1} [Ring R] (n : ℕ) (t : Rˣ) : burauCoordMatrix n t * burauColMatrix n ↑t = 1

The Burau columns are independent: at a unit t the matrix of Burau columns has an explicit left inverse. In particular the submodule they span is free of rank n - 1 and is a direct summand of the free module on the strands.

theorem TauCeti.KnotTheory.burauColMatrix_mulVec_burauCoordMatrix_mulVec {R : Type u_1} [Ring R] (n : ℕ) (t : Rˣ) (x : Fin n → R) (hx : (fun (k : Fin n) => ↑t ^ ↑k) ⬝ᵥ x = 0) : (burauColMatrix n ↑t).mulVec ((burauCoordMatrix n t).mulVec x) = x

The Burau columns span the kernel of the geometric covector: every vector annihilated by (1, t, …, t ^ (n - 1)) is reconstructed from its burauCoordMatrix coordinates. Together with TauCeti.KnotTheory.burauCoordMatrix_mul_burauColMatrix, this identifies the kernel with the free module on Fin (n - 1).

The elementary reduced Burau matrices

def TauCeti.KnotTheory.reducedBurauColRow {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : Fin (n - 1) → R

The pairings of the i-th Burau row against all the Burau columns. This is the row in which the reduced Burau matrix in the Burau-column basis differs from the identity.

Equations

• TauCeti.KnotTheory.reducedBurauColRow t i j = TauCeti.KnotTheory.burauRow R i ⬝ᵥ TauCeti.KnotTheory.burauCol t j

theorem TauCeti.KnotTheory.burauRow_vecMul_burauColMatrix {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : Matrix.vecMul (burauRow R i) (burauColMatrix n t) = reducedBurauColRow t i

Pairing a Burau row against the Burau columns is what multiplying into TauCeti.KnotTheory.burauColMatrix computes.

@[simp]

theorem TauCeti.KnotTheory.reducedBurauColRow_self {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : reducedBurauColRow t i i = t + 1

The diagonal value of TauCeti.KnotTheory.reducedBurauColRow is t + 1.

theorem TauCeti.KnotTheory.reducedBurauColRow_of_succ {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) : reducedBurauColRow t i j = -t

The value of TauCeti.KnotTheory.reducedBurauColRow just above the diagonal is -t.

theorem TauCeti.KnotTheory.reducedBurauColRow_of_succ_rev {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑j + 1 = ↑i) : reducedBurauColRow t i j = -1

The value of TauCeti.KnotTheory.reducedBurauColRow just below the diagonal is -1.

theorem TauCeti.KnotTheory.reducedBurauColRow_of_not_adjacent {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : reducedBurauColRow t i j = 0

Away from the diagonal and its two neighbours TauCeti.KnotTheory.reducedBurauColRow vanishes.

def TauCeti.KnotTheory.reducedBurauColMatrix {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : Matrix (Fin (n - 1)) (Fin (n - 1)) R

The reduced Burau matrix in the Burau-column basis of the elementary braid TauCeti.BraidGroup.sigma i: the identity outside the i-th row, which is (…, 1, -t, t, …) with -t on the diagonal.

Equations

• TauCeti.KnotTheory.reducedBurauColMatrix t i = 1 - Matrix.vecMulVec (Pi.single i 1) (TauCeti.KnotTheory.reducedBurauColRow t i)

theorem TauCeti.KnotTheory.reducedBurauColMatrix_def {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : reducedBurauColMatrix t i = 1 - Matrix.vecMulVec (Pi.single i 1) (reducedBurauColRow t i)

The defining formula for an elementary reduced Burau matrix: it differs from the identity by the rank-one matrix vecMulVec (Pi.single i 1) (reducedBurauColRow t i), supported in the i-th row.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_apply {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i a b : Fin (n - 1)) : reducedBurauColMatrix t i a b = (if a = b then 1 else 0) - (if a = i then 1 else 0) * reducedBurauColRow t i b

The entries of an elementary reduced Burau matrix.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_apply_of_ne {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i a : Fin (n - 1)} (h : a ≠ i) (b : Fin (n - 1)) : reducedBurauColMatrix t i a b = if a = b then 1 else 0

Outside its i-th row an elementary reduced Burau matrix has the rows of the identity.

@[simp]

theorem TauCeti.KnotTheory.reducedBurauColMatrix_apply_self {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : reducedBurauColMatrix t i i i = -t

The diagonal entry of an elementary reduced Burau matrix in its nontrivial row is -t.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_apply_of_succ {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) : reducedBurauColMatrix t i i j = t

The entry just above the diagonal in the nontrivial row of an elementary reduced Burau matrix is t.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_apply_of_succ_rev {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑j + 1 = ↑i) : reducedBurauColMatrix t i i j = 1

The entry just below the diagonal in the nontrivial row of an elementary reduced Burau matrix is 1.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_apply_of_not_adjacent {R : Type u_1} [Ring R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : reducedBurauColMatrix t i i j = 0

Away from the diagonal and its two neighbours the nontrivial row of an elementary reduced Burau matrix vanishes.

The reduced matrices are the restriction of the unreduced ones

theorem TauCeti.KnotTheory.burauMatrix_mul_burauColMatrix {R : Type u_1} [Ring R] {n : ℕ} (t : R) (i : Fin (n - 1)) : burauMatrix t i * burauColMatrix n t = burauColMatrix n t * reducedBurauColMatrix t i

An elementary Burau matrix restricts to the elementary reduced Burau matrix on the span of the Burau columns.

The reduced Burau matrices in the Burau-column basis on two and three strands

theorem TauCeti.KnotTheory.reducedBurauColMatrix_two {R : Type u_1} [Ring R] (t : R) (i : Fin (2 - 1)) : reducedBurauColMatrix t i = !![-t]

On two strands the reduced Burau representation is one-dimensional, sending the single elementary braid to -t.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_three_zero {R : Type u_1} [Ring R] (t : R) : reducedBurauColMatrix t 0 = !![-t, t; 0, 1]

The reduced Burau matrix of the first elementary braid on three strands.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_three_one {R : Type u_1} [Ring R] (t : R) : reducedBurauColMatrix t 1 = !![1, 0; 1, -t]

The reduced Burau matrix of the second elementary braid on three strands.

@[simp]

theorem TauCeti.KnotTheory.det_burauColMatrix_submatrix_castSucc {R : Type u_1} [CommRing R] (n : ℕ) (t : R) : ((burauColMatrix (n + 1) t).submatrix Fin.castSucc id).det = t ^ n

The first n rows of the Burau-column basis form a lower triangular matrix with constant diagonal t. Thus they give invertible coordinates whenever t is a unit.

theorem TauCeti.KnotTheory.burauColMatrix_mulVec_mem_reducedBurauSpace {R : Type u_1} [CommRing R] (n : ℕ) (t : R) (c : Fin (n - 1) → R) : (burauColMatrix n t).mulVec c ∈ reducedBurauSpace n t

Every linear combination of the Burau columns belongs to the invariant kernel carrying the reduced Burau representation.

def TauCeti.KnotTheory.reducedBurauSpaceEquiv {R : Type u_1} [CommRing R] (n : ℕ) (t : R) : (Fin n → R) ≃ₗ[R] ReducedBurauSpace (n + 1) t

Coordinates on the reduced Burau space of an (n + 1)-strand braid. The tail coordinates are free, and the zeroth coordinate is determined by the equation x₀ + ∑ i, t ^ (i + 1) x_(i+1) = 0.

Equations

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

@[simp]

theorem TauCeti.KnotTheory.reducedBurauSpaceEquiv_apply_coe {R : Type u_1} [CommRing R] (n : ℕ) (t : R) (x : Fin n → R) : ↑((reducedBurauSpaceEquiv n t) x) = Fin.cons (-∑ i : Fin n, t ^ (↑i + 1) * x i) x

The vector underlying reducedBurauSpaceEquiv: the free coordinates form its tail.

@[simp]

theorem TauCeti.KnotTheory.reducedBurauSpaceEquiv_symm_apply {R : Type u_1} [CommRing R] (n : ℕ) (t : R) (x : ReducedBurauSpace (n + 1) t) : (reducedBurauSpaceEquiv n t).symm x = Fin.tail ↑x

The inverse coordinate map takes the tail of a vector in the reduced Burau space.

def TauCeti.KnotTheory.burauRepresentation {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) : Representation R (BraidGroup n) (Fin n → R)

The unreduced Burau matrix representation, regarded as a representation on the free module of column vectors.

Equations

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

@[simp]

theorem TauCeti.KnotTheory.burauRepresentation_apply {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (b : BraidGroup n) (x : Fin n → R) : ((burauRepresentation n t) b) x = (↑((burau n t) b)).mulVec x

The module action of the unreduced Burau representation is multiplication by its Burau matrix.

theorem TauCeti.KnotTheory.geometricCovector_burauRepresentation {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (b : BraidGroup n) (x : Fin n → R) : (geometricCovector n ↑t) (((burauRepresentation n t) b) x) = (geometricCovector n ↑t) x

The geometric covector is invariant under the unreduced Burau representation.

theorem TauCeti.KnotTheory.reducedBurauSpace_invariant {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (b : BraidGroup n) : reducedBurauSpace n ↑t ≤ Submodule.comap ((burauRepresentation n t) b) (reducedBurauSpace n ↑t)

The kernel of the geometric covector is invariant under the unreduced Burau action.

def TauCeti.KnotTheory.reducedBurauSubrepresentation {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) : Representation R (BraidGroup n) (ReducedBurauSpace n ↑t)

The reduced Burau representation on the invariant kernel of the geometric covector.

Equations

• TauCeti.KnotTheory.reducedBurauSubrepresentation n t = (TauCeti.KnotTheory.burauRepresentation n t).subrepresentation (TauCeti.KnotTheory.reducedBurauSpace n ↑t) ⋯

@[simp]

theorem TauCeti.KnotTheory.coe_reducedBurauSubrepresentation_apply {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (b : BraidGroup n) (x : ReducedBurauSpace n ↑t) : ↑(((reducedBurauSubrepresentation n t) b) x) = (↑((burau n t) b)).mulVec ↑x

The kernel representation acts by the unreduced Burau matrix on underlying vectors.

def TauCeti.KnotTheory.reducedBurau {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) : Representation R (BraidGroup (n + 1)) (Fin n → R)

The reduced Burau representation of the braid group on n + 1 strands, transported from the invariant kernel to its n free tail coordinates.

Equations

• TauCeti.KnotTheory.reducedBurau n t = (TauCeti.KnotTheory.reducedBurauSpaceEquiv n ↑t).symm.conjRingEquiv.toMonoidHom.comp (TauCeti.KnotTheory.reducedBurauSubrepresentation (n + 1) t)

@[simp]

theorem TauCeti.KnotTheory.reducedBurau_apply {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (b : BraidGroup (n + 1)) (x : Fin n → R) : ((reducedBurau n t) b) x = Fin.tail ((↑((burau (n + 1) t) b)).mulVec ↑((reducedBurauSpaceEquiv n ↑t) x))

The reduced action is obtained by inserting free coordinates into the invariant kernel, applying the unreduced Burau matrix, and taking the tail.

theorem TauCeti.KnotTheory.reducedBurau_sigma {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (i : Fin n) (x : Fin n → R) : ((reducedBurau n t) (BraidGroup.sigma i)) x = Fin.tail ((burauMatrix (↑t) i).mulVec ↑((reducedBurauSpaceEquiv n ↑t) x))

On an elementary braid, the reduced action is the tail of the elementary Burau matrix acting on the canonical kernel coordinates.

theorem TauCeti.KnotTheory.reducedBurau_sigma_apply {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (i : Fin n) (x : Fin n → R) (j : Fin n) : ((reducedBurau n t) (BraidGroup.sigma i)) x j = (burauMatrix (↑t) i).mulVec (↑((reducedBurauSpaceEquiv n ↑t) x)) j.succ

The individual free coordinates of the reduced action of an elementary braid: the j-th coordinate of the reduced action is the j.succ-th coordinate of the unreduced action. This is TauCeti.KnotTheory.reducedBurau_sigma evaluated at a coordinate, using that Fin.tail v j is by definition v j.succ; it is the form in which entrywise computations with the reduced matrices are carried out.

@[simp]

theorem TauCeti.KnotTheory.reducedBurau_sigma_zero_apply {R : Type u_1} [CommRing R] (t : Rˣ) (x : Fin 1 → R) : ((reducedBurau 1 t) (BraidGroup.sigma 0)) x 0 = -↑t * x 0

On two strands the reduced Burau representation sends the elementary braid to multiplication by -t. This is the first nonzero-dimensional case and fixes the normalization of the reduced representation.

The braid relations, the inverse and the Hecke relation

@[simp]

theorem TauCeti.KnotTheory.det_reducedBurauColMatrix {R : Type u_1} [CommRing R] {n : ℕ} (t : R) (i : Fin (n - 1)) : (reducedBurauColMatrix t i).det = -t

The determinant of an elementary reduced Burau matrix is -t, as for the unreduced one.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_mul_comm {R : Type u_1} [CommRing R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) : reducedBurauColMatrix t i * reducedBurauColMatrix t j = reducedBurauColMatrix t j * reducedBurauColMatrix t i

The distant commutation relation for the elementary reduced Burau matrices.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_braid {R : Type u_1} [CommRing R] {n : ℕ} (t : R) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i) : reducedBurauColMatrix t i * reducedBurauColMatrix t j * reducedBurauColMatrix t i = reducedBurauColMatrix t j * reducedBurauColMatrix t i * reducedBurauColMatrix t j

The braid relation for the elementary reduced Burau matrices.

theorem TauCeti.KnotTheory.reducedBurauColMatrix_mul_self {R : Type u_1} [CommRing R] {n : ℕ} (t : R) (i : Fin (n - 1)) : reducedBurauColMatrix t i * reducedBurauColMatrix t i = (1 - t) • reducedBurauColMatrix t i + t • 1

The quadratic relation for the elementary reduced Burau matrices, equivalently (x - 1) * (x + t) = 0. This is the Iwahori-Hecke quadratic relation in the normalisation with eigenvalues 1 and -t.

The reduced Burau homomorphism in the Burau-column basis

def TauCeti.KnotTheory.reducedBurauColGL {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (i : Fin (n - 1)) : GL (Fin (n - 1)) R

An elementary reduced Burau matrix as an element of the general linear group, with inverse 1 - t⁻¹ • vecMulVec (Pi.single i 1) (reducedBurauColRow t i).

Equations

• TauCeti.KnotTheory.reducedBurauColGL t i = TauCeti.oneSubVecMulVecGL t (Pi.single i 1) (TauCeti.KnotTheory.reducedBurauColRow (↑t) i) ⋯

@[simp]

theorem TauCeti.KnotTheory.coe_reducedBurauColGL {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (i : Fin (n - 1)) : ↑(reducedBurauColGL t i) = reducedBurauColMatrix (↑t) i

The matrix underlying TauCeti.KnotTheory.reducedBurauColGL.

@[simp]

theorem TauCeti.KnotTheory.inv_reducedBurauColMatrix {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (i : Fin (n - 1)) : (reducedBurauColMatrix (↑t) i)⁻¹ = 1 - ↑t⁻¹ • Matrix.vecMulVec (Pi.single i 1) (reducedBurauColRow (↑t) i)

The nonsingular inverse of an elementary reduced Burau matrix.

def TauCeti.KnotTheory.reducedBurauCol {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) : BraidGroup n →* GL (Fin (n - 1)) R

The reduced Burau homomorphism in the basis of Burau columns. Its name records the basis to distinguish it from TauCeti.KnotTheory.reducedBurau, which uses canonical tail coordinates.

Equations

• TauCeti.KnotTheory.reducedBurauCol n t = TauCeti.KnotTheory.braidHomOfOneSubVecMulVec n t (fun (i : Fin (n - 1)) => Pi.single i 1) (TauCeti.KnotTheory.reducedBurauColRow ↑t) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.KnotTheory.reducedBurauCol_sigma {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (i : Fin (n - 1)) : (reducedBurauCol n t) (BraidGroup.sigma i) = reducedBurauColGL t i

The Burau-column reduced homomorphism takes an elementary braid to its corresponding elementary reduced matrix.

theorem TauCeti.KnotTheory.coe_reducedBurauCol_sigma {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (i : Fin (n - 1)) : ↑((reducedBurauCol n t) (BraidGroup.sigma i)) = reducedBurauColMatrix (↑t) i

The matrix of an elementary braid under the Burau-column reduced homomorphism.

theorem TauCeti.KnotTheory.det_reducedBurauCol {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (b : BraidGroup n) : Matrix.GeneralLinearGroup.det ((reducedBurauCol n t) b) = (-t) ^ Multiplicative.toAdd ((ArtinGroup.exponentSum (CoxeterMatrix.A (n - 1))) b)

The determinant of the Burau-column reduced matrix of a braid is -t raised to its exponent sum, as for the unreduced representation.

theorem TauCeti.KnotTheory.burau_mul_burauColMatrix {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (b : BraidGroup n) : ↑((burau n t) b) * burauColMatrix n ↑t = burauColMatrix n ↑t * ↑((reducedBurauCol n t) b)

The reduced Burau homomorphism in the Burau-column basis is the restriction of the unreduced one to the span of those columns.

theorem TauCeti.KnotTheory.reducedBurauCol_eq {R : Type u_1} [CommRing R] {n : ℕ} (t : Rˣ) (b : BraidGroup n) : ↑((reducedBurauCol n t) b) = burauCoordMatrix n t * ↑((burau n t) b) * burauColMatrix n ↑t

The reduced Burau matrix of a braid in the Burau-column basis can be read off from the unreduced matrix using the explicit left inverse of the column matrix.

theorem TauCeti.KnotTheory.reducedBurau_apply_burauColMatrix_mulVec {R : Type u_1} [CommRing R] (n : ℕ) (t : Rˣ) (b : BraidGroup (n + 1)) (c : Fin (n + 1 - 1) → R) : ((reducedBurau n t) b) (Fin.tail ((burauColMatrix (n + 1) ↑t).mulVec c)) = Fin.tail ((burauColMatrix (n + 1) ↑t).mulVec ((↑((reducedBurauCol (n + 1) t) b)).mulVec c))

The Burau-column and tail-coordinate constructions give the same reduced action after the coordinate change that takes column coefficients to the tail of their linear combination.