Slopes on a framed boundary torus

A slope on the boundary torus T of a knot or link complement is the datum needed to specify a Dehn filling: the isotopy class of an unoriented essential simple closed curve on T, equivalently a primitive class in H₁(T; ℤ) taken modulo sign (Rolfsen, Knots and Links, Chapter 9). This is basis-free: it refers only to the homology group H₁(T; ℤ), an abstract rank-two free ℤ-module, with no coordinates chosen. Once T is framed by an ordered basis (μ, λ) of meridian and longitude, H₁(T; ℤ) is identified with ℤ × ℤ (first coordinate the μ-coefficient, second the λ-coefficient) and every slope acquires a value p / q ∈ ℚ ∪ {∞}, the ratio of its coordinates; the filling then sends the solid torus's meridian to p · μ + q · λ.

This file builds the slope arithmetic for the framed model. It keeps two objects distinct: the sign-quotient Slope, which is basis-free, and the ℚ ∪ {∞} parametrisation, which depends on a basis. So TauCeti.Slope M is the set of primitive classes modulo sign in an abstract ℤ-module M, and every framing-dependent notion — meridian, longitude, value, and the bijection slopeEquiv — belongs to TauCeti.FramedBoundaryTorus, which carries its own ordered basis. For a topological boundary torus, H₁(T; ℤ) is BoundaryTorus.firstHomology, its degree-one singular homology; the framed boundary torus of a knot exterior is built in TauCeti.LowDimTopology.DehnSurgery.Framing, as TauCeti.IsSolidTorusNeighborhood.framedBoundaryTorus via TauCeti.FramedBoundaryTorus.ofHomeomorph.

Primitivity of v : M is expressed basis-freely: v is primitive when some ℤ-linear functional M →ₗ[ℤ] ℤ sends it to 1, so v splits off a copy of ℤ. Over the standard lattice ℤ × ℤ this is exactly coprimality of the two coordinates, and that concrete arithmetic supplies the ℚ ∪ {∞} bijection through any framing's coordinate isomorphism.

Main definitions

• TauCeti.IsPrimitive v: the class v : M is primitive, i.e. some ℤ-functional sends it to 1.
• TauCeti.Slope M: primitive classes in M modulo the sign action v ↦ -v (basis-free).
• TauCeti.Slope.congr: transport of Slope along a ℤ-linear equivalence.
• TauCeti.slopeValue v: the value p / q ∈ ℚ ∪ {∞} of a class v = (p, q) : ℤ × ℤ, being ∞ when q = 0.
• TauCeti.slopeEquivStd: the bijection Slope (ℤ × ℤ) ≃ ℚ ∪ {∞} for the standard lattice.
• TauCeti.BoundaryTorus: a topological space homeomorphic to the standard two-torus.
• TauCeti.BoundaryTorus.firstHomology: its degree-one singular homology with integer coefficients.
• TauCeti.FramedBoundaryTorus: a boundary torus with an ordered meridian-longitude basis of that homology group.
• TauCeti.FramedBoundaryTorus.meridian / .longitude: the slopes (1, 0) and (0, 1) of the framing.
• TauCeti.FramedBoundaryTorus.value: the framing-dependent ℚ ∪ {∞} value of a slope.
• TauCeti.FramedBoundaryTorus.slopeEquiv: the bijection Slope T.H ≃ ℚ ∪ {∞} a framing produces.
• TauCeti.FramedBoundaryTorus.shiftLongitude: the framing with the same meridian and the longitude λ + n · μ.

Main results

• TauCeti.FramedBoundaryTorus.value_meridian / .value_longitude: the meridian is ∞ and the longitude is 0, fixing the meridian-longitude convention.
• TauCeti.FramedBoundaryTorus.slopeEquiv_symm_coe_ne_meridian: a slope of finite value is not the meridian.
• TauCeti.FramedBoundaryTorus.value_mk / .slopeEquiv_symm_apply: the parametrisation in coordinates, in each direction — a primitive class has the value of its (μ, λ)-coordinates, and a value comes from the slope whose coordinates are the corresponding reduced pair.
• TauCeti.FramedBoundaryTorus.coord_symm_apply: a pair of coordinates (p, q) names the class p · μ + q · λ, so the filling class of a slope is reachable without unfolding coord.
• TauCeti.FramedBoundaryTorus.value_shiftLongitude: replacing the longitude λ by λ + n · μ lowers every finite slope value by n.

ℚ ∪ {∞} is Mathlib's one-point extension OnePoint ℚ from Mathlib/Topology/Compactification/OnePoint/Basic.lean; the reduced-fraction bookkeeping reuses Mathlib's Rat normalisation (Rat.num_div_den, Rat.num_div_eq_of_coprime, Rat.den_div_eq_of_coprime).

Primitive classes and the basis-free slope type

The Quotient model of Slope, and the bodies of the maps into and out of it, are implementation details: the underlying setoid is private and the bodies stay unexposed, so consumers work through the public defining equations (Slope.congr_mk, Slope.value_mk, slopeOfValue_infty, slopeEquivStd_apply, …). Those equations are proved by a parenthesised (rfl), which keeps them ordinary propositional lemmas instead of implicitly @[defeq] ones; an exported @[defeq] theorem would have to expose every definition it unfolds.

def TauCeti.Slope (M : Type u_3) [AddCommGroup M] : Type u_3

A slope on a boundary torus with homology M: a primitive homology class taken modulo the sign action, i.e. an unoriented essential simple closed curve up to isotopy. This is basis-free — it refers only to the abstract module M, not to any choice of meridian-longitude basis.

def TauCeti.Slope.mk {M : Type u_1} [AddCommGroup M] (v : M) (h : IsPrimitive v) : Slope M

The slope represented by a primitive class v : M.

theorem TauCeti.Slope.mk_eq_mk {M : Type u_1} [AddCommGroup M] {v w : M} (hv : IsPrimitive v) (hw : IsPrimitive w) (h : v = w ∨ v = -w) : mk v hv = mk w hw

@[simp]

theorem TauCeti.Slope.mk_eq_mk_iff {M : Type u_1} [AddCommGroup M] {v w : M} (hv : IsPrimitive v) (hw : IsPrimitive w) : mk v hv = mk w hw ↔ v = w ∨ v = -w

Two primitive representatives define the same slope exactly when they agree up to sign.

theorem TauCeti.Slope.induction_on {M : Type u_1} [AddCommGroup M] {C : Slope M → Prop} (s : Slope M) (h : ∀ (v : M) (hv : IsPrimitive v), C (mk v hv)) : C s

def TauCeti.Slope.congr {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module ℤ M] [Module ℤ N] (φ : M ≃ₗ[ℤ] N) : Slope M ≃ Slope N

A ℤ-linear equivalence M ≃ₗ[ℤ] N transports slopes bijectively; a framing's coordinate isomorphism uses this to carry a slope to the standard lattice.

@[simp]

theorem TauCeti.Slope.congr_mk {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module ℤ M] [Module ℤ N] (φ : M ≃ₗ[ℤ] N) (v : M) (h : IsPrimitive v) : (congr φ) (mk v h) = mk (φ v) ⋯

@[simp]

theorem TauCeti.Slope.congr_symm {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module ℤ M] [Module ℤ N] (φ : M ≃ₗ[ℤ] N) : (congr φ).symm = congr φ.symm

Transporting slopes along φ and along φ.symm are inverse to one another.

The standard lattice ℤ × ℤ

For the standard lattice ℤ × ℤ, primitivity is coprimality of the coordinates, and the reduced fraction p / q supplies the ℚ ∪ {∞} parametrisation. Every framing produces its own copy of this bijection through its coordinate isomorphism.

theorem TauCeti.isPrimitive_prod_iff {v : ℤ × ℤ} : IsPrimitive v ↔ IsCoprime v.1 v.2

Over ℤ × ℤ, a class is primitive exactly when its two coordinates are coprime.

theorem TauCeti.isPrimitive_prod_one_zero : IsPrimitive (1, 0)

The first standard basis vector of ℤ × ℤ is primitive.

theorem TauCeti.isPrimitive_prod_zero_one : IsPrimitive (0, 1)

The second standard basis vector of ℤ × ℤ is primitive.

theorem TauCeti.isPrimitive_num_den (r : ℚ) : IsPrimitive (r.num, ↑r.den)

The reduced form (r.num, r.den) of a rational is a primitive class.

theorem TauCeti.isPrimitive_prod_fst_eq_one_or_neg_one_of_snd_eq_zero {v : ℤ × ℤ} (h : IsPrimitive v) (hq : v.2 = 0) : v.1 = 1 ∨ v.1 = -1

A primitive class of ℤ × ℤ with vanishing second coordinate has first coordinate ±1.

def TauCeti.slopeValue (v : ℤ × ℤ) : OnePoint ℚ

The value p / q ∈ ℚ ∪ {∞} of a class v = (p, q), taken to be ∞ when q = 0. This is the ratio of the meridian- and longitude-coordinates in a framing.

@[simp]

theorem TauCeti.slopeValue_of_snd_eq_zero {v : ℤ × ℤ} (hq : v.2 = 0) : slopeValue v = OnePoint.infty

@[simp]

theorem TauCeti.slopeValue_of_snd_ne_zero {v : ℤ × ℤ} (hq : v.2 ≠ 0) : slopeValue v = ↑(↑v.1 / ↑v.2)

theorem TauCeti.slopeValue_neg (v : ℤ × ℤ) : slopeValue (-v) = slopeValue v

The value of a class is unchanged by the sign action v ↦ -v.

def TauCeti.Slope.value : Slope (ℤ × ℤ) → OnePoint ℚ

The ℚ ∪ {∞} value of a standard-lattice slope, the ratio of its coordinates.

@[simp]

theorem TauCeti.Slope.value_mk (v : ℤ × ℤ) (h : IsPrimitive v) : (mk v h).value = slopeValue v

def TauCeti.slopeOfValue : OnePoint ℚ → Slope (ℤ × ℤ)

The primitive class attached to a value in ℚ ∪ {∞}: the class (1, 0) for ∞, and the reduced fraction (r.num, r.den) for a rational r.

@[simp]

theorem TauCeti.slopeOfValue_infty : slopeOfValue OnePoint.infty = Slope.mk (1, 0) isPrimitive_prod_one_zero

@[simp]

theorem TauCeti.slopeOfValue_coe (r : ℚ) : slopeOfValue ↑r = Slope.mk (r.num, ↑r.den) ⋯

theorem TauCeti.slopeOfValue_value (s : Slope (ℤ × ℤ)) : slopeOfValue s.value = s

Reading off the value of a standard-lattice slope and rebuilding a slope from it recovers the original slope.

theorem TauCeti.value_slopeOfValue (x : OnePoint ℚ) : (slopeOfValue x).value = x

The standard-lattice slope built from a value in ℚ ∪ {∞} has that value again.

def TauCeti.slopeEquivStd : Slope (ℤ × ℤ) ≃ OnePoint ℚ

The standard slope parametrisation. For the standard lattice ℤ × ℤ, primitive homology classes modulo sign biject with ℚ ∪ {∞}: a reduced fraction p / q corresponds to the primitive class (p, q), with ∞ the class (1, 0). A framing produces the corresponding bijection on any boundary torus through its coordinate isomorphism (TauCeti.FramedBoundaryTorus.slopeEquiv).

@[simp]

theorem TauCeti.slopeEquivStd_apply (s : Slope (ℤ × ℤ)) : slopeEquivStd s = s.value

@[simp]

theorem TauCeti.slopeEquivStd_symm_apply (x : OnePoint ℚ) : slopeEquivStd.symm x = slopeOfValue x

Boundary tori and framings

A framing supplies the coordinate isomorphism H₁(T; ℤ) ≃ ℤ × ℤ that turns the basis-free Slope into the ℚ ∪ {∞} parametrisation. The homology object and the ordered meridian-longitude basis are carried explicitly, keeping the basis-dependent notions (meridian, longitude, value, slopeEquiv) genuinely parametrised by the framing rather than globally canonical.

structure TauCeti.BoundaryTorus : Type 1

A boundary torus is a topological space that is homeomorphic to the standard two-torus; no particular homeomorphism is chosen. Its first homology, rather than an unrelated abstract lattice, is the carrier on which slopes are defined.

• carrier : Type

  The underlying topological space.

• topologicalSpace : TopologicalSpace self.carrier
• parametrization : Nonempty (self.carrier ≃ₜ UnitAddTorus (Fin 2))

  The assertion that the space is homeomorphic to the standard two-torus. Only the existence of such a homeomorphism is recorded, keeping this field a Prop, so it never obstructs equality: two boundary tori with the same carrier and the same topology are equal.

@[reducible, inline]

abbrev TauCeti.BoundaryTorus.firstHomology (T : BoundaryTorus) : Type

The first singular homology of a boundary torus with integer coefficients.

structure TauCeti.FramedBoundaryTorus : Type 1

A framed boundary torus: a boundary torus together with an ordered meridian-longitude basis (μ, λ) = (basis 0, basis 1) of its actual singular homology group. The framing is exactly this ordered basis; it is what identifies H₁(T; ℤ) with ℤ × ℤ and so what the ℚ ∪ {∞} parametrisation depends on.

• torus : BoundaryTorus

  The boundary torus being framed.

• basis : Module.Basis (Fin 2) ℤ self.torus.firstHomology

  The ordered meridian-longitude basis (μ, λ) framing the torus.

@[reducible, inline]

abbrev TauCeti.FramedBoundaryTorus.H (T : FramedBoundaryTorus) : Type

The first singular homology group of the underlying boundary torus.

noncomputable def TauCeti.FramedBoundaryTorus.coord (T : FramedBoundaryTorus) : T.H ≃ₗ[ℤ] ℤ × ℤ

The coordinate isomorphism H₁(T; ℤ) ≃ ℤ × ℤ induced by the ordered basis (μ, λ), sending a class to its (μ, λ)-coordinates. This is the data that makes the parametrisation basis-dependent.

@[simp]

theorem TauCeti.FramedBoundaryTorus.coord_basis_zero (T : FramedBoundaryTorus) : T.coord (T.basis 0) = (1, 0)

@[simp]

theorem TauCeti.FramedBoundaryTorus.coord_basis_one (T : FramedBoundaryTorus) : T.coord (T.basis 1) = (0, 1)

@[simp]

theorem TauCeti.FramedBoundaryTorus.coord_symm_apply (T : FramedBoundaryTorus) (v : ℤ × ℤ) : T.coord.symm v = v.1 • T.basis 0 + v.2 • T.basis 1

The inverse coordinate isomorphism reads a pair of coordinates as the corresponding combination p · μ + q · λ of the framing basis.

theorem TauCeti.FramedBoundaryTorus.isPrimitive_basis_zero (T : FramedBoundaryTorus) : IsPrimitive (T.basis 0)

theorem TauCeti.FramedBoundaryTorus.isPrimitive_basis_one (T : FramedBoundaryTorus) : IsPrimitive (T.basis 1)

noncomputable def TauCeti.FramedBoundaryTorus.meridian (T : FramedBoundaryTorus) : Slope T.H

The meridian slope μ = basis 0 of the framing.

noncomputable def TauCeti.FramedBoundaryTorus.longitude (T : FramedBoundaryTorus) : Slope T.H

The longitude slope λ = basis 1 of the framing.

noncomputable def TauCeti.FramedBoundaryTorus.value (T : FramedBoundaryTorus) (s : Slope T.H) : OnePoint ℚ

The framing-dependent value p / q ∈ ℚ ∪ {∞} of a slope: the ratio of its (μ, λ)-coordinates. Different framings give different values, which is why this is an operation of the framing rather than of the basis-free Slope.

noncomputable def TauCeti.FramedBoundaryTorus.slopeEquiv (T : FramedBoundaryTorus) : Slope T.H ≃ OnePoint ℚ

The framed slope parametrisation. A framing makes primitive homology classes modulo sign biject with ℚ ∪ {∞}, a reduced fraction p / q corresponding to the class with (μ, λ)-coordinates (p, q) and ∞ to the meridian.

@[simp]

theorem TauCeti.FramedBoundaryTorus.slopeEquiv_apply (T : FramedBoundaryTorus) (s : Slope T.H) : T.slopeEquiv s = T.value s

@[simp]

theorem TauCeti.FramedBoundaryTorus.value_mk (T : FramedBoundaryTorus) (v : T.H) (hv : IsPrimitive v) : T.value (Slope.mk v hv) = slopeValue (T.coord v)

The value of the slope of a primitive class is the ratio of its (μ, λ)-coordinates.

@[simp]

theorem TauCeti.FramedBoundaryTorus.slopeEquiv_symm_apply (T : FramedBoundaryTorus) (x : OnePoint ℚ) : T.slopeEquiv.symm x = (Slope.congr T.coord.symm) (slopeOfValue x)

The framed parametrisation in the inverse direction. The slope with value x ∈ ℚ ∪ {∞} is the one whose (μ, λ)-coordinates are the standard reduced pair slopeOfValue x; for a rational p / q in lowest terms that is the class p · μ + q · λ, by TauCeti.FramedBoundaryTorus.coord_symm_apply.

@[simp]

theorem TauCeti.FramedBoundaryTorus.value_meridian (T : FramedBoundaryTorus) : T.value T.meridian = OnePoint.infty

The framed meridian has slope value ∞.

@[simp]

theorem TauCeti.FramedBoundaryTorus.value_longitude (T : FramedBoundaryTorus) : T.value T.longitude = ↑0

The framed longitude has slope value 0.

theorem TauCeti.FramedBoundaryTorus.slopeEquiv_symm_coe_ne_meridian (T : FramedBoundaryTorus) (x : ℚ) : T.slopeEquiv.symm ↑x ≠ T.meridian

A slope of finite value is not the meridian, whose value is ∞.

Changing the longitude

noncomputable def TauCeti.FramedBoundaryTorus.shiftLongitudeBasis (T : FramedBoundaryTorus) (n : ℤ) : Module.Basis (Fin 2) ℤ T.H

The basis (μ, λ + n · μ) of H₁(T; ℤ).

@[reducible, inline]

noncomputable abbrev TauCeti.FramedBoundaryTorus.shiftLongitude (T : FramedBoundaryTorus) (n : ℤ) : FramedBoundaryTorus

The framing of the same torus with the same meridian μ and the longitude λ + n · μ. For the boundary torus of a knot exterior this is the framing changed by n twists about the meridian.

This is reducible so that the torus of the new framing is that of T for consumers, and hence that classes of T.H are classes of (T.shiftLongitude n).H.

@[simp]

theorem TauCeti.FramedBoundaryTorus.coord_shiftLongitude (T : FramedBoundaryTorus) (n : ℤ) (x : T.H) : (T.shiftLongitude n).coord x = ((T.coord x).1 - n * (T.coord x).2, (T.coord x).2)

The coordinates of a class for the shifted framing: p · μ + q · λ = (p - n q) · μ + q · (λ + n · μ).

@[simp]

theorem TauCeti.FramedBoundaryTorus.shiftLongitudeBasis_zero (T : FramedBoundaryTorus) (n : ℤ) : (T.shiftLongitudeBasis n) 0 = T.basis 0

The shifted framing keeps the meridian.

@[simp]

theorem TauCeti.FramedBoundaryTorus.shiftLongitudeBasis_one (T : FramedBoundaryTorus) (n : ℤ) : (T.shiftLongitudeBasis n) 1 = T.basis 1 + n • T.basis 0

The longitude of the shifted framing is λ + n · μ.

theorem TauCeti.FramedBoundaryTorus.value_shiftLongitude (T : FramedBoundaryTorus) (n : ℤ) (s : Slope T.H) : (T.shiftLongitude n).value s = OnePoint.map (fun (x : ℚ) => x - ↑n) (T.value s)

Slope values under a change of longitude. Replacing the longitude λ by λ + n · μ lowers every finite slope value by n and keeps ∞: the class p · μ + q · λ is (p - n q) · μ + q · (λ + n · μ).

This is not a simp lemma: framings such as the preferred framing of a knot are reducible shiftLongitudes, and rewriting their values this way would preempt the lemmas stated for them.

@[simp]

theorem TauCeti.FramedBoundaryTorus.shiftLongitude_zero (T : FramedBoundaryTorus) : T.shiftLongitude 0 = T

Shifting the longitude by 0 leaves the framing unchanged.