The meridian of a knot and its preferred framing

Let Φ : D² × S¹ → X be a solid torus neighbourhood of a knot f : S¹ → X in a Hausdorff space whose first and second integral homology vanish, such as S³ or an integral homology sphere. The boundary torus T of the exterior of the knot is framed by Φ (TauCeti.IsSolidTorusNeighborhood.framedBoundaryTorus), with meridian μ and longitude λ. This file computes the map H₁(T; ℤ) → H₁(X ∖ K; ℤ) induced by the inclusion of T into the knot complement X ∖ K, K the image of f (TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap).

• The meridian generates H₁(X ∖ K). There is an isomorphism H₁(X ∖ K; ℤ) ≃ ℤ sending the class of the meridian to 1 (TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv). For a knot in S³ this is the linking number with the knot, oriented so that the meridian of Φ has linking number 1.
• The framing number. The longitude of Φ is homologous in X ∖ K to n times the meridian for a unique integer n, the framing number of Φ (TauCeti.IsSolidTorusNeighborhood.framingNumber); the class with (μ, λ)-coordinates (p, q) goes to p + n q.
• The preferred framing. Replacing the longitude by λ - n · μ gives the preferred framing (μ, λ₀) of the boundary torus (TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus). The preferred longitude λ₀ is null-homologous in X ∖ K, and it generates the kernel of H₁(T) → H₁(X ∖ K): in the preferred framing a class goes to its meridian coordinate. For a knot in S³ this is the classical Seifert framing, whose longitude bounds a Seifert surface (TauCeti.SeifertSurface, which this file does not use); the 0-framing of surgery theory and the ℚ ∪ {∞} surgery coefficients refer to it.

The homology hypotheses are stated for reduced singular homology in degrees 1 and 2. For the unit sphere of a four-dimensional real inner product space they are TauCeti.isZero_reducedSingularHomologyFunctor_sphere_of_ne, and a C² knot in it has solid torus neighbourhoods by TauCeti.exists_isSolidTorusNeighborhood_sphere.

The computation is the Mayer–Vietoris sequence of the cover of X by the open solid torus U = Φ (B² × S¹) and the knot complement X ∖ K. Their intersection is the punctured open solid torus Φ ((B² ∖ {0}) × S¹), which is homotopy equivalent to the torus S¹ × S¹ at radius 1 / 2. Since H₂(X) and H₁(X) vanish, H₁(U ∩ (X ∖ K)) ≅ H₁(U) ⊕ H₁(X ∖ K). The meridian dies in U, while the longitude survives in U, since it maps to a generator of H₁(S¹) under the projection of U to its core. Hence H₁(X ∖ K) is freely generated by the meridian at radius 1 / 2, which is homotopic in X ∖ K to the meridian on the boundary torus.

Main definitions

• TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap: the map H₁(T) → H₁(X ∖ K).
• TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv: the isomorphism H₁(X ∖ K) ≃ ℤ sending the meridian to 1.
• TauCeti.IsSolidTorusNeighborhood.framingNumber: the framing number of Φ.
• TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus: the preferred framing of the boundary torus.

Main results

• TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_basis_one_eq_zero_of_map: a null-homologous longitude stays null-homologous under a reparametrization of the core circle followed by a map of knot complements.
• TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_boundaryHomologyMap: a class with (μ, λ)-coordinates (p, q) goes to p + n q.
• TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_boundaryHomologyMap_preferred: a class goes to its meridian coordinate in the preferred framing.
• TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_preferredFramedBoundaryTorus_basis_one: the preferred longitude is null-homologous in the knot complement.
• TauCeti.IsSolidTorusNeighborhood.ker_boundaryHomologyMap: the preferred longitude generates the kernel of H₁(T) → H₁(X ∖ K).

References

• D. Rolfsen, Knots and Links, Publish or Perish (1976), Section 2E: meridians and longitudes of a solid torus, and Exercise 2E7 and Definition 2E8, the preferred framing of a solid torus in S³, whose longitude is the unique one homologically trivial in the exterior.
• A. Hatcher, Algebraic Topology, Section 2.2, the Mayer–Vietoris sequence.

The open and the punctured open solid torus

The Mayer–Vietoris computation

The meridian generates the homology of the knot complement

noncomputable def TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : h.framedBoundaryTorus.H →ₗ[ℤ] ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧↑(Set.range f)ᶜ) 1)

The map H₁(T; ℤ) → H₁(X ∖ K; ℤ) induced by the inclusion of the boundary torus T of the exterior of the knot K = range f into the knot complement.

theorem TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_def {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h : IsSolidTorusNeighborhood f Φ) : h.boundaryHomologyMap = ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map (TopCat.ofHom (ContinuousMap.inclusion ⋯))) 1)

TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap is induced by the inclusion of the boundary torus of the exterior into the knot complement.

theorem TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_basis_one_eq_zero_of_map {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] {Y : Type} [TopologicalSpace Y] [T2Space Y] {f' : Circle → Y} {Φ' : SolidTorus → Y} (h : IsSolidTorusNeighborhood f Φ) (h' : IsSolidTorusNeighborhood f' Φ') (g : C(Circle, Circle)) (m : C(↑(Set.range f)ᶜ, ↑(Set.range f')ᶜ)) (hm : ∀ (x : ↑(Set.range f)ᶜ) (q : Circle × Circle), ↑x = Φ (SolidTorus.boundaryInclusion (q.1, g q.2)) → ↑(m x) = Φ' (SolidTorus.boundaryInclusion q)) (hΦ : h.boundaryHomologyMap (h.framedBoundaryTorus.basis 1) = 0) : h'.boundaryHomologyMap (h'.framedBoundaryTorus.basis 1) = 0

A null-homologous longitude stays null-homologous under a reparametrization of the core circle followed by a map of knot complements. Let Φ' be a solid torus neighbourhood of a loop f' in a Hausdorff space Y, g a self-map of the circle and m a map from the complement of f to the complement of f' sending Φ (w, g z) to Φ' (w, z) on the boundary torus. If the longitude of Φ is null-homologous in the complement of f, then the longitude of Φ' is null-homologous in the complement of f'.

theorem TauCeti.IsSolidTorusNeighborhood.bijective_toSpanSingleton_boundaryHomologyMap_basis_zero {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : Function.Bijective ⇑(LinearMap.toSpanSingleton ℤ (↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧↑(Set.range f)ᶜ) 1)) (h.boundaryHomologyMap (h.framedBoundaryTorus.basis 0)))

Integer multiples of the boundary meridian parametrize the first homology of the knot complement bijectively.

noncomputable def TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : ↑(HomologicalComplex.homology ((singularChains ℤ).obj ↧↑(Set.range f)ᶜ) 1) ≃ₗ[ℤ] ℤ

The meridian generates the first homology of the knot complement. For a knot with a solid torus neighbourhood Φ in a Hausdorff space X with H₁(X; ℤ) = H₂(X; ℤ) = 0, the first integral homology of the knot complement is infinite cyclic, freely generated by the meridian of Φ: this isomorphism H₁(X ∖ K; ℤ) ≃ ℤ sends the meridian to 1 (TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_boundaryHomologyMap_basis_zero). For a knot in S³ it is the linking number with the knot, oriented so that the meridian of Φ has linking number 1.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_symm_apply {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) (k : ℤ) : (complementHomologyEquiv h₁ h₂ h).symm k = k • h.boundaryHomologyMap (h.framedBoundaryTorus.basis 0)

The inverse of TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv sends k to k times the meridian.

@[simp]

theorem TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_boundaryHomologyMap_basis_zero {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : (complementHomologyEquiv h₁ h₂ h) (h.boundaryHomologyMap (h.framedBoundaryTorus.basis 0)) = 1

The meridian goes to 1.

noncomputable def TauCeti.IsSolidTorusNeighborhood.framingNumber {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : ℤ

The framing number of the solid torus neighbourhood Φ: the longitude of Φ is homologous in the knot complement to framingNumber times the meridian. Equivalently, the longitude of Φ is λ₀ + n · μ for the preferred longitude λ₀ (TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus_basis_one). For a knot in S³ it is the linking number of the longitude of Φ with the knot.

theorem TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_framedBoundaryTorus_basis_one {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : h.boundaryHomologyMap (h.framedBoundaryTorus.basis 1) = framingNumber h₁ h₂ h • h.boundaryHomologyMap (h.framedBoundaryTorus.basis 0)

The longitude is homologous in the complement to the framing number times the meridian.

theorem TauCeti.IsSolidTorusNeighborhood.framingNumber_eq_iff {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) (n : ℤ) : framingNumber h₁ h₂ h = n ↔ h.boundaryHomologyMap (h.framedBoundaryTorus.basis 1) = n • h.boundaryHomologyMap (h.framedBoundaryTorus.basis 0)

The framing number is the unique integer relating the longitude and meridian in the homology of the knot complement.

theorem TauCeti.IsSolidTorusNeighborhood.framingNumber_eq_zero_iff {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : framingNumber h₁ h₂ h = 0 ↔ h.boundaryHomologyMap (h.framedBoundaryTorus.basis 1) = 0

The framing number vanishes exactly when the longitude is null-homologous in the knot complement, that is, when the framing is the preferred (Seifert) framing.

theorem TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_boundaryHomologyMap {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) (x : h.framedBoundaryTorus.H) : (complementHomologyEquiv h₁ h₂ h) (h.boundaryHomologyMap x) = (h.framedBoundaryTorus.coord x).1 + framingNumber h₁ h₂ h * (h.framedBoundaryTorus.coord x).2

A class of the boundary torus with (μ, λ)-coordinates (p, q) is homologous in the knot complement to p + n q times the meridian, n the framing number.

theorem TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_eq_zero_iff {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) (x : h.framedBoundaryTorus.H) : h.boundaryHomologyMap x = 0 ↔ (h.framedBoundaryTorus.coord x).1 + framingNumber h₁ h₂ h * (h.framedBoundaryTorus.coord x).2 = 0

A class of the boundary torus with (μ, λ)-coordinates (p, q) is null-homologous in the knot complement exactly when p + n q = 0, n the framing number.

The preferred framing

@[reducible, inline]

noncomputable abbrev TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : FramedBoundaryTorus

The preferred framing of the boundary torus of the exterior: the meridian μ of Φ together with the preferred longitude λ₀ = λ - n · μ, n the framing number of Φ. The preferred longitude is null-homologous in the knot complement (TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_preferredFramedBoundaryTorus_basis_one) and generates the kernel of H₁(T) → H₁(X ∖ K) (TauCeti.IsSolidTorusNeighborhood.ker_boundaryHomologyMap), so up to sign it is the only longitude completing μ to a basis that is null-homologous in the knot complement. For a knot in S³ this is the Seifert framing of surgery theory.

This is reducible so that its torus is the boundary torus of the exterior for consumers, and hence that classes of h.framedBoundaryTorus.H are classes of its homology.

theorem TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus_basis_zero {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : (preferredFramedBoundaryTorus h₁ h₂ h).basis 0 = h.framedBoundaryTorus.basis 0

The preferred framing keeps the meridian of Φ.

theorem TauCeti.IsSolidTorusNeighborhood.preferredFramedBoundaryTorus_basis_one {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : (preferredFramedBoundaryTorus h₁ h₂ h).basis 1 = h.framedBoundaryTorus.basis 1 - framingNumber h₁ h₂ h • h.framedBoundaryTorus.basis 0

The preferred longitude is λ - n · μ, for the longitude λ and meridian μ of Φ and its framing number n.

theorem TauCeti.IsSolidTorusNeighborhood.complementHomologyEquiv_boundaryHomologyMap_preferred {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) (x : h.framedBoundaryTorus.H) : (complementHomologyEquiv h₁ h₂ h) (h.boundaryHomologyMap x) = ((preferredFramedBoundaryTorus h₁ h₂ h).coord x).1

In the preferred framing a class goes to its meridian coordinate. A class of the boundary torus is homologous in the knot complement to its μ-coordinate in the preferred framing times the meridian.

theorem TauCeti.IsSolidTorusNeighborhood.boundaryHomologyMap_preferredFramedBoundaryTorus_basis_one {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : h.boundaryHomologyMap ((preferredFramedBoundaryTorus h₁ h₂ h).basis 1) = 0

The preferred longitude is null-homologous in the knot complement.

theorem TauCeti.IsSolidTorusNeighborhood.ker_boundaryHomologyMap {X : Type} [TopologicalSpace X] {f : Circle → X} {Φ : SolidTorus → X} [T2Space X] (h₁ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 1).obj ↧X)) (h₂ : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor (↧ℤ) 2).obj ↧X)) (h : IsSolidTorusNeighborhood f Φ) : h.boundaryHomologyMap.ker = ℤ ∙ (preferredFramedBoundaryTorus h₁ h₂ h).basis 1

The preferred longitude generates the classes of the boundary torus that are null-homologous in the knot complement.