Recognising elementary enlargements up to congruence

The row enlargement TauCeti.KnotTheory.enlargeRow V η adds two basis vectors a = inr 0 and b = inr 1 to the basis of V: the column of b vanishes, and the row of b is the coordinate vector of a. Adding a tube to a Seifert surface produces exactly this pattern, with b the meridian of the tube and a a curve running once along it, but only after a change of basis: in a basis adapted to the surface, the row of the meridian is in general a unit multiple of the coordinate vector of the dual curve, and the other basis curves still link the dual curve.

This file shows that the pattern on the new basis vector b alone already forces the shape of an enlargement up to unimodular congruence: subtracting multiples of b from the other basis vectors clears their linking with a, and rescaling a normalises the unit. The transposed statement gives the column enlargement TauCeti.KnotTheory.enlargeColumn.

Main results

• TauCeti.KnotTheory.exists_mul_mul_transpose_eq_enlargeRow: a matrix in which the column of inr 1 vanishes and its row is a unit multiple of the coordinate vector of inr 0 is congruent, by a matrix with unit determinant, to the row enlargement of its upper left block.
• TauCeti.KnotTheory.exists_mul_mul_transpose_eq_enlargeColumn: the transposed statement.

References

• W. B. R. Lickorish, An Introduction to Knot Theory, Springer GTM 175 (1997), Chapter 8 (S-equivalence of Seifert matrices).

theorem TauCeti.KnotTheory.exists_mul_mul_transpose_eq_enlargeRow {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (W : Matrix (ι ⊕ Fin 2) (ι ⊕ Fin 2) R) {s : Rˣ} (hrow : W (Sum.inr 1) = Pi.single (Sum.inr 0) ↑s) (hcol : ∀ (i : ι ⊕ Fin 2), W i (Sum.inr 1) = 0) : ∃ (P : Matrix (ι ⊕ Fin 2) (ι ⊕ Fin 2) R) (η : ι → R), IsUnit P.det ∧ P * W * P.transpose = enlargeRow W.toBlocks₁₁ η

Recognising a row enlargement. If the column of inr 1 vanishes and the row of inr 1 is a unit s times the coordinate vector of inr 0, then W is congruent, by a matrix with unit determinant, to the row enlargement of its upper left block.

theorem TauCeti.KnotTheory.exists_mul_mul_transpose_eq_enlargeColumn {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (W : Matrix (ι ⊕ Fin 2) (ι ⊕ Fin 2) R) {s : Rˣ} (hcol : W.col (Sum.inr 1) = Pi.single (Sum.inr 0) ↑s) (hrow : ∀ (j : ι ⊕ Fin 2), W (Sum.inr 1) j = 0) : ∃ (P : Matrix (ι ⊕ Fin 2) (ι ⊕ Fin 2) R) (ξ : ι → R), IsUnit P.det ∧ P * W * P.transpose = enlargeColumn W.toBlocks₁₁ ξ

Recognising a column enlargement. If the row of inr 1 vanishes and the column of inr 1 is a unit s times the coordinate vector of inr 0, then W is congruent, by a matrix with unit determinant, to the column enlargement of its upper left block.