The Seifert matrix of a closed braid

Seifert's algorithm applied to the closure of a braid word w = σ_{i₁}^{ε₁} ⋯ σ_{iₖ}^{εₖ} on n strands produces a canonical Seifert surface: n parallel discs D₀, …, D_{n-1} stacked along the braid axis, one for each strand position, and one half-twisted band for each letter, the t-th letter σ_i^ε joining Dᵢ to D_{i+1} with a half twist of sign ε. The letters on a fixed level i are its bands between Dᵢ and D_{i+1}; two consecutive ones, at positions t < t' of the word with no letter of level i in between, span a loop γ_{t,t'} that runs up the band t, along D_{i+1}, down the band t' and back along Dᵢ. These loops form a basis of the first homology of the surface, and this file records the Seifert matrix V(γ, γ') = lk(γ, γ'⁺) in that basis, with γ'⁺ the push-off of γ' along the positive normal of the surface (the boundary orientation of every disc agreeing with the orientation of the braid).

Writing γ = γ_{t₁,t₂} and γ' = γ_{s₁,s₂}, the entries are as follows.

• On the diagonal, V(γ, γ) = -ε if both bands of γ have the same sign ε, and 0 otherwise: each half twist of sign ε contributes -ε / 2.
• For two loops on the same level sharing a band, t₂ = s₁ with the shared band of sign ε: V(γ, γ') = -1 and V(γ', γ) = 0 if ε = -1, while V(γ, γ') = 0 and V(γ', γ) = 1 if ε = 1. In both cases V(γ, γ') - V(γ', γ) = -1: the two loops cross once inside the shared band.
• For γ one level above γ', V(γ, γ') is -1 if s₁ < t₁ < s₂ < t₂, 1 if t₁ < s₁ < t₂ < s₂, and 0 otherwise; the two loops cross on their common disc exactly when their bands interleave. In the other order the entry vanishes: γ' lies on or below the disc they share, and the push-off of γ lies above it.
• All other entries vanish.

Positions in the word are natural numbers and a loop is labelled by the pair (t, t') of its positions, so that the operations below, which move letters around, act on loop labels by renaming positions. The matrix is indexed by the finite set TauCeti.BraidWord.seifertLoops w of these labels; for a braid closing up to a knot, every level is used and the surface has genus g, so there are 2 * g loops.

The normalisation is pinned by the two classical examples: σ₁³ (the right-handed trefoil) gives the transpose of TauCeti.KnotTheory.trefoilSeifertMatrix, so Alexander polynomial t - 1 + t⁻¹ and signature -2, and σ₁ σ₂⁻¹ σ₁ σ₂⁻¹ (the figure-eight knot) gives a matrix congruent to TauCeti.KnotTheory.figureEightSeifertMatrix, so Alexander polynomial -t + 3 - t⁻¹ and signature 0.

Up to relabelling the loops, the Seifert matrix does not change when two letters on distant levels are exchanged, nor under the Markov stabilization w ↦ w σₙ^{±1}, which adds one disc and one band and no new loop.

Cyclic rotation x :: v ↦ v ++ [x] cuts the same closed braid at another place, so the surface is the same, but the basis of loops changes on the level l of x: the loop through the first two letters of level l is replaced by the loop through the last letter of level l and the moved letter. The loops of level l around the braid axis sum to zero in the homology of the surface, so the new loop is minus the sum of the old ones, and the Seifert matrix changes by the corresponding unimodular congruence V ↦ P V Pᵀ. To check this from the entries above, note that for a fixed loop b the entries V(c, b) and V(b, c), as c runs over the loops of level l, are differences f c.2 - f c.1 of an explicit function of positions, so their sum over c telescopes along the letters of level l.

The canonical surface is connected exactly when every level 0, …, n - 2 carries a letter, and only then is the matrix a Seifert matrix of the closure in the sense of S-equivalence. If some level carries no letter, the surface is disconnected and the matrix forgets the splitting: on two strands, the empty word gives the 0 × 0 matrix while σ₁ σ₁⁻¹ gives [0], although both close to the two-component unlink. Among words using every level, the remaining moves generating Markov equivalence of braid words (the braid relation, and free cancellation that keeps every level used) change the matrix only up to S-equivalence, as for any two Seifert matrices of isotopic links; that is what makes its Alexander polynomial an invariant of the closure. The Tristram–Levine signatures need no condition on the levels: free cancellation on an unused level only adds a zero row and column, so for every word they are invariant under Markov equivalence (TauCeti.MarkovEquiv.tristramLevineSignature_eq in TauCeti.KnotTheory.Markov.TristramLevine). Those comparisons are not made here.

Main definitions

• TauCeti.BraidWord.IsSeifertLoop: a pair of positions holding consecutive letters of one level.
• TauCeti.BraidWord.seifertLoops: the finite set of these pairs, the basis loops of the canonical Seifert surface.
• TauCeti.BraidWord.seifertMatrix: the Seifert matrix of the closure in this basis.

Main results

• TauCeti.BraidWord.seifertMatrix_apply: the entries of the Seifert matrix.
• TauCeti.BraidWord.exists_seifertMatrix_append_cons_cons_comm: exchanging adjacent letters on distant levels relabels the Seifert matrix.
• TauCeti.BraidWord.exists_seifertMatrix_stabilize: so does Markov stabilization.
• TauCeti.BraidWord.exists_seifertMatrix_append_cons_of_not_exists: so does changing the sign of a letter alone on its level, whose band lies on no loop.
• TauCeti.BraidWord.exists_seifertMatrix_append_singleton: moving the first letter to the end changes the Seifert matrix by a unimodular congruence.
• TauCeti.BraidWord.alexander_seifertMatrix_rotate and TauCeti.BraidWord.tristramLevineSignature_seifertMatrix_rotate: so cyclic rotation of the word keeps the Alexander polynomial and the Tristram–Levine signatures of the Seifert matrix.
• TauCeti.BraidWord.alexander_seifertMatrix_trefoil and TauCeti.BraidWord.signature_seifertMatrix_trefoil: the right-handed trefoil.
• TauCeti.BraidWord.alexander_seifertMatrix_mirrorTrefoil and TauCeti.BraidWord.signature_seifertMatrix_mirrorTrefoil: the left-handed trefoil.
• TauCeti.BraidWord.alexander_seifertMatrix_figureEight and TauCeti.BraidWord.signature_seifertMatrix_figureEight: the figure-eight knot.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 2 (Seifert's algorithm) and Chapter 6 (Seifert matrices).
• J. Birman, Braids, Links, and Mapping Class Groups, Annals of Mathematics Studies 82 (1974), Chapter 2 (braids and links).
• H. Seifert, Über das Geschlecht von Knoten, Math. Ann. 110 (1935), 571–592.

def TauCeti.BraidWord.IsSeifertLoop {n : ℕ} (w : BraidWord n) (p : ℕ × ℕ) : Prop

The pair of positions p = (t, t') labels a loop of the canonical Seifert surface: t < t' are positions of the word holding letters of the same level, with no letter of that level in between. The loop runs up the band t and down the band t'.

theorem TauCeti.BraidWord.isSeifertLoop_iff {n : ℕ} (w : BraidWord n) {p : ℕ × ℕ} : w.IsSeifertLoop p ↔ p.1 < p.2 ∧ p.2 < List.length w ∧ w.levelAt p.2 = w.levelAt p.1 ∧ ∀ k < p.2, p.1 < k → w.levelAt k ≠ w.levelAt p.1

The defining property of a loop label.

theorem TauCeti.BraidWord.IsSeifertLoop.fst_lt_snd {n : ℕ} {w : BraidWord n} {p : ℕ × ℕ} (h : w.IsSeifertLoop p) : p.1 < p.2

The two bands of a loop are in order.

theorem TauCeti.BraidWord.IsSeifertLoop.snd_lt_length {n : ℕ} {w : BraidWord n} {p : ℕ × ℕ} (h : w.IsSeifertLoop p) : p.2 < List.length w

The second band of a loop is a letter of the word.

theorem TauCeti.BraidWord.IsSeifertLoop.fst_lt_length {n : ℕ} {w : BraidWord n} {p : ℕ × ℕ} (h : w.IsSeifertLoop p) : p.1 < List.length w

The first band of a loop is a letter of the word.

theorem TauCeti.BraidWord.IsSeifertLoop.eq_of_fst_eq {n : ℕ} {w : BraidWord n} {p q : ℕ × ℕ} (hp : w.IsSeifertLoop p) (hq : w.IsSeifertLoop q) (h : p.1 = q.1) : p = q

A loop is determined by its first band.

@[instance_reducible]

instance TauCeti.BraidWord.instDecidablePredProdNatIsSeifertLoop {n : ℕ} (w : BraidWord n) : DecidablePred w.IsSeifertLoop

def TauCeti.BraidWord.seifertLoops {n : ℕ} (w : BraidWord n) : Finset (ℕ × ℕ)

The labels of the basis loops of the first homology of the canonical Seifert surface of the closure of w: the pairs of consecutive positions of letters on a common level.

@[simp]

theorem TauCeti.BraidWord.mem_seifertLoops {n : ℕ} (w : BraidWord n) {p : ℕ × ℕ} : p ∈ w.seifertLoops ↔ w.IsSeifertLoop p

instance TauCeti.BraidWord.isEmpty_seifertLoops_nil {n : ℕ} : IsEmpty ↥(seifertLoops [])

The empty braid word has no basis loops, regardless of its strand count.

theorem TauCeti.BraidWord.isSeifertLoop_append_singleton_iff {n : ℕ} (w : BraidWord n) (y : Fin (n - 1) × ℤˣ) {p : ℕ × ℕ} (hp : p.2 < List.length w) : (w ++ [y]).IsSeifertLoop p ↔ w.IsSeifertLoop p

A loop of w ++ [y] not running through the appended letter is a loop of w.

theorem TauCeti.BraidWord.mem_seifertLoops_append_singleton_iff {n : ℕ} (w : BraidWord n) (i : Fin (n - 1)) (ε ε' : ℤˣ) (p : ℕ × ℕ) : p ∈ (w ++ [(i, ε)]).seifertLoops ↔ p ∈ (w ++ [(i, ε')]).seifertLoops

The loops of w ++ [(i, ε)] do not depend on the sign ε of the appended letter.

def TauCeti.BraidWord.seifertMatrix {n : ℕ} (w : BraidWord n) : Matrix ↥w.seifertLoops ↥w.seifertLoops ℤ

The Seifert matrix of the closure of a braid word, read off the canonical Seifert surface of Seifert's algorithm in the basis of loops TauCeti.BraidWord.seifertLoops w. Its entry at a pair of loops (γ, γ') is the linking number of γ with the positive push-off of γ'.

theorem TauCeti.BraidWord.seifertMatrix_apply {n : ℕ} (w : BraidWord n) (a b : ↥w.seifertLoops) : w.seifertMatrix a b = if a = b then if w.signAt (↑a).1 = w.signAt (↑a).2 then -w.signAt (↑a).1 else 0 else if w.levelAt (↑a).1 = w.levelAt (↑b).1 then if (↑a).2 = (↑b).1 then if w.signAt (↑a).2 = -1 then -1 else 0 else if (↑b).2 = (↑a).1 then if w.signAt (↑a).1 = 1 then 1 else 0 else 0 else if w.levelAt (↑a).1 = Option.map (fun (x : ℕ) => x + 1) (w.levelAt (↑b).1) then if (↑b).1 < (↑a).1 ∧ (↑a).1 < (↑b).2 ∧ (↑b).2 < (↑a).2 then -1 else if (↑a).1 < (↑b).1 ∧ (↑b).1 < (↑a).2 ∧ (↑a).2 < (↑b).2 then 1 else 0 else 0

The entries of the Seifert matrix of a braid word. For loops a = (t₁, t₂) and b = (s₁, s₂): the diagonal records the signs of the two bands of a; loops on one level meet only when they share a band; and a loop meets the loops one level below it when their bands interleave.

@[simp]

theorem TauCeti.BraidWord.seifertMatrix_apply_self {n : ℕ} (w : BraidWord n) (a : ↥w.seifertLoops) : w.seifertMatrix a a = if w.signAt (↑a).1 = w.signAt (↑a).2 then -w.signAt (↑a).1 else 0

The diagonal entry at a loop whose two bands have the same sign ε is -ε.

theorem TauCeti.BraidWord.seifertMatrix_apply_eq_zero_of_levelAt_eq_map_succ {n : ℕ} (w : BraidWord n) {a b : ↥w.seifertLoops} (h : w.levelAt (↑b).1 = Option.map (fun (x : ℕ) => x + 1) (w.levelAt (↑a).1)) : w.seifertMatrix a b = 0

A loop has linking number zero with the push-off of a loop on the level above it.

Moving letters

The two lemmas below transport loops and entries along a renaming e of positions which keeps every letter and the order of any two letters on equal or adjacent levels: these are the only comparisons the definition makes.

theorem TauCeti.BraidWord.exists_seifertMatrix_append_cons_cons_comm {n : ℕ} (u v : BraidWord n) {a b : Fin (n - 1) × ℤˣ} (h : ↑a.1 + 2 ≤ ↑b.1 ∨ ↑b.1 + 2 ≤ ↑a.1) : ∃ (ι : ↥(u ++ b :: a :: v).seifertLoops ≃ ↥(u ++ a :: b :: v).seifertLoops), (u ++ b :: a :: v).seifertMatrix = (u ++ a :: b :: v).seifertMatrix.submatrix ⇑ι ⇑ι

Exchanging two adjacent letters on distant levels relabels the Seifert matrix. The two bands lie between disjoint pairs of discs, so exchanging them moves no loop across another.

theorem TauCeti.BraidWord.exists_seifertMatrix_stabilize {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) : ∃ (ι : ↥(w.stabilize ε).seifertLoops ≃ ↥w.seifertLoops), (w.stabilize ε).seifertMatrix = w.seifertMatrix.submatrix ⇑ι ⇑ι

Markov stabilization relabels the Seifert matrix. The new strand adds a disc and a single band joining it to the surface, which creates no loop.

theorem TauCeti.BraidWord.exists_seifertMatrix_append_cons_of_not_exists {n : ℕ} (u v : BraidWord n) (i : Fin (n - 1)) (ε ε' : ℤˣ) (h : ¬∃ x ∈ u ++ v, x.1 = i) : ∃ (ι : ↥(u ++ (i, ε') :: v).seifertLoops ≃ ↥(u ++ (i, ε) :: v).seifertLoops), (u ++ (i, ε') :: v).seifertMatrix = (u ++ (i, ε) :: v).seifertMatrix.submatrix ⇑ι ⇑ι

The sign of a letter alone on its level does not change the Seifert matrix. If no other letter lies on level i, the band of the letter σᵢ^ε is the only band between the discs Dᵢ and Dᵢ₊₁ of the canonical Seifert surface, so it lies on no loop, and changing its sign only relabels the loops.

Telescoping along a level

Seen from a fixed loop b, the entries V(c, b) and V(b, c) as c runs over the loops of one level are differences f c.2 - f c.1 of a function f of positions, so their sum telescopes along the letters of that level. This is what makes the Seifert matrix compatible with replacing a loop by minus the sum of all the others on its level, as cyclic rotation of the word does.

Cyclic rotation

Moving the first letter x of the word x :: v to the end gives v ++ [x], whose closure is the same diagram cut at a different place (TauCeti.BraidWord.closure_rotate). Seifert's algorithm gives the same surface, and the loops on the levels other than the level l of x are the same loops. On level l, the loop through the first two letters of level l disappears, and the loop through the last letter of level l and the moved letter x appears. The loops of level l, taken all the way around the braid axis, sum to zero in the first homology of the surface, so the new loop is minus the sum of the old loops of level l. This is a unimodular change of basis, and it carries the Seifert matrix of x :: v to that of v ++ [x].

theorem TauCeti.BraidWord.exists_seifertMatrix_append_singleton {n : ℕ} (x : Fin (n - 1) × ℤˣ) (v : BraidWord n) : ∃ (ι : ↥(v ++ [x]).seifertLoops ≃ ↥(seifertLoops (x :: v))) (P : Matrix ↥(seifertLoops (x :: v)) ↥(seifertLoops (x :: v)) ℤ), IsUnit P.det ∧ (v ++ [x]).seifertMatrix = (P * seifertMatrix (x :: v) * P.transpose).submatrix ⇑ι ⇑ι

Cyclic rotation is a unimodular change of basis of the Seifert matrix. Moving the first letter x of a braid word to the end changes the Seifert matrix of the canonical Seifert surface only by a congruence P V Pᵀ with P invertible over ℤ, followed by a relabelling of the loops. The loop through the last letter of the level of x and the moved letter x is minus the sum of the loops of that level in x :: v; every other loop is the same loop, one position earlier.

Consequences for the invariants

theorem TauCeti.BraidWord.alexander_seifertMatrix_append_cons_cons_comm {n : ℕ} {u v : BraidWord n} {a b : Fin (n - 1) × ℤˣ} (h : ↑a.1 + 2 ≤ ↑b.1 ∨ ↑b.1 + 2 ≤ ↑a.1) : KnotTheory.alexander (u ++ b :: a :: v).seifertMatrix = KnotTheory.alexander (u ++ a :: b :: v).seifertMatrix

Exchanging two adjacent letters on distant levels keeps the Alexander polynomial of the Seifert matrix.

theorem TauCeti.BraidWord.tristramLevineSignature_seifertMatrix_append_cons_cons_comm {n : ℕ} {u v : BraidWord n} {a b : Fin (n - 1) × ℤˣ} (h : ↑a.1 + 2 ≤ ↑b.1 ∨ ↑b.1 + 2 ≤ ↑a.1) (ω : ℂ) : KnotTheory.tristramLevineSignature ((u ++ b :: a :: v).seifertMatrix.map Int.cast) ω = KnotTheory.tristramLevineSignature ((u ++ a :: b :: v).seifertMatrix.map Int.cast) ω

Exchanging two adjacent letters on distant levels keeps the Tristram–Levine signatures of the Seifert matrix.

theorem TauCeti.BraidWord.alexander_seifertMatrix_stabilize {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) : KnotTheory.alexander (w.stabilize ε).seifertMatrix = KnotTheory.alexander w.seifertMatrix

Markov stabilization keeps the Alexander polynomial of the Seifert matrix.

theorem TauCeti.BraidWord.tristramLevineSignature_seifertMatrix_stabilize {n : ℕ} (w : BraidWord (n + 1)) (ε : ℤˣ) (ω : ℂ) : KnotTheory.tristramLevineSignature ((w.stabilize ε).seifertMatrix.map Int.cast) ω = KnotTheory.tristramLevineSignature (w.seifertMatrix.map Int.cast) ω

Markov stabilization keeps the Tristram–Levine signatures of the Seifert matrix.

theorem TauCeti.BraidWord.alexander_seifertMatrix_append_singleton {n : ℕ} (x : Fin (n - 1) × ℤˣ) (v : BraidWord n) : KnotTheory.alexander (v ++ [x]).seifertMatrix = KnotTheory.alexander (seifertMatrix (x :: v))

Moving the first letter of a braid word to the end keeps the Alexander polynomial of the Seifert matrix.

theorem TauCeti.BraidWord.tristramLevineSignature_seifertMatrix_append_singleton {n : ℕ} (x : Fin (n - 1) × ℤˣ) (v : BraidWord n) (ω : ℂ) : KnotTheory.tristramLevineSignature ((v ++ [x]).seifertMatrix.map Int.cast) ω = KnotTheory.tristramLevineSignature ((seifertMatrix (x :: v)).map Int.cast) ω

Moving the first letter of a braid word to the end keeps the Tristram–Levine signatures of the Seifert matrix.

@[simp]

theorem TauCeti.BraidWord.alexander_seifertMatrix_rotate {n : ℕ} (w : BraidWord n) (k : ℕ) : KnotTheory.alexander (seifertMatrix (List.rotate w k)) = KnotTheory.alexander w.seifertMatrix

Cyclically rotating a braid word keeps the Alexander polynomial of the Seifert matrix.

@[simp]

theorem TauCeti.BraidWord.tristramLevineSignature_seifertMatrix_rotate {n : ℕ} (w : BraidWord n) (k : ℕ) (ω : ℂ) : KnotTheory.tristramLevineSignature ((seifertMatrix (List.rotate w k)).map Int.cast) ω = KnotTheory.tristramLevineSignature (w.seifertMatrix.map Int.cast) ω

Cyclically rotating a braid word keeps the Tristram–Levine signatures of the Seifert matrix.

The trefoil and the figure-eight knot

theorem TauCeti.BraidWord.seifertMatrix_trefoil : ∃ (e : Fin 2 ≃ ↥(seifertLoops [(0, 1), (0, 1), (0, 1)])), (seifertMatrix [(0, 1), (0, 1), (0, 1)]).submatrix ⇑e ⇑e = KnotTheory.trefoilSeifertMatrix.transpose

The closure of σ₁³ is the right-handed trefoil. Its canonical Seifert surface has the two loops (0, 1) and (1, 2), and in that basis its Seifert matrix is the transpose of TauCeti.KnotTheory.trefoilSeifertMatrix.

theorem TauCeti.BraidWord.alexander_seifertMatrix_trefoil : KnotTheory.alexander (seifertMatrix [(0, 1), (0, 1), (0, 1)]) = LaurentPolynomial.T 1 - 1 + LaurentPolynomial.T (-1)

The Seifert matrix of the braid σ₁³ has the Alexander polynomial t - 1 + t⁻¹ of the trefoil.

theorem TauCeti.BraidWord.signature_seifertMatrix_trefoil {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] : ((seifertMatrix [(0, 1), (0, 1), (0, 1)]).map Int.cast).signature = -2

The Seifert matrix of the braid σ₁³ has the signature -2 of the right-handed trefoil.

theorem TauCeti.BraidWord.seifertMatrix_mirrorTrefoil : ∃ (e : Fin 2 ≃ ↥(seifertLoops [(0, -1), (0, -1), (0, -1)])), (seifertMatrix [(0, -1), (0, -1), (0, -1)]).submatrix ⇑e ⇑e = -KnotTheory.trefoilSeifertMatrix

The closure of σ₁⁻³ is the left-handed trefoil, the mirror image of the closure of σ₁³. Its canonical Seifert surface has the two loops (0, 1) and (1, 2), and in that basis its Seifert matrix is the negative of TauCeti.KnotTheory.trefoilSeifertMatrix.

theorem TauCeti.BraidWord.signature_seifertMatrix_mirrorTrefoil {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] : ((seifertMatrix [(0, -1), (0, -1), (0, -1)]).map Int.cast).signature = 2

The Seifert matrix of the braid σ₁⁻³ has the signature 2 of the left-handed trefoil.

theorem TauCeti.BraidWord.alexander_seifertMatrix_mirrorTrefoil : KnotTheory.alexander (seifertMatrix [(0, -1), (0, -1), (0, -1)]) = LaurentPolynomial.T 1 - 1 + LaurentPolynomial.T (-1)

The Seifert matrix of the braid σ₁⁻³ has the Alexander polynomial t - 1 + t⁻¹ of the left-handed trefoil, the same as for the right-handed one.

theorem TauCeti.BraidWord.seifertMatrix_figureEight : ∃ (e : Fin 2 ≃ ↥(seifertLoops [(0, 1), (1, -1), (0, 1), (1, -1)])), (seifertMatrix [(0, 1), (1, -1), (0, 1), (1, -1)]).submatrix ⇑e ⇑e = !![1, -1; 0, -1]

The closure of σ₁ σ₂⁻¹ σ₁ σ₂⁻¹ is the figure-eight knot. Its canonical Seifert surface has the loop (1, 3) on the upper level and (0, 2) on the lower one, and in that basis its Seifert matrix is !![1, -1; 0, -1], congruent to TauCeti.KnotTheory.figureEightSeifertMatrix by reversing the second loop.

theorem TauCeti.BraidWord.alexander_seifertMatrix_figureEight : KnotTheory.alexander (seifertMatrix [(0, 1), (1, -1), (0, 1), (1, -1)]) = -LaurentPolynomial.T 1 + 3 - LaurentPolynomial.T (-1)

The Seifert matrix of the braid σ₁ σ₂⁻¹ σ₁ σ₂⁻¹ has the Alexander polynomial -t + 3 - t⁻¹ of the figure-eight knot.

theorem TauCeti.BraidWord.signature_seifertMatrix_figureEight {𝕜 : Type u_1} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] : ((seifertMatrix [(0, 1), (1, -1), (0, 1), (1, -1)]).map Int.cast).signature = 0

The Seifert matrix of the braid σ₁ σ₂⁻¹ σ₁ σ₂⁻¹ has the signature 0 of the figure-eight knot.