Documentation

TauCeti.KnotTheory.Burau.Basic

The Burau representation of the braid group #

The braid group TauCeti.BraidGroup n acts on the first homology of the infinite cyclic cover of the n-punctured disc relative to the fibre over a basepoint. This relative homology is free of rank n over the ring of Laurent polynomials, and a choice of basis gives the unreduced Burau representation. This file constructs it over an arbitrary commutative ring R and an arbitrary unit t : Rˣ, so the Laurent-polynomial case is the instance R = ℤ[T;T⁻¹], t = T. The absolute first homology of the cover instead has rank n - 1 and carries the reduced representation.

Concretely the elementary braid σ i is sent to the matrix that is the identity outside the two strands it crosses and is !![1 - t, t; 1, 0] on them. The whole file is organised around the observation that this matrix differs from the identity by a rank-one matrix, burauMatrix t i = 1 - vecMulVec (burauCol t i) (burauRow R i), where burauCol t i = t • e i - e (i + 1) and burauRow R i = e i - e (i + 1). Products of rank-one matrices are governed by a single scalar, vecMulVec u v * vecMulVec u' v' = (v ⬝ᵥ u') • vecMulVec u v', so all four dot products between the rows and columns attached to two elementary braids are computed once, and both defining braid relations, the inverse matrix, and the determinant follow from them by pure module algebra. This is what keeps the verification of the relations short: the braid relation reduces to U * U = (t + 1) • U, U * V * U = t • U and their mirror images.

Two theorems keep the representation honest. TauCeti.KnotTheory.det_burauMatrix computes the determinant of an elementary Burau matrix as -t, so the representation is by genuinely invertible matrices and its determinant character is (-t) to the exponent sum; TauCeti.KnotTheory.coe_burau_one_eq_permMatrix identifies the specialisation at t = 1 with the permutation representation TauCeti.BraidGroup.permHom of the strands, so the Burau representation is a one-parameter deformation of the permutation representation. Over a nontrivial ring no elementary Burau matrix is the identity (TauCeti.KnotTheory.burauMatrix_ne_one), so as soon as 2 ≤ n — that is, as soon as there is an elementary braid at all — the representation is not trivial.

Finally there are two dual invariant vectors, unconditionally in n and R: the all-ones column vector is fixed (TauCeti.KnotTheory.burau_mulVec_one), and the row vector (1, t, …, t ^ (n - 1)) is fixed (TauCeti.KnotTheory.vecMul_burau_geom). The kernel of the latter covector is therefore an invariant submodule, and for 2 ≤ n over a nontrivial ring it is a proper nonzero one, which is the reducibility that the reduced Burau representation — the restriction to that kernel — is carved out of. The restriction and an explicit basis of its kernel are constructed in TauCeti.KnotTheory.Burau.Reduced.Basic; its comparison with the Seifert-matrix Alexander polynomial of TauCeti/KnotTheory/Alexander.lean still needs the closure of a braid to a link.

This is the Burau route of the "knot polynomials, each a project in itself, with several algorithms apiece" bullet of Layer 4 ("knot theory, done properly") of the GeometricTopology roadmap.

Main definitions #

Main results #

References #

The rank-one part of an elementary Burau matrix #

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

The column vector t • e i - e (i + 1) indexed by the strands, where i and i + 1 are the two strands crossed by the elementary braid TauCeti.BraidGroup.sigma i.

Equations
Instances For
    source
    def TauCeti.KnotTheory.burauRow (R : Type u_2) [Ring R] {n : ℕ} (i : Fin (n - 1)) :
    Fin n → R

    The row vector e i - e (i + 1) indexed by the strands, where i and i + 1 are the two strands crossed by the elementary braid TauCeti.BraidGroup.sigma i.

    Equations
    Instances For
      source
      theorem TauCeti.KnotTheory.burauCol_apply {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) (k : Fin n) :
      burauCol t i k = (if k = BraidGroup.strand i then t else 0) - if k = BraidGroup.strandSucc i then 1 else 0

      The entries of the Burau column vector.

      source
      theorem TauCeti.KnotTheory.burauRow_apply {R : Type u_1} {n : ℕ} [Ring R] (i : Fin (n - 1)) (k : Fin n) :
      burauRow R i k = (if k = BraidGroup.strand i then 1 else 0) - if k = BraidGroup.strandSucc i then 1 else 0

      The entries of the Burau row vector.

      source
      theorem TauCeti.KnotTheory.burauRow_dotProduct {R : Type u_1} {n : ℕ} [Ring R] (i : Fin (n - 1)) (w : Fin n → R) :
      burauRow R i ⬝ᵥ w = w (BraidGroup.strand i) - w (BraidGroup.strandSucc i)

      Dotting the Burau row vector against any vector reads off the difference of its values at the two crossed strands.

      source
      theorem TauCeti.KnotTheory.dotProduct_burauCol {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) (w : Fin n → R) :
      w ⬝ᵥ burauCol t i = w (BraidGroup.strand i) * t - w (BraidGroup.strandSucc i)

      Dotting any vector against the Burau column vector.

      source
      theorem TauCeti.KnotTheory.burauRow_dotProduct_burauCol_self {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
      burauRow R i ⬝ᵥ burauCol t i = t + 1

      The row and column vectors of one and the same elementary braid pair to t + 1.

      source
      theorem TauCeti.KnotTheory.burauRow_dotProduct_burauCol_of_succ {R : Type u_1} {n : ℕ} [Ring R] (t : R) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) :
      burauRow R i ⬝ᵥ burauCol t j = -t

      For two consecutive elementary braids the row of the first pairs with the column of the second to -t.

      source
      theorem TauCeti.KnotTheory.burauRow_dotProduct_burauCol_of_succ_rev {R : Type u_1} {n : ℕ} [Ring R] (t : R) {i j : Fin (n - 1)} (h : ↑i + 1 = ↑j) :
      burauRow R j ⬝ᵥ burauCol t i = -1

      For two consecutive elementary braids the row of the second pairs with the column of the first to -1.

      source
      theorem TauCeti.KnotTheory.burauRow_dotProduct_burauCol_of_not_adjacent {R : Type u_1} {n : ℕ} [Ring R] (t : R) {i j : Fin (n - 1)} (h : ↑i + 2 ≤ ↑j ∨ ↑j + 2 ≤ ↑i) :
      burauRow R i ⬝ᵥ burauCol t j = 0

      Two elementary braids that share no strand have orthogonal rows and columns.

      The elementary Burau matrices #

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

      The unreduced Burau matrix of the elementary braid TauCeti.BraidGroup.sigma i at the parameter t: the identity outside the two strands crossed by sigma i, and !![1 - t, t; 1, 0] on them.

      Equations
      Instances For
        source
        theorem TauCeti.KnotTheory.burauMatrix_def {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        burauMatrix t i = 1 - Matrix.vecMulVec (burauCol t i) (burauRow R i)

        The defining formula for an elementary Burau matrix: it differs from the identity by the rank-one matrix vecMulVec (burauCol t i) (burauRow R i).

        source
        theorem TauCeti.KnotTheory.burauMatrix_apply {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) (a b : Fin n) :
        burauMatrix t i a b = (if a = b then 1 else 0) - burauCol t i a * burauRow R i b

        The entries of an elementary Burau matrix.

        source
        @[simp]
        theorem TauCeti.KnotTheory.burauMatrix_apply_strand_strand {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        burauMatrix t i (BraidGroup.strand i) (BraidGroup.strand i) = 1 - t

        The upper left entry of the nontrivial two-by-two block of an elementary Burau matrix.

        source
        @[simp]
        theorem TauCeti.KnotTheory.burauMatrix_apply_strand_strandSucc {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        burauMatrix t i (BraidGroup.strand i) (BraidGroup.strandSucc i) = t

        The upper right entry of the nontrivial two-by-two block of an elementary Burau matrix.

        source
        @[simp]
        theorem TauCeti.KnotTheory.burauMatrix_apply_strandSucc_strand {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        burauMatrix t i (BraidGroup.strandSucc i) (BraidGroup.strand i) = 1

        The lower left entry of the nontrivial two-by-two block of an elementary Burau matrix.

        source
        @[simp]
        theorem TauCeti.KnotTheory.burauMatrix_apply_strandSucc_strandSucc {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        burauMatrix t i (BraidGroup.strandSucc i) (BraidGroup.strandSucc i) = 0

        The lower right entry of the nontrivial two-by-two block of an elementary Burau matrix.

        source
        theorem TauCeti.KnotTheory.burauMatrix_apply_of_ne {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) {a : Fin n} (h : a ≠ BraidGroup.strand i) (h' : a ≠ BraidGroup.strandSucc i) (b : Fin n) :
        burauMatrix t i a b = if a = b then 1 else 0

        Away from the two crossed strands the Burau matrix has the rows of the identity.

        source
        theorem TauCeti.KnotTheory.burauMatrix_ne_one {R : Type u_1} {n : ℕ} [Ring R] [Nontrivial R] (t : R) (i : Fin (n - 1)) :
        burauMatrix t i ≠ 1

        An elementary Burau matrix is never the identity: the entry at which the two crossed strands meet is 1 rather than 0. Since an i : Fin (n - 1) exists exactly when 2 ≤ n, this says that the Burau representation is nontrivial for 2 ≤ n over a nontrivial ring.

        source
        theorem TauCeti.KnotTheory.burauMatrix_one_eq_permMatrix {R : Type u_1} {n : ℕ} [Ring R] (i : Fin (n - 1)) :
        burauMatrix 1 i = Equiv.Perm.permMatrix R (BraidGroup.transposition i)

        At t = 1 an elementary Burau matrix is the permutation matrix of the transposition of the two crossed strands.

        source
        theorem TauCeti.KnotTheory.vecMul_burauMatrix {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) (w : Fin n → R) :
        Matrix.vecMul w (burauMatrix t i) = w - (w ⬝ᵥ burauCol t i) • burauRow R i

        The action of an elementary Burau matrix on a row vector, in rank-one form.

        source
        @[simp]
        theorem TauCeti.KnotTheory.burauMatrix_mulVec_one {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        (burauMatrix t i).mulVec 1 = 1

        The all-ones column vector is fixed by every elementary Burau matrix.

        source
        theorem TauCeti.KnotTheory.geom_dotProduct_burauCol_eq_zero {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        (fun (k : Fin n) => t ^ ↑k) ⬝ᵥ burauCol t i = 0

        The geometric row vector (1, t, …, t ^ (n - 1)) annihilates every Burau column.

        source
        @[simp]
        theorem TauCeti.KnotTheory.vecMul_burauMatrix_geom {R : Type u_1} {n : ℕ} [Ring R] (t : R) (i : Fin (n - 1)) :
        Matrix.vecMul (fun (k : Fin n) => t ^ ↑k) (burauMatrix t i) = fun (k : Fin n) => t ^ ↑k

        The geometric row vector (1, t, …, t ^ (n - 1)) is fixed by every elementary Burau matrix.

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

        The distant commutation relation for the elementary Burau matrices.

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

        The braid relation for the elementary Burau matrices.

        source
        @[simp]
        theorem TauCeti.KnotTheory.det_burauMatrix {R : Type u_1} {n : ℕ} [CommRing R] (t : R) (i : Fin (n - 1)) :
        (burauMatrix t i).det = -t

        The determinant of an elementary Burau matrix is -t.

        The Burau representation #

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

        An elementary Burau matrix as an element of the general linear group: its underlying matrix is TauCeti.KnotTheory.burauMatrix t i, with inverse 1 - t⁻¹ • vecMulVec (burauCol t i) (burauRow R i).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem TauCeti.KnotTheory.coe_burauGL {R : Type u_1} {n : ℕ} [CommRing R] (t : Rˣ) (i : Fin (n - 1)) :
          ↑(burauGL t i) = burauMatrix (↑t) i

          The matrix underlying TauCeti.KnotTheory.burauGL.

          source
          @[simp]
          theorem TauCeti.KnotTheory.inv_burauMatrix {R : Type u_1} {n : ℕ} [CommRing R] (t : Rˣ) (i : Fin (n - 1)) :
          (burauMatrix (↑t) i)⁻¹ = 1 - ↑t⁻¹ • Matrix.vecMulVec (burauCol (↑t) i) (burauRow R i)

          The nonsingular inverse of an elementary Burau matrix.

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

          The unreduced Burau representation of the braid group on n strands at a unit t, sending the elementary braid sigma i to TauCeti.KnotTheory.burauGL t i.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.KnotTheory.burau_sigma {R : Type u_1} {n : ℕ} [CommRing R] (t : Rˣ) (i : Fin (n - 1)) :
            (burau n t) (BraidGroup.sigma i) = burauGL t i

            The Burau representation takes an elementary braid to the elementary Burau matrix.

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

            The determinant of the Burau matrix of a braid is -t raised to its exponent sum.

            The permutation representation as the specialisation at t = 1 #

            source
            theorem TauCeti.KnotTheory.burau_one_eq_permMatrixHom_comp {R : Type u_1} [CommRing R] (n : ℕ) :
            burau n 1 = Matrix.permMatrixHom.toHomUnits.comp (BraidGroup.permHom n)

            The Burau representation at t = 1 is the permutation representation of the strands. Note that TauCeti.BraidGroup.permHom is a homomorphism while Equiv.Perm.permMatrix is an antihomomorphism, so the comparison is with Matrix.permMatrixHom, which inverts before taking the permutation matrix.

            source
            theorem TauCeti.KnotTheory.coe_burau_one_eq_permMatrix {R : Type u_1} {n : ℕ} [CommRing R] (b : BraidGroup n) :
            ↑((burau n 1) b) = Matrix.permMatrixHom ((BraidGroup.permHom n) b)

            At t = 1 the Burau matrix of a braid is the permutation matrix of the underlying permutation of the strands.

            Reducibility: the invariant vector and covector #

            source
            theorem TauCeti.KnotTheory.burauMatrix_mulVec {R : Type u_1} {n : ℕ} [CommRing R] (t : R) (i : Fin (n - 1)) (v : Fin n → R) :
            (burauMatrix t i).mulVec v = v - (burauRow R i ⬝ᵥ v) • burauCol t i

            The action of an elementary Burau matrix on a column vector, in rank-one form.

            source
            theorem TauCeti.KnotTheory.burau_mulVec_of_forall {R : Type u_1} {n : ℕ} [CommRing R] {t : Rˣ} {v : Fin n → R} (h : ∀ (i : Fin (n - 1)), (burauMatrix (↑t) i).mulVec v = v) (b : BraidGroup n) :
            (↑((burau n t) b)).mulVec v = v

            A column vector fixed by every elementary Burau matrix is fixed by the whole representation.

            source
            theorem TauCeti.KnotTheory.vecMul_burau_of_forall {R : Type u_1} {n : ℕ} [CommRing R] {t : Rˣ} {w : Fin n → R} (h : ∀ (i : Fin (n - 1)), Matrix.vecMul w (burauMatrix (↑t) i) = w) (b : BraidGroup n) :
            Matrix.vecMul w ↑((burau n t) b) = w

            A row vector fixed by every elementary Burau matrix is fixed by the whole representation.

            source
            theorem TauCeti.KnotTheory.burau_mul_of_forall {R : Type u_1} {n : ℕ} [CommRing R] {β : Type u_2} [Fintype β] [DecidableEq β] {t : Rˣ} {C : Matrix (Fin n) β R} {ρ : BraidGroup n →* GL β R} (h : ∀ (i : Fin (n - 1)), burauMatrix (↑t) i * C = C * ↑(ρ (BraidGroup.sigma i))) (b : BraidGroup n) :
            ↑((burau n t) b) * C = C * ↑(ρ b)

            A matrix intertwining every elementary Burau matrix with the corresponding value of a representation ρ intertwines the whole Burau representation with ρ.

            source
            @[simp]
            theorem TauCeti.KnotTheory.burau_mulVec_one {R : Type u_1} {n : ℕ} [CommRing R] (t : Rˣ) (b : BraidGroup n) :
            (↑((burau n t) b)).mulVec 1 = 1

            The all-ones column vector is fixed by the Burau representation. The line it spans is therefore an invariant submodule; for 2 ≤ n over a nontrivial ring it is a proper nonzero one, so the unreduced Burau representation is reducible.

            source
            @[simp]
            theorem TauCeti.KnotTheory.vecMul_burau_geom {R : Type u_1} {n : ℕ} [CommRing R] (t : Rˣ) (b : BraidGroup n) :
            Matrix.vecMul (fun (k : Fin n) => ↑t ^ ↑k) ↑((burau n t) b) = fun (k : Fin n) => ↑t ^ ↑k

            The geometric row vector (1, t, …, t ^ (n - 1)) is fixed by the Burau representation. Its kernel is therefore an invariant submodule — for 2 ≤ n over a nontrivial ring a proper nonzero one — and it is what carries the reduced Burau representation.