The Alexander polynomial of a Seifert matrix

A Seifert surface of a knot carries a bilinear linking form, and a basis of its first homology turns that form into a square integer matrix V, the Seifert matrix of the surface. The Alexander polynomial of the knot is read off V as the determinant of t^(1/2) V - t^(-1/2) Vᵀ. This file builds that invariant and proves the identities that make it one: the symmetry Δ(t) = Δ(t⁻¹), the value Δ(1) = det (V - Vᵀ), and invariance under the two moves generating S-equivalence of Seifert matrices (congruence V ↦ P * V * Pᵀ by a matrix P whose determinant squares to 1 — over ℤ this is precisely a change of basis of the homology — and the enlargements that change the Seifert surface without changing the knot).

Half-integer powers are avoided by pulling t^(-1/2) out of every row: for a matrix of size 2 * g — the size of every Seifert matrix, g the genus of the surface — the determinant of t^(1/2) V - t^(-1/2) Vᵀ is T ^ (-g) times the determinant of alexanderMatrix V = T • V - Vᵀ, which lives in the Laurent polynomial ring R[T;T⁻¹] on the nose. That is the definition of alexander below, with the genus read off the index type as Fintype.card ι / 2.

This is the algebraic half of the Alexander polynomial: the input is a matrix, not a knot. Producing a Seifert matrix from a knot (a Seifert surface, a basis of its homology, and the linking form) is separate work, as is the agreement of this route with the Conway skein relation on a diagram and with the Burau representation of a braid word. What is fixed here is the normalisation those routes must match, pinned by the trefoil and figure-eight computations at the end of the file.

Everything is stated over an arbitrary commutative ring and an arbitrary index type; the knot-theoretic case is R = ℤ and ι = Fin (2 * g).

This is the Seifert-matrix route to the Alexander polynomial called for by Layer 4 (knot theory) of the GeometricTopology roadmap.

Main definitions

• TauCeti.KnotTheory.alexanderMatrix: the matrix T • V - Vᵀ over R[T;T⁻¹].
• TauCeti.KnotTheory.alexander: the Conway-normalised Alexander polynomial T ^ (-g) * det (T • V - Vᵀ), where 2 * g is the size of V.
• TauCeti.KnotTheory.enlargeColumn, TauCeti.KnotTheory.enlargeRow: the two enlargements of a Seifert matrix, which together with congruence generate S-equivalence.

Main results

• TauCeti.KnotTheory.invert_alexander: Δ(t⁻¹) = Δ(t) for a matrix of even size.
• TauCeti.KnotTheory.alexander_congruence_of_det_sq_eq_one: Δ is unchanged by V ↦ P * V * Pᵀ whenever det P ^ 2 = 1. Over ℤ that is exactly the congruence by a change of basis of the first homology of the Seifert surface, since a change of basis of a free ℤ-module has determinant ±1; over a general commutative ring an invertible P need only have unit determinant, and the hypothesis is a genuine restriction.
• TauCeti.KnotTheory.alexander_enlargeColumn, TauCeti.KnotTheory.alexander_enlargeRow: Δ is unchanged by the enlargements. This is where the normalisation earns its keep: the unnormalised determinant is multiplied by T.
• TauCeti.KnotTheory.eval₂_one_alexander: Δ(1) = det (V - Vᵀ), the determinant of the intersection form of the Seifert surface; for a knot it is 1, so Δ is normalised so that the unknot has Δ = 1 (TauCeti.KnotTheory.alexander_of_isEmpty).
• TauCeti.KnotTheory.alexander_fin_two: the closed form of Δ for a genus-one (2 × 2) Seifert matrix, from which the two examples below are read off.
• TauCeti.KnotTheory.alexander_trefoilSeifertMatrix and TauCeti.KnotTheory.alexander_figureEightSeifertMatrix: the classical values t - 1 + t⁻¹ and -t + 3 - t⁻¹.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapters 6 and 8 (Seifert matrices, S-equivalence, and the Conway-normalised Alexander polynomial).
• G. Burde, H. Zieschang, Knots, 2nd ed., de Gruyter (2003), Chapter 8.

noncomputable def TauCeti.KnotTheory.alexanderMatrix {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) : Matrix ι ι (LaurentPolynomial R)

The Alexander matrix T • V - Vᵀ of a square matrix V over R, with entries in the ring R[T;T⁻¹] of Laurent polynomials.

This is t^(1/2) times the classical matrix t^(1/2) V - t^(-1/2) Vᵀ, so for V of size 2 * g its determinant is T ^ g times the classical one; the normalisation is restored in TauCeti.KnotTheory.alexander.

Equations

• TauCeti.KnotTheory.alexanderMatrix V = LaurentPolynomial.T 1 • V.map ⇑LaurentPolynomial.C - (V.map ⇑LaurentPolynomial.C).transpose

@[simp]

theorem TauCeti.KnotTheory.alexanderMatrix_apply {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (i j : ι) : alexanderMatrix V i j = LaurentPolynomial.T 1 * LaurentPolynomial.C (V i j) - LaurentPolynomial.C (V j i)

The entries of the Alexander matrix.

@[simp]

theorem TauCeti.KnotTheory.transpose_alexanderMatrix {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) : (alexanderMatrix V).transpose = alexanderMatrix V.transpose

Transposing the Alexander matrix transposes the underlying matrix.

theorem TauCeti.KnotTheory.map_invert_alexanderMatrix {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) : (alexanderMatrix V).map ⇑LaurentPolynomial.invert = -LaurentPolynomial.T (-1) • (alexanderMatrix V).transpose

Substituting T⁻¹ for T in the Alexander matrix transposes it and rescales it by -T⁻¹. This is the matrix-level source of the symmetry of the Alexander polynomial.

@[simp]

theorem TauCeti.KnotTheory.map_eval₂_alexanderMatrix {R : Type u_1} [CommRing R] {ι : Type u_2} {S : Type u_3} [CommRing S] (f : R →+* S) (x : Sˣ) (V : Matrix ι ι R) : (alexanderMatrix V).map ⇑(LaurentPolynomial.eval₂ f x) = ↑x • V.map ⇑f - (V.map ⇑f).transpose

Evaluating the Alexander matrix at a unit parameter gives the usual matrix x • V - Vᵀ, with coefficients transported by the chosen ring homomorphism.

def TauCeti.KnotTheory.enlargeBlock {R : Type u_1} [CommRing R] {ι : Type u_2} (ξ : ι → R) : Matrix ι (Fin 2) R

The two extra columns of an enlargement: a chosen vector ξ in the first, zero in the second.

Equations

• TauCeti.KnotTheory.enlargeBlock ξ = Matrix.of fun (i : ι) => ![ξ i, 0]

@[simp]

theorem TauCeti.KnotTheory.enlargeBlock_apply_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (ξ : ι → R) (i : ι) : enlargeBlock ξ i 0 = ξ i

The first column of the enlargement block is ξ.

@[simp]

theorem TauCeti.KnotTheory.enlargeBlock_apply_one {R : Type u_1} [CommRing R] {ι : Type u_2} (ξ : ι → R) (i : ι) : enlargeBlock ξ i 1 = 0

The second column of the enlargement block vanishes.

def TauCeti.KnotTheory.enlargeColumn {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) : Matrix (ι ⊕ Fin 2) (ι ⊕ Fin 2) R

The column enlargement of a Seifert matrix by a vector ξ, the block matrix

⎛ V  ξ  0 ⎞
⎜ 0  0  1 ⎟
⎝ 0  0  0 ⎠

Adding a tube to a Seifert surface changes its Seifert matrix by this move (or by the transposed move TauCeti.KnotTheory.enlargeRow) up to a change of basis, and the two enlargements together with congruence are what generate S-equivalence of Seifert matrices.

Equations

• TauCeti.KnotTheory.enlargeColumn V ξ = Matrix.fromBlocks V (TauCeti.KnotTheory.enlargeBlock ξ) 0 !![0, 1; 0, 0]

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inl_inl {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) (i j : ι) : enlargeColumn V ξ (Sum.inl i) (Sum.inl j) = V i j

The old block of a column enlargement is the original matrix.

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inl_inr_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) (i : ι) : enlargeColumn V ξ (Sum.inl i) (Sum.inr 0) = ξ i

The first new column of a column enlargement is ξ.

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inl_inr_one {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) (i : ι) : enlargeColumn V ξ (Sum.inl i) (Sum.inr 1) = 0

The second new column of a column enlargement vanishes on the old rows.

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inr_inl {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) (i : Fin 2) (j : ι) : enlargeColumn V ξ (Sum.inr i) (Sum.inl j) = 0

The new rows of a column enlargement vanish on the old columns.

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inr_zero_inr_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) : enlargeColumn V ξ (Sum.inr 0) (Sum.inr 0) = 0

The new 2 × 2 block of a column enlargement, at (0, 0).

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inr_zero_inr_one {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) : enlargeColumn V ξ (Sum.inr 0) (Sum.inr 1) = 1

The new 2 × 2 block of a column enlargement, at (0, 1): the single new 1.

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inr_one_inr_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) : enlargeColumn V ξ (Sum.inr 1) (Sum.inr 0) = 0

The new 2 × 2 block of a column enlargement, at (1, 0).

@[simp]

theorem TauCeti.KnotTheory.enlargeColumn_apply_inr_one_inr_one {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) : enlargeColumn V ξ (Sum.inr 1) (Sum.inr 1) = 0

The new 2 × 2 block of a column enlargement, at (1, 1).

@[simp]

theorem TauCeti.KnotTheory.map_enlargeColumn {R : Type u_1} [CommRing R] {ι : Type u_2} {S : Type u_3} [CommRing S] (f : R →+* S) (V : Matrix ι ι R) (xi : ι → R) : (enlargeColumn V xi).map ⇑f = enlargeColumn (V.map ⇑f) (⇑f ∘ xi)

Ring homomorphisms commute with column enlargement.

def TauCeti.KnotTheory.enlargeRow {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) : Matrix (ι ⊕ Fin 2) (ι ⊕ Fin 2) R

The row enlargement of a Seifert matrix by a vector η, the transpose of the column enlargement, that is the block matrix

⎛ V  0  0 ⎞
⎜ η  0  0 ⎟
⎝ 0  1  0 ⎠

Equations

• TauCeti.KnotTheory.enlargeRow V η = Matrix.fromBlocks V 0 (TauCeti.KnotTheory.enlargeBlock η).transpose !![0, 0; 1, 0]

theorem TauCeti.KnotTheory.enlargeRow_def {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) : enlargeRow V η = (enlargeColumn V.transpose η).transpose

A row enlargement is the transpose of the column enlargement of the transpose.

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inl_inl {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) (i j : ι) : enlargeRow V η (Sum.inl i) (Sum.inl j) = V i j

The old block of a row enlargement is the original matrix.

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inl_inr {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) (i : ι) (j : Fin 2) : enlargeRow V η (Sum.inl i) (Sum.inr j) = 0

The new columns of a row enlargement vanish on the old rows.

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inr_zero_inl {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) (j : ι) : enlargeRow V η (Sum.inr 0) (Sum.inl j) = η j

The first new row of a row enlargement is η.

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inr_one_inl {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) (j : ι) : enlargeRow V η (Sum.inr 1) (Sum.inl j) = 0

The second new row of a row enlargement vanishes on the old columns.

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inr_zero_inr_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) : enlargeRow V η (Sum.inr 0) (Sum.inr 0) = 0

The new 2 × 2 block of a row enlargement, at (0, 0).

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inr_zero_inr_one {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) : enlargeRow V η (Sum.inr 0) (Sum.inr 1) = 0

The new 2 × 2 block of a row enlargement, at (0, 1).

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inr_one_inr_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) : enlargeRow V η (Sum.inr 1) (Sum.inr 0) = 1

The new 2 × 2 block of a row enlargement, at (1, 0): the single new 1.

@[simp]

theorem TauCeti.KnotTheory.enlargeRow_apply_inr_one_inr_one {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (η : ι → R) : enlargeRow V η (Sum.inr 1) (Sum.inr 1) = 0

The new 2 × 2 block of a row enlargement, at (1, 1).

@[simp]

theorem TauCeti.KnotTheory.map_enlargeRow {R : Type u_1} [CommRing R] {ι : Type u_2} {S : Type u_3} [CommRing S] (f : R →+* S) (V : Matrix ι ι R) (eta : ι → R) : (enlargeRow V eta).map ⇑f = enlargeRow (V.map ⇑f) (⇑f ∘ eta)

Ring homomorphisms commute with row enlargement.

def TauCeti.KnotTheory.enlargeColumnFin {R : Type u_1} [CommRing R] {n : ℕ} (V : Matrix (Fin n) (Fin n) R) (xi : Fin n → R) : Matrix (Fin (n + 2)) (Fin (n + 2)) R

A column enlargement, reindexed onto the canonical finite type of the enlarged size.

Equations

• TauCeti.KnotTheory.enlargeColumnFin V xi = (TauCeti.KnotTheory.enlargeColumn V xi).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

theorem TauCeti.KnotTheory.enlargeColumnFin_def {R : Type u_1} [CommRing R] {n : ℕ} (V : Matrix (Fin n) (Fin n) R) (xi : Fin n → R) : enlargeColumnFin V xi = (enlargeColumn V xi).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

The defining formula for a canonically reindexed column enlargement.

def TauCeti.KnotTheory.enlargeRowFin {R : Type u_1} [CommRing R] {n : ℕ} (V : Matrix (Fin n) (Fin n) R) (eta : Fin n → R) : Matrix (Fin (n + 2)) (Fin (n + 2)) R

A row enlargement, reindexed onto the canonical finite type of the enlarged size.

Equations

• TauCeti.KnotTheory.enlargeRowFin V eta = (TauCeti.KnotTheory.enlargeRow V eta).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

theorem TauCeti.KnotTheory.enlargeRowFin_def {R : Type u_1} [CommRing R] {n : ℕ} (V : Matrix (Fin n) (Fin n) R) (eta : Fin n → R) : enlargeRowFin V eta = (enlargeRow V eta).submatrix ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

The defining formula for a canonically reindexed row enlargement.

@[simp]

theorem TauCeti.KnotTheory.map_enlargeColumnFin {R : Type u_1} [CommRing R] {S : Type u_3} [CommRing S] {n : ℕ} (f : R →+* S) (V : Matrix (Fin n) (Fin n) R) (xi : Fin n → R) : (enlargeColumnFin V xi).map ⇑f = enlargeColumnFin (V.map ⇑f) (⇑f ∘ xi)

Ring homomorphisms commute with canonically reindexed column enlargement.

@[simp]

theorem TauCeti.KnotTheory.map_enlargeRowFin {R : Type u_1} [CommRing R] {S : Type u_3} [CommRing S] {n : ℕ} (f : R →+* S) (V : Matrix (Fin n) (Fin n) R) (eta : Fin n → R) : (enlargeRowFin V eta).map ⇑f = enlargeRowFin (V.map ⇑f) (⇑f ∘ eta)

Ring homomorphisms commute with canonically reindexed row enlargement.

theorem TauCeti.KnotTheory.alexanderMatrix_enlargeColumn {R : Type u_1} [CommRing R] {ι : Type u_2} (V : Matrix ι ι R) (ξ : ι → R) : alexanderMatrix (enlargeColumn V ξ) = Matrix.fromBlocks (alexanderMatrix V) (LaurentPolynomial.T 1 • (enlargeBlock ξ).map ⇑LaurentPolynomial.C) (-((enlargeBlock ξ).map ⇑LaurentPolynomial.C).transpose) !![0, LaurentPolynomial.T 1; -1, 0]

The Alexander matrix of a column enlargement, in blocks. The bottom-right block is the only new content: it is invertible with determinant T, which is where the extra factor of T in TauCeti.KnotTheory.det_alexanderMatrix_enlargeColumn comes from.

theorem TauCeti.KnotTheory.alexanderMatrix_congruence {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (P V : Matrix ι ι R) : alexanderMatrix (P * V * P.transpose) = P.map ⇑LaurentPolynomial.C * alexanderMatrix V * (P.map ⇑LaurentPolynomial.C).transpose

Congruence of matrices is congruence of Alexander matrices.

theorem TauCeti.KnotTheory.det_alexanderMatrix_transpose {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) : (alexanderMatrix V.transpose).det = (alexanderMatrix V).det

Transposing a matrix does not change its Alexander determinant.

theorem TauCeti.KnotTheory.invert_det_alexanderMatrix {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) : LaurentPolynomial.invert (alexanderMatrix V).det = (-1) ^ Fintype.card ι * LaurentPolynomial.T (-↑(Fintype.card ι)) * (alexanderMatrix V).det

Substituting T⁻¹ for T multiplies the unnormalised Alexander determinant by (-1) ^ n * T ^ (-n), where n is the size of the matrix.

theorem TauCeti.KnotTheory.det_alexanderMatrix_congruence {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (P V : Matrix ι ι R) : (alexanderMatrix (P * V * P.transpose)).det = LaurentPolynomial.C P.det ^ 2 * (alexanderMatrix V).det

Congruence multiplies the Alexander determinant by the square of the determinant of the congruence matrix.

noncomputable def TauCeti.KnotTheory.alexander {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) : LaurentPolynomial R

The Conway-normalised Alexander polynomial of a Seifert matrix V: the determinant of t^(1/2) V - t^(-1/2) Vᵀ, written without half-integer powers as T ^ (-g) * det (T • V - Vᵀ) for V of size 2 * g.

A Seifert matrix always has even size, so Fintype.card ι / 2 is the genus g of the underlying Seifert surface; the results below that depend on the size being even take Fintype.card ι = 2 * g as an explicit hypothesis.

Equations

• TauCeti.KnotTheory.alexander V = LaurentPolynomial.T (-↑(Fintype.card ι / 2)) * (TauCeti.KnotTheory.alexanderMatrix V).det

theorem TauCeti.KnotTheory.alexander_def {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) : alexander V = LaurentPolynomial.T (-↑(Fintype.card ι / 2)) * (alexanderMatrix V).det

The defining formula for the Alexander polynomial of an arbitrary finite matrix.

@[simp]

theorem TauCeti.KnotTheory.map_alexander {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Type u_3} [CommRing S] (g : R →+* S) (V : Matrix ι ι R) : (AddMonoidAlgebra.mapRingHom ℤ g) (alexander V) = alexander (V.map ⇑g)

Transporting coefficients of the Alexander polynomial agrees with transporting the entries of the underlying matrix.

theorem TauCeti.KnotTheory.eval₂_alexander {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Type u_3} [CommRing S] (f : R →+* S) (x : Sˣ) (V : Matrix ι ι R) : (LaurentPolynomial.eval₂ f x) (alexander V) = ↑(x ^ (-↑(Fintype.card ι / 2))) * (↑x • V.map ⇑f - (V.map ⇑f).transpose).det

The value of the normalized Alexander polynomial at a unit parameter, expressed as the determinant of the evaluated Alexander matrix.

@[simp]

theorem TauCeti.KnotTheory.eval₂_alexander_map {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Type u_3} {A : Type u_4} [CommRing S] [CommRing A] (f : S →+* A) (g : R →+* S) (x : Aˣ) (V : Matrix ι ι R) : (LaurentPolynomial.eval₂ f x) (alexander (V.map ⇑g)) = (LaurentPolynomial.eval₂ (f.comp g) x) (alexander V)

Mapping the coefficients before evaluating the Alexander polynomial agrees with composing the coefficient homomorphisms.

theorem TauCeti.KnotTheory.alexander_eq_of_card {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {g : ℕ} (V : Matrix ι ι R) (h : Fintype.card ι = 2 * g) : alexander V = LaurentPolynomial.T (-↑g) * (alexanderMatrix V).det

The Alexander polynomial of a matrix of size 2 * g, with the genus g named.

theorem TauCeti.KnotTheory.invert_alexander {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {g : ℕ} (V : Matrix ι ι R) (h : Fintype.card ι = 2 * g) : LaurentPolynomial.invert (alexander V) = alexander V

The Alexander polynomial is symmetric: Δ(t⁻¹) = Δ(t). This is exactly what the normalisation T ^ (-g) buys, and it needs the size of the Seifert matrix to be even.

theorem TauCeti.KnotTheory.alexander_congruence {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (P V : Matrix ι ι R) : alexander (P * V * P.transpose) = LaurentPolynomial.C P.det ^ 2 * alexander V

Congruence multiplies the Alexander polynomial by the square of the determinant of the congruence matrix.

theorem TauCeti.KnotTheory.alexander_congruence_of_det_sq_eq_one {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {P : Matrix ι ι R} (V : Matrix ι ι R) (hP : P.det ^ 2 = 1) : alexander (P * V * P.transpose) = alexander V

The Alexander polynomial is a congruence invariant as soon as the determinant of the congruence matrix squares to 1: alexander (P * V * Pᵀ) = alexander V.

The hypothesis P.det ^ 2 = 1 is not automatic for an invertible P over an arbitrary commutative ring, where P.det need only be a unit; it is automatic in the knot-theoretic case R = ℤ, where a change of basis of the first homology of the Seifert surface is a matrix in GL (2 * g) ℤ and so has determinant ±1.

@[simp]

theorem TauCeti.KnotTheory.alexander_transpose {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) : alexander V.transpose = alexander V

Reversing the orientation of the Seifert surface transposes its Seifert matrix and leaves the Alexander polynomial unchanged.

theorem TauCeti.KnotTheory.eval₂_one_alexander {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) : (LaurentPolynomial.eval₂ (RingHom.id R) 1) (alexander V) = (V - V.transpose).det

Δ(1) is the determinant of the intersection form V - Vᵀ of the Seifert surface. For a knot that form is unimodular, so Δ(1) = ±1.

@[simp]

theorem TauCeti.KnotTheory.alexander_of_isEmpty {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [IsEmpty ι] (V : Matrix ι ι R) : alexander V = 1

The empty Seifert matrix, that of a disc, has Alexander polynomial 1: the unknot is normalised to Δ = 1.

theorem TauCeti.KnotTheory.det_alexanderMatrix_enlargeColumn {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) (ξ : ι → R) : (alexanderMatrix (enlargeColumn V ξ)).det = LaurentPolynomial.T 1 * (alexanderMatrix V).det

The unnormalised Alexander determinant picks up exactly one factor of T under a column enlargement.

theorem TauCeti.KnotTheory.det_alexanderMatrix_enlargeRow {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) (η : ι → R) : (alexanderMatrix (enlargeRow V η)).det = LaurentPolynomial.T 1 * (alexanderMatrix V).det

The unnormalised Alexander determinant picks up exactly one factor of T under a row enlargement.

@[simp]

theorem TauCeti.KnotTheory.alexander_enlargeColumn {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) (ξ : ι → R) : alexander (enlargeColumn V ξ) = alexander V

The Alexander polynomial is unchanged by a column enlargement of the Seifert matrix. The extra factor of T in the determinant is exactly cancelled by the genus going up by one.

@[simp]

theorem TauCeti.KnotTheory.alexander_enlargeRow {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (V : Matrix ι ι R) (η : ι → R) : alexander (enlargeRow V η) = alexander V

The Alexander polynomial is unchanged by a row enlargement of the Seifert matrix.

theorem TauCeti.KnotTheory.alexander_fin_two {R : Type u_1} [CommRing R] (V : Matrix (Fin 2) (Fin 2) R) : alexander V = (LaurentPolynomial.T 1 - 2 + LaurentPolynomial.T (-1)) * LaurentPolynomial.C (V 0 0) * LaurentPolynomial.C (V 1 1) - (LaurentPolynomial.T 1 + LaurentPolynomial.T (-1)) * LaurentPolynomial.C (V 0 1) * LaurentPolynomial.C (V 1 0) + (LaurentPolynomial.C (V 0 1) ^ 2 + LaurentPolynomial.C (V 1 0) ^ 2)

The Alexander polynomial of a genus-one Seifert matrix: for V = !![a, b; c, d],

Δ = (t - 2 + t⁻¹) * a * d - (t + t⁻¹) * b * c + b ^ 2 + c ^ 2.

This is the closed form behind the trefoil and figure-eight computations below.

def TauCeti.KnotTheory.trefoilSeifertMatrix : Matrix (Fin 2) (Fin 2) ℤ

The Seifert matrix of the right-handed trefoil, read off the standard genus-one Seifert surface (Lickorish, An Introduction to Knot Theory, Chapter 6).

Equations

• TauCeti.KnotTheory.trefoilSeifertMatrix = !![-1, 1; 0, -1]

@[simp]

theorem TauCeti.KnotTheory.trefoilSeifertMatrix_apply (i j : Fin 2) : trefoilSeifertMatrix i j = !![-1, 1; 0, -1] i j

The entries of the right-handed trefoil's Seifert matrix.

@[simp]

theorem TauCeti.KnotTheory.map_trefoilSeifertMatrix {S : Type u_3} [AddGroupWithOne S] : trefoilSeifertMatrix.map Int.cast = !![-1, 1; 0, -1]

The right-handed trefoil's Seifert matrix, read in an arbitrary additive group with one.

def TauCeti.KnotTheory.figureEightSeifertMatrix : Matrix (Fin 2) (Fin 2) ℤ

The Seifert matrix of the figure-eight knot, read off the standard genus-one Seifert surface.

Equations

• TauCeti.KnotTheory.figureEightSeifertMatrix = !![1, 1; 0, -1]

@[simp]

theorem TauCeti.KnotTheory.figureEightSeifertMatrix_apply (i j : Fin 2) : figureEightSeifertMatrix i j = !![1, 1; 0, -1] i j

The entries of the figure-eight knot's Seifert matrix.

@[simp]

theorem TauCeti.KnotTheory.map_figureEightSeifertMatrix {S : Type u_3} [AddGroupWithOne S] : figureEightSeifertMatrix.map Int.cast = !![1, 1; 0, -1]

The figure-eight knot's Seifert matrix, read in an arbitrary additive group with one.

theorem TauCeti.KnotTheory.alexander_trefoilSeifertMatrix : alexander trefoilSeifertMatrix = LaurentPolynomial.T 1 - 1 + LaurentPolynomial.T (-1)

The Alexander polynomial of the right-handed trefoil is t - 1 + t⁻¹.

theorem TauCeti.KnotTheory.alexander_figureEightSeifertMatrix : alexander figureEightSeifertMatrix = -LaurentPolynomial.T 1 + 3 - LaurentPolynomial.T (-1)

The Alexander polynomial of the figure-eight knot is -t + 3 - t⁻¹.