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, the first piece of the geometric-topology roadmap's Dehn-surgery layer (TauCetiRoadmap/GeometricTopology/README.md, layer 5, "Dehn surgery": "Slopes, with the primitive pinned … give a FramedBoundaryTorus an ordered basis (μ, λ) … and the resulting bijection Slope T ≃ ℚ ∪ {∞}"). The layer asks for two objects kept distinct: the sign-quotient Slope (basis-free) and the ℚ ∪ {∞} parametrisation (basis-dependent). Accordingly TauCeti.Slope M is the basis-free set of primitive classes modulo sign in an abstract ℤ-module M, and every framing-dependent notion — meridian, longitude, value, and the bijection slopeEquiv — is a field/operation of TauCeti.FramedBoundaryTorus, carrying its own ordered basis. Identifying H₁(T; ℤ) with the boundary torus of a genuine link complement is now expressed through BoundaryTorus.firstHomology; constructing that boundary torus from the complement is later layer-5 work that consumes this arithmetic.

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.

Main results

• TauCeti.FramedBoundaryTorus.value_meridian / .value_longitude: the meridian is ∞ and the longitude is 0, fixing the meridian-longitude convention.
• 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.

ℚ ∪ {∞} 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.IsPrimitive {M : Type u_1} [AddCommGroup M] [Module ℤ M] (v : M) : Prop

A homology class v : M on a boundary torus is primitive when some ℤ-linear functional M →ₗ[ℤ] ℤ sends it to 1, so the span of v splits off a copy of ℤ. Over the standard lattice ℤ × ℤ this is coprimality of the two coordinates (TauCeti.isPrimitive_prod_iff). The definition mentions no basis, so it is preserved by every ℤ-linear equivalence (TauCeti.isPrimitive_congr).

Equations

• TauCeti.IsPrimitive v = ∃ (f : M →ₗ[ℤ] ℤ), f v = 1

theorem TauCeti.IsPrimitive.neg {M : Type u_1} [AddCommGroup M] [Module ℤ M] {v : M} (h : IsPrimitive v) : IsPrimitive (-v)

Primitivity is unchanged by the sign action v ↦ -v.

theorem TauCeti.isPrimitive_congr {M : Type u_1} {N : Type u_2} [AddCommGroup M] [AddCommGroup N] [Module ℤ M] [Module ℤ N] (φ : M ≃ₗ[ℤ] N) {v : M} : IsPrimitive (φ v) ↔ IsPrimitive v

Primitivity transports along a ℤ-linear equivalence: it is a basis-free property.

def TauCeti.Slope (M : Type u_3) [AddCommGroup M] [Module ℤ 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.

Equations

• TauCeti.Slope M = Quotient (TauCeti.slopeSetoid✝ M)

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

The slope represented by a primitive class v : M.

Equations

• TauCeti.Slope.mk v h = ⟦⟨v, h⟩⟧

theorem TauCeti.Slope.mk_eq_mk {M : Type u_1} [AddCommGroup M] [Module ℤ 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] [Module ℤ 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] [Module ℤ 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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• TauCeti.slopeValue v = if v.2 = 0 then OnePoint.infty else ↑(↑v.1 / ↑v.2)

@[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.

Equations

• TauCeti.Slope.value = Quotient.lift (fun (v : { v : ℤ × ℤ // TauCeti.IsPrimitive v }) => TauCeti.slopeValue ↑v) TauCeti.Slope.value._proof_1✝

@[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.

Equations

• TauCeti.slopeOfValue none = TauCeti.Slope.mk (1, 0) TauCeti.isPrimitive_prod_one_zero
• TauCeti.slopeOfValue (some r) = TauCeti.Slope.mk (r.num, ↑r.den) ⋯

@[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).

Equations

• TauCeti.slopeEquivStd = { toFun := TauCeti.Slope.value, invFun := TauCeti.slopeOfValue, left_inv := TauCeti.slopeOfValue_value, right_inv := TauCeti.value_slopeOfValue }

@[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.

Equations

• T.firstHomology = ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) 1).obj (ModuleCat.of ℤ ℤ)).obj (TopCat.of T.carrier))

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.

Equations

• T.H = T.torus.firstHomology

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.

Equations

• T.coord = T.basis.equivFun ≪≫ₗ LinearEquiv.finTwoArrow ℤ ℤ

@[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.

Equations

• T.meridian = TauCeti.Slope.mk (T.basis 0) ⋯

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

The longitude slope λ = basis 1 of the framing.

Equations

• T.longitude = TauCeti.Slope.mk (T.basis 1) ⋯

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.

Equations

• T.value s = ((TauCeti.Slope.congr T.coord) s).value

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.

Equations

• T.slopeEquiv = (TauCeti.Slope.congr T.coord).trans TauCeti.slopeEquivStd

@[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.