Skip to content

Knot diagrams

64 fully proved

Regular Projection

StructureDart diagram#✓fully proved

A dart diagram consists of a finite set \(V\) of crossings, a fixed-point-free involution \(\mathrm{pair}\) of the set \(V \times \{0, 1, 2, 3\}\) of darts, and a natural number counting isolated crossingless components.

Darts \(0, 1, 2, 3\) at a crossing are read in counterclockwise order, darts \(0\) and \(2\) form the over-strand and darts \(1\) and \(3\) the under-strand, and \(\mathrm{pair}\) glues darts across edge segments. The structure does not by itself assert planarity.

structure DartDiagram where
  Vertex : Type
  [vertexFintype : Fintype Vertex]
  [vertexDecidableEq : DecidableEq Vertex]
  pair : Vertex × Fin 4 → Vertex × Fin 4
  pair_involutive : ∀ d, pair (pair d) = d
  pair_ne_self : ∀ d, pair d ≠ d
  isolated : ℕ
Used by 18
Used byNumber of components of a dart diagram · Strand-connectivity relation on darts · Number of crossings of a dart diagram · Darts of a dart diagram · Empty dart diagram · Alternating dart diagrams · Over-strand darts · Isolated components are counted in the component count · Strand traversal step · Strand traversal permutation · Opposite dart · Opposite-dart permutation · Edge-pairing permutation · Rotation of a dart · Rotation permutation of darts · Same component relation on darts · A traversal step stays in the same component · A traversal step stays in its strand cycle

Dart Diagram

AbbreviationDarts of a dart diagram#✓fully proved

The darts of a dart diagram \(D\) with crossing set \(V\) are the pairs \((v, i)\) with \(v \in V\) and \(i \in \{0, 1, 2, 3\}\); the dart \((v, i)\) is the \(i\)-th incident half-edge at the crossing \(v\).

abbrev Dart (D : DartDiagram) : Type :=
  D.Vertex × Fin 4
Uses 1 · Used by 15
Statement usesDart diagram
Used byNumber of components of a dart diagram · Strand-connectivity relation on darts · Alternating dart diagrams · Over-strand darts · Isolated components are counted in the component count · Strand traversal step · Strand traversal permutation · Opposite dart · Opposite-dart permutation · Edge-pairing permutation · Rotation of a dart · Rotation permutation of darts · Same component relation on darts · A traversal step stays in the same component · A traversal step stays in its strand cycle

DefinitionNumber of crossings of a dart diagram#✓fully proved

The crossing count of a dart diagram \(D\) is the number of vertices of \(D\), each vertex being one crossing.

def crossingCount (D : DartDiagram) : ℕ := by
  letI := D.vertexFintype
  exact Fintype.card D.Vertex
Uses 1
Statement usesDart diagram

DefinitionRotation of a dart#✓fully proved

For a dart diagram \(D\), the rotation of a dart \((v, i)\) of \(D\), with \(v\) a crossing and \(i \in \mathbb{Z}/4\), is the dart \((v, i + 1)\): one step counterclockwise around the crossing \(v\).

def rot (D : DartDiagram) (d : D.Dart) : D.Dart :=
  (d.1, d.2 + 1)
Uses 2 · Used by 3
Statement usesDart diagram · Darts of a dart diagram
Used byOpposite dart · Rotation permutation of darts · A traversal step stays in its strand cycle

DefinitionOpposite dart#✓fully proved

For a dart diagram \(D\) and a dart \(d = (v, i)\) of \(D\), the opposite dart is obtained by rotating \(d\) twice counterclockwise around its crossing \(v\); it is the dart \((v, i + 2)\), with labels taken modulo \(4\).

def opposite (D : DartDiagram) (d : D.Dart) : D.Dart :=
  D.rot (D.rot d)
Uses 3 · Used by 4
Statement usesDart diagram · Darts of a dart diagram · Rotation of a dart
Used byStrand-connectivity relation on darts · Strand traversal step · Same component relation on darts · A traversal step stays in the same component

DefinitionOver-strand darts#✓fully proved

The four darts at a crossing of a dart diagram carry the labels \(0, 1, 2, 3\) in cyclic order. A dart lies on the over-strand at its crossing when its label is \(0\) or \(2\).

def isOver (D : DartDiagram) (d : D.Dart) : Bool :=
  decide (d.2 = 0 ∨ d.2 = 2)
Uses 2 · Used by 1
Statement usesDart diagram · Darts of a dart diagram
Used byAlternating dart diagrams

DefinitionEdge-pairing permutation#✓fully proved

For a dart diagram \(D\), the edge-pairing permutation is the edge-pairing involution of \(D\) regarded as a permutation of the darts of \(D\); it is its own inverse.

def pairPerm (D : DartDiagram) : Equiv.Perm D.Dart where
  toFun := D.pair
  invFun := D.pair
  left_inv := D.pair_involutive
  right_inv := D.pair_involutive
Uses 2 · Used by 2
Statement usesDart diagram · Darts of a dart diagram
Used byStrand traversal permutation · A traversal step stays in its strand cycle

DefinitionRotation permutation of darts#✓fully proved

For a dart diagram \(D\), the rotation permutation is the permutation of the darts of \(D\) sending a dart \((v, i)\), with \(v\) a crossing and \(i \in \mathbb{Z}/4\), to \((v, i + 1)\); its inverse sends \((v, i)\) to \((v, i - 1)\).

def rotPerm (D : DartDiagram) : Equiv.Perm D.Dart where
  toFun := D.rot
  invFun := fun d => (d.1, d.2 - 1)
  left_inv := by intro d; simp [DartDiagram.rot]
  right_inv := by intro d; simp [DartDiagram.rot]
Uses 3 · Used by 1
Statement usesDart diagram · Darts of a dart diagram · Rotation of a dart
Used byOpposite-dart permutation

DefinitionOpposite-dart permutation#✓fully proved

For a dart diagram \(D\), the opposite-dart permutation of the darts of \(D\) is the square of the quarter-turn rotation permutation: it sends the dart \((v, i)\) at crossing \(v\) to the dart \((v, i + 2)\), with labels taken modulo \(4\).

def oppositePerm (D : DartDiagram) : Equiv.Perm D.Dart :=
  D.rotPerm ^ 2
Uses 3 · Used by 2
Statement usesDart diagram · Darts of a dart diagram · Rotation permutation of darts
Used byStrand traversal permutation · A traversal step stays in its strand cycle

DefinitionStrand traversal step#✓fully proved

For a dart diagram \(D\) and a dart \(d\) of \(D\), the next dart after \(d\) is the dart opposite \(\mathrm{pair}(d)\) at its crossing, where \(\mathrm{pair}\) is the edge-pairing involution of \(D\): cross the edge segment at \(d\), then go straight through the crossing reached.

def next (D : DartDiagram) (d : D.Dart) : D.Dart :=
  D.opposite (D.pair d)
Uses 3 · Used by 3
Statement usesDart diagram · Darts of a dart diagram · Opposite dart
Used byAlternating dart diagrams · A traversal step stays in the same component · A traversal step stays in its strand cycle

DefinitionStrand traversal permutation#✓fully proved

For a dart diagram \(D\), the strand traversal permutation of the darts of \(D\) is the edge-pairing permutation followed by the opposite-dart permutation: it sends a dart \(d\) to the dart opposite \(\mathrm{pair}(d)\) at its crossing, where \(\mathrm{pair}\) is the edge-pairing involution of \(D\).

def nextPerm (D : DartDiagram) : Equiv.Perm D.Dart :=
  D.oppositePerm * D.pairPerm
Uses 4 · Used by 1
Statement usesDart diagram · Darts of a dart diagram · Opposite-dart permutation · Edge-pairing permutation
Used byA traversal step stays in its strand cycle

TheoremA traversal step stays in its strand cycle#✓fully proved

Let \(D\) be a dart diagram, and for a dart \(d\) of \(D\) let \(\operatorname{next}(d)\) be the dart reached from \(d\) by crossing its edge segment and then going straight through the next crossing. Then for every dart \(d\) of \(D\), the darts \(d\) and \(\operatorname{next}(d)\) lie in the same cycle of the strand traversal permutation of \(D\), the permutation of the darts of \(D\) that sends each dart \(e\) to \(\operatorname{next}(e)\).

theorem sameCycle_next (D : DartDiagram) (d : D.Dart) :
    D.nextPerm.SameCycle d (D.next d)
Uses 7
Statement usesDart diagram · Darts of a dart diagram · Strand traversal step · Strand traversal permutation
Proof usesOpposite-dart permutation · Edge-pairing permutation · Rotation of a dart

DefinitionAlternating dart diagrams#✓fully proved

A dart diagram is alternating when, for every dart \(d\), the dart \(\operatorname{next}(d)\), reached from \(d\) by crossing its edge segment and going straight through the next crossing, has the opposite over/under status to \(d\). In other words, consecutive crossings on every strand have opposite over/under status.

Crossingless components impose no condition.

def IsAlternating (D : DartDiagram) : Prop :=
  ∀ d, D.isOver (D.next d) ≠ D.isOver d
Uses 4
Statement usesDart diagram · Darts of a dart diagram · Over-strand darts · Strand traversal step

DefinitionSame component relation on darts#✓fully proved

For a dart diagram \(D\), two darts of \(D\) lie in the same component when they are related by the equivalence relation on darts generated by \(d \sim \operatorname{pair}(d)\), crossing an edge segment, and \(d \sim \operatorname{opposite}(d)\), going straight through a crossing.

The oriented traversal \(\operatorname{next}\) traverses every component twice, once in each orientation, so the cycles of the traversal permutation are not themselves the components.

def SameComponent (D : DartDiagram) : D.Dart → D.Dart → Prop :=
  Relation.EqvGen (fun x y => y = D.pair x ∨ y = D.opposite x)
Uses 3 · Used by 1
Statement usesDart diagram · Darts of a dart diagram · Opposite dart
Used byA traversal step stays in the same component

DefinitionStrand-connectivity relation on darts#✓fully proved

For a dart diagram \(D\), this is the equivalence relation on the darts of \(D\) generated by relating each dart \(d\) to its partner across an edge segment and to the opposite dart of \(d\) at the same crossing. Two darts are related exactly when they lie on the same unoriented strand component.

def componentSetoid (D : DartDiagram) : Setoid D.Dart :=
  Relation.EqvGen.setoid (fun x y => y = D.pair x ∨ y = D.opposite x)
Uses 3 · Used by 2
Statement usesDart diagram · Darts of a dart diagram · Opposite dart
Used byNumber of components of a dart diagram · Isolated components are counted in the component count

TheoremA traversal step stays in the same component#✓fully proved

For every dart \(d\) of a dart diagram \(D\), the dart \(\operatorname{next}(d)\) reached by one step of strand traversal lies in the same component as \(d\).

theorem sameComponent_next (D : DartDiagram) (d : D.Dart) :
    D.SameComponent d (D.next d)
Uses 5
Statement usesDart diagram · Darts of a dart diagram · Same component relation on darts · Strand traversal step
Proof usesOpposite dart

DefinitionNumber of components of a dart diagram#✓fully proved

The number of components of a dart diagram \(D\) is the number of classes of darts of \(D\) under unoriented strand connectivity, plus the recorded number of isolated crossingless components of \(D\).

noncomputable def componentCount (D : DartDiagram) : ℕ :=
  Nat.card (Quotient D.componentSetoid) + D.isolated
Uses 3 · Used by 1
Statement usesDart diagram · Darts of a dart diagram · Strand-connectivity relation on darts
Used byIsolated components are counted in the component count

TheoremIsolated components are counted in the component count#✓fully proved

For every dart diagram \(D\), the number of isolated crossingless components recorded in \(D\) is at most the number of components of \(D\).

theorem isolated_le_componentCount (D : DartDiagram) :
    D.isolated ≤ D.componentCount
Uses 4
Statement usesDart diagram · Number of components of a dart diagram
Proof usesDarts of a dart diagram · Strand-connectivity relation on darts

DefinitionEmpty dart diagram#✓fully proved

For a natural number \(k\), the empty dart diagram with \(k\) isolated components has no crossings, hence no darts, and records \(k\) isolated crossingless components.

It is alternating, since the alternating condition is vacuous when there are no darts.

def empty (isolated : ℕ) : DartDiagram where
  Vertex := PEmpty
  pair := fun d => d.1.elim
  pair_involutive := fun d => d.1.elim
  pair_ne_self := fun d => d.1.elim
  isolated := isolated
Uses 1
Statement usesDart diagram

Regular Projection

AbbreviationEuclidean plane#✓fully proved

The space \(\mathbb{R}^2\) with its Euclidean inner product and norm, the target plane of the fixed standard projection frame.

abbrev R2 : Type := EuclideanSpace ℝ (Fin 2)
Used by 27
Used byLinks with a crossing-free regular projection admit alternating diagrams · Crossings of a link projection · A crossing-free regular projection has crossing count zero · A regular projection with a crossing has positive crossing count · Crossing number zero from a crossing-free representative · Double points of a link projection · The over and under preimages exhaust a crossing · Double points have exactly two preimages · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Points with the same projection have different heights · The under-strand lies strictly below the over-strand · The projected trace is the union of the projected components · Crossingless regular projections are alternating · Crossing preimages · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · Being the over-strand preimage of a crossing · Regular projections · Being the under-strand preimage of a crossing · Standard projection to the plane · Projected curve of a link component · Projected point of a link at a parameter point · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Projected tangent vector · Over and under preimages differ

DefinitionStandard projection to the plane#✓fully proved

The standard projection sends a point \(x = (x_0, x_1, x_2)\) of Euclidean 3-space to the point \((x_0, x_1)\) of the Euclidean plane, forgetting the third coordinate.

def plane (x : R3) : R2 :=
  WithLp.toLp 2 (fun i => x (Fin.castSucc i))
Uses 2 · Used by 5
Statement usesEuclidean 3-space · Euclidean plane
Used byPoints with the same projection have different heights · The projected trace is the union of the projected components · Projected curve of a link component · Projected point of a link at a parameter point · Projected tangent vector

DefinitionHeight in the standard projection frame#✓fully proved

The height of a point \(x = (x_1, x_2, x_3)\) of Euclidean 3-space is its third coordinate \(x_3\).

def height (x : R3) : ℝ :=
  x 2
Uses 1 · Used by 2
Statement usesEuclidean 3-space
Used byHeight of a parameter point · Points with the same projection have different heights

StructureParameter point#✓fully proved

For a natural number \(n\), a parameter point consists of a component index \(i \in \{0, \dots, n-1\}\) and a real parameter \(t\) with \(0 \le t < 2\pi\), the fundamental half-open period. It represents the point at parameter \(t\) of component \(i\) of a parametrized link with \(n\) components.

structure ParamPoint (n : ℕ) where
  comp : Fin n
  t : ℝ
  ht : t ∈ Set.Ico 0 (2 * Real.pi)
Used by 26
Used byCyclically adjacent crossing preimages · Double points of a link projection · The over and under preimages exhaust a crossing · Double points have exactly two preimages · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Height of a parameter point · Points with the same projection have different heights · The under-strand lies strictly below the over-strand · Open arc on the parameter circle · Alternating regular projections · Crossingless regular projections are alternating · Crossing preimages · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · Being the over-strand preimage of a crossing · Regular projections · Being the under-strand preimage of a crossing · Over-strand preimage of a crossing · Point of a link at a parameter point · Projected point of a link at a parameter point · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Projected tangent vector · Under-strand preimage of a crossing · Over and under preimages differ

Euclidean

DefinitionPoint of a link at a parameter point#✓fully proved

For a parametrized link \(L\) with components \(\gamma_0, \dots, \gamma_{n-1} \colon \mathbb{R} \to \mathbb{R}^3\) and a parameter point \(a = (i, t)\), with \(i < n\) and \(t \in [0, 2\pi)\), the point of \(L\) at \(a\) is \(\gamma_i(t) \in \mathbb{R}^3\).

def ParametrizedLink.point {n : ℕ} (L : ParametrizedLink n)
    (a : RegularProjection.ParamPoint n) : R3 :=
  (L.component a.comp).curve a.t
Uses 4 · Used by 3
Statement usesEuclidean 3-space · Parametrized knot · Parametrized link · Parameter point
Used byHeight of a parameter point · Points with the same projection have different heights · Projected point of a link at a parameter point

DefinitionProjected curve of a link component#✓fully proved

For a parametrized link \(L\) with components \(\gamma_0, \dots, \gamma_{n-1} \colon \mathbb{R} \to \mathbb{R}^3\) and \(i < n\), the projected curve of component \(i\) is the map \(\mathbb{R} \to \mathbb{R}^2\), \(t \mapsto \pi(\gamma_i(t))\), where \(\pi(x_0, x_1, x_2) = (x_0, x_1)\) is the standard projection forgetting the third coordinate.

def ParametrizedLink.projCurve {n : ℕ} (L : ParametrizedLink n)
    (i : Fin n) : ℝ → RegularProjection.R2 :=
  RegularProjection.plane ∘ (L.component i).curve
Uses 5 · Used by 1
Statement usesEuclidean 3-space · Parametrized knot · Parametrized link · Euclidean plane · Standard projection to the plane
Used byThe projected trace is the union of the projected components

DefinitionProjected point of a link at a parameter point#✓fully proved

For a parametrized link \(L\) with components \(\gamma_0, \dots, \gamma_{n-1} \colon \mathbb{R} \to \mathbb{R}^3\) and a parameter point \(a = (i, t)\), with \(i < n\) and \(t \in [0, 2\pi)\), the projected point of \(L\) at \(a\) is \(\pi(\gamma_i(t)) \in \mathbb{R}^2\), where \(\pi(x_0, x_1, x_2) = (x_0, x_1)\) forgets the third coordinate.

def ParametrizedLink.projPoint {n : ℕ} (L : ParametrizedLink n)
    (a : RegularProjection.ParamPoint n) : RegularProjection.R2 :=
  RegularProjection.plane (L.point a)
Uses 5 · Used by 17
Statement usesParametrized link · Point of a link at a parameter point · Parameter point · Euclidean plane · Standard projection to the plane
Used byDouble points of a link projection · The over and under preimages exhaust a crossing · Double points have exactly two preimages · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Points with the same projection have different heights · The under-strand lies strictly below the over-strand · Crossingless regular projections are alternating · Crossing preimages · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · Being the over-strand preimage of a crossing · Regular projections · Being the under-strand preimage of a crossing · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Over and under preimages differ

DefinitionProjected tangent vector#✓fully proved

Let \(L\) be a parametrized link and let \(a\) be a parameter point of \(L\), given by a component \(i\) and a parameter \(t\). The projected tangent vector of \(L\) at \(a\) is the vector of \(\mathbb{R}^2\) obtained by applying the standard projection \((x, y, z) \mapsto (x, y)\) to the derivative \(\gamma_i'(t)\) of the curve \(\gamma_i\) of the \(i\)-th component of \(L\) at \(t\).

This is the projection of the ambient derivative; it is not defined as the derivative of the projected curve.

noncomputable def ParametrizedLink.tangent {n : ℕ} (L : ParametrizedLink n)
    (a : RegularProjection.ParamPoint n) : RegularProjection.R2 :=
  RegularProjection.plane (deriv (L.component a.comp).curve a.t)
Uses 6 · Used by 1
Statement usesEuclidean 3-space · Parametrized knot · Parametrized link · Parameter point · Euclidean plane · Standard projection to the plane
Used byRegular projections

DefinitionHeight of a parameter point#✓fully proved

For a parametrized link \(L\) with \(n\) components and a parameter point \(a\) of \(L\), the height of \(L\) at \(a\) is the height (the third coordinate) of the point of Euclidean 3-space that \(a\) represents on \(L\).

def ParametrizedLink.heightAt {n : ℕ} (L : ParametrizedLink n)
    (a : RegularProjection.ParamPoint n) : ℝ :=
  RegularProjection.height (L.point a)
Uses 4 · Used by 9
Statement usesParametrized link · Point of a link at a parameter point · Parameter point · Height in the standard projection frame
Used byThe over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Points with the same projection have different heights · The under-strand lies strictly below the over-strand · Being the over-strand preimage of a crossing · Being the under-strand preimage of a crossing · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Over and under preimages differ

DefinitionDouble points of a link projection#✓fully proved

For an oriented labeled parametrized link \(L\) with \(n\) components, the double-point set of \(L\) is the set of points \(p\) of the plane \(\mathbb{R}^2\) for which there are two distinct parameter points of \(L\) (each a component index together with a parameter in \([0, 2\pi)\)) whose images under the standard projection, which forgets the third coordinate, both equal \(p\).

def ParametrizedLink.doublePointSet {n : ℕ} (L : ParametrizedLink n) :
    Set RegularProjection.R2 :=
  {p | ∃ a b : RegularProjection.ParamPoint n, a ≠ b ∧ L.projPoint a = p ∧ L.projPoint b = p}
Uses 4 · Used by 20
Statement usesParametrized link · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Used byLinks with a crossing-free regular projection admit alternating diagrams · Crossings of a link projection · A crossing-free regular projection has crossing count zero · A regular projection with a crossing has positive crossing count · Crossing number zero from a crossing-free representative · The over and under preimages exhaust a crossing · Double points have exactly two preimages · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · The under-strand lies strictly below the over-strand · Crossingless regular projections are alternating · Crossing preimages · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · Being the over-strand preimage of a crossing · Regular projections · Being the under-strand preimage of a crossing · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Over and under preimages differ

StructureRegular projections#✓fully proved

Let \(L\) be a parametrized link; a parameter point of \(L\) is a component of \(L\) together with a parameter in \([0, 2\pi)\). The standard projection of \(L\) to the plane, which forgets the third coordinate, is regular when the following hold: at every parameter point, the projection of the velocity vector of the component curve is nonzero; the double-point set is finite; no three pairwise distinct parameter points have the same projection; and at any two distinct parameter points with the same projection, the projected velocity vectors are linearly independent over \(\mathbb{R}\).

The condition records no diagram, crossing labels or over/under data. The heights at two distinct parameter points with the same projection always differ, because each component is injective on a period and the components are pairwise disjoint.

structure ParametrizedLink.IsRegularProjection {n : ℕ}
    (L : ParametrizedLink n) : Prop where
  cuspFree : ∀ a : RegularProjection.ParamPoint n, L.tangent a ≠ 0
  finiteDouble : L.doublePointSet.Finite
  noTriple : ∀ a b c : RegularProjection.ParamPoint n,
    L.projPoint a = L.projPoint b → L.projPoint b = L.projPoint c →
      a = b ∨ b = c ∨ a = c
  transverse : ∀ a b : RegularProjection.ParamPoint n, a ≠ b →
    L.projPoint a = L.projPoint b →
      LinearIndependent ℝ ![L.tangent a, L.tangent b]
Uses 6 · Used by 27
Statement usesParametrized link · Double points of a link projection · Projected point of a link at a parameter point · Projected tangent vector · Parameter point · Euclidean plane
Used byLinks admitting an alternating diagram · Links with a crossing-free regular projection admit alternating diagrams · Crossing count of a regular projection · A crossing-free regular projection has crossing count zero · A regular projection with a crossing has positive crossing count · Crossing number of a link · The crossing number is an isotopy invariant · Crossing number zero from a crossing-free representative · Regular projections of isotopic links bound the crossing number · A link's own regular projection bounds its crossing number · Finiteness of the crossing number · The over and under preimages exhaust a crossing · Double points have exactly two preimages · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · The under-strand lies strictly below the over-strand · Alternating regular projections · Crossingless regular projections are alternating · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · Admitting an alternating diagram is an isotopy invariant · Over-strand preimage of a crossing · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Under-strand preimage of a crossing · Over and under preimages differ · Alternating link types have finite crossing number

TheoremPoints with the same projection have different heights#✓fully proved

Let \(L\) be a parametrized link with \(n\) components. If two distinct parameter points \(a \ne b\) of \(L\) have the same projected point, then the heights of \(L\) at \(a\) and at \(b\) are different.

This is forced by component injectivity in one period and pairwise disjoint component traces; over/under is therefore derived from the parametrization rather than chosen.

theorem ParametrizedLink.heightAt_ne_of_projPoint_eq_of_ne {n : ℕ}
    (L : ParametrizedLink n) {a b : RegularProjection.ParamPoint n} (hab : a ≠ b)
    (hproj : L.projPoint a = L.projPoint b) :
    L.heightAt a ≠ L.heightAt b
Uses 10 · Used by 2
Statement usesParametrized link · Height of a parameter point · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Proof usesEuclidean 3-space · Parametrized knot · Point of a link at a parameter point · Height in the standard projection frame · Standard projection to the plane
Used byThe over-strand preimage exists and is unique · The under-strand preimage exists and is unique

AbbreviationCrossings of a link projection#✓fully proved

Let \(L\) be a parametrized link with \(n\) components. A crossing of \(L\) is a point of the double-point set of \(L\), that is, a point \(p\) of the plane \(\mathbb{R}^2\) such that two distinct parameter points of \(L\) both have image \(p\) under the standard projection forgetting the third coordinate.

abbrev ParametrizedLink.Crossing {n : ℕ} (L : ParametrizedLink n) : Type :=
  {p : RegularProjection.R2 // p ∈ L.doublePointSet}
Uses 3 · Used by 15
Statement usesParametrized link · Double points of a link projection · Euclidean plane
Used byCrossing count of a regular projection · A crossing-free regular projection has crossing count zero · A regular projection with a crossing has positive crossing count · The over and under preimages exhaust a crossing · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · The under-strand lies strictly below the over-strand · The two preimages of a crossing have opposite status · Being the over-strand preimage of a crossing · Being the under-strand preimage of a crossing · Over-strand preimage of a crossing · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Under-strand preimage of a crossing · Over and under preimages differ

DefinitionCrossing count of a regular projection#✓fully proved

For a parametrized link \(L\) whose standard projection is regular, the crossing count of \(L\) is the number of crossings of the projection, that is, the number of points of its double-point set.

Regularity guarantees that the double-point set is finite, and the value does not depend on the chosen proof of regularity.

noncomputable def ParametrizedLink.crossingCount {n : ℕ}
    (L : ParametrizedLink n) (_h : L.IsRegularProjection) : ℕ :=
  Nat.card L.Crossing
Uses 3 · Used by 8
Statement usesParametrized link · Crossings of a link projection · Regular projections
Used byA crossing-free regular projection has crossing count zero · A regular projection with a crossing has positive crossing count · Crossing number of a link · The crossing number is an isotopy invariant · Crossing number zero from a crossing-free representative · Regular projections of isotopic links bound the crossing number · A link's own regular projection bounds its crossing number · Finiteness of the crossing number

TheoremDouble points have exactly two preimages#✓fully proved

Let \(L\) be a parametrized link with \(n\) components whose standard projection is regular, and let \(p\) be a point of the double-point set of \(L\). Then there are parameter points \(a \ne b\) of \(L\) whose projected points are both \(p\), and every parameter point of \(L\) whose projected point is \(p\) is \(a\) or \(b\).

theorem ParametrizedLink.exists_pair_of_mem_doublePointSet {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    {p : RegularProjection.R2} (hp : p ∈ L.doublePointSet) :
    ∃ a b : RegularProjection.ParamPoint n, a ≠ b ∧ L.projPoint a = p ∧ L.projPoint b = p ∧
      ∀ c : RegularProjection.ParamPoint n, L.projPoint c = p → c = a ∨ c = b
Uses 6 · Used by 4
Statement usesParametrized link · Regular projections · Double points of a link projection · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Used byThe over and under preimages exhaust a crossing · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Over and under preimages differ

DefinitionBeing the over-strand preimage of a crossing#✓fully proved

Let \(L\) be a parametrized link and \(p\) a crossing of its standard projection to the plane. A parameter point \(a\) of \(L\) is an over point of \(p\) when \(a\) projects to \(p\) and every other parameter point that projects to \(p\) has strictly smaller height than \(a\).

def ParametrizedLink.IsOverPoint {n : ℕ} (L : ParametrizedLink n)
    (p : L.Crossing) (a : RegularProjection.ParamPoint n) : Prop :=
  L.projPoint a = p.1 ∧ ∀ b : RegularProjection.ParamPoint n,
    L.projPoint b = p.1 → b = a ∨ L.heightAt b < L.heightAt a
Uses 7 · Used by 5
Statement usesParametrized link · Crossings of a link projection · Double points of a link projection · Height of a parameter point · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Used byThe over-strand preimage exists and is unique · The under-strand lies strictly below the over-strand · Over-strand preimage of a crossing · The over-strand preimage lies over its crossing · Over and under preimages differ

DefinitionBeing the under-strand preimage of a crossing#✓fully proved

Let \(L\) be a parametrized link and \(p\) a crossing of its standard projection to the plane. A parameter point \(a\) of \(L\) is an under point of \(p\) when \(a\) projects to \(p\) and every other parameter point that projects to \(p\) has strictly greater height than \(a\).

def ParametrizedLink.IsUnderPoint {n : ℕ} (L : ParametrizedLink n)
    (p : L.Crossing) (a : RegularProjection.ParamPoint n) : Prop :=
  L.projPoint a = p.1 ∧ ∀ b : RegularProjection.ParamPoint n,
    L.projPoint b = p.1 → b = a ∨ L.heightAt a < L.heightAt b
Uses 7 · Used by 5
Statement usesParametrized link · Crossings of a link projection · Double points of a link projection · Height of a parameter point · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Used byThe under-strand preimage exists and is unique · The under-strand lies strictly below the over-strand · The under-strand preimage lies over its crossing · Under-strand preimage of a crossing · Over and under preimages differ

TheoremThe over-strand preimage exists and is unique#✓fully proved

Let \(L\) be a parametrized link with \(n\) components whose standard projection is regular, and let \(p\) be a crossing of that projection. There is exactly one parameter point \(a\) of \(L\) that is an over-strand preimage of \(p\): the projected point of \(a\) is \(p\), and every other parameter point whose projected point is \(p\) has height strictly less than the height of \(a\).

theorem ParametrizedLink.existsUnique_isOverPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : ∃! a, L.IsOverPoint p a
Uses 11 · Used by 4
Statement usesParametrized link · Crossings of a link projection · Being the over-strand preimage of a crossing · Regular projections · Parameter point
Proof usesDouble points of a link projection · Double points have exactly two preimages · Height of a parameter point · Points with the same projection have different heights · Projected point of a link at a parameter point · Euclidean plane
Used byThe under-strand lies strictly below the over-strand · Over-strand preimage of a crossing · The over-strand preimage lies over its crossing · Over and under preimages differ

TheoremThe under-strand preimage exists and is unique#✓fully proved

Let \(L\) be a parametrized link with \(n\) components whose standard projection is regular, and let \(p\) be a crossing of that projection. There is exactly one parameter point \(a\) of \(L\) that is an under-strand preimage of \(p\): the projected point of \(a\) is \(p\), and every other parameter point whose projected point is \(p\) has height strictly greater than the height of \(a\).

theorem ParametrizedLink.existsUnique_isUnderPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : ∃! a, L.IsUnderPoint p a
Uses 11 · Used by 4
Statement usesParametrized link · Crossings of a link projection · Regular projections · Being the under-strand preimage of a crossing · Parameter point
Proof usesDouble points of a link projection · Double points have exactly two preimages · Height of a parameter point · Points with the same projection have different heights · Projected point of a link at a parameter point · Euclidean plane
Used byThe under-strand lies strictly below the over-strand · The under-strand preimage lies over its crossing · Under-strand preimage of a crossing · Over and under preimages differ

DefinitionOver-strand preimage of a crossing#✓fully proved

Let \(L\) be a parametrized link with \(n\) components whose standard projection is regular, and let \(p\) be a crossing of that projection. The over-strand preimage of \(p\) is the unique parameter point \(a\) of \(L\) that projects to \(p\) and such that every other parameter point projecting to \(p\) has strictly smaller height than \(a\).

noncomputable def ParametrizedLink.overPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : RegularProjection.ParamPoint n :=
  Classical.choose (L.existsUnique_isOverPoint hreg p)
Uses 6 · Used by 6
Statement usesParametrized link · Crossings of a link projection · Being the over-strand preimage of a crossing · Regular projections · The over-strand preimage exists and is unique · Parameter point
Used byThe over and under preimages exhaust a crossing · The under-strand lies strictly below the over-strand · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · The over-strand preimage lies over its crossing · Over and under preimages differ

DefinitionUnder-strand preimage of a crossing#✓fully proved

Let \(L\) be a parametrized link whose standard projection is regular, and let \(p\) be a crossing of this projection. The under-strand preimage of \(p\) is the unique parameter point \(a\) of \(L\) that projects to \(p\) and whose height is strictly less than the height of every other parameter point projecting to \(p\); the height of a parameter point is the third coordinate of the corresponding point of \(L\) in \(\mathbb{R}^3\).

noncomputable def ParametrizedLink.underPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : RegularProjection.ParamPoint n :=
  Classical.choose (L.existsUnique_isUnderPoint hreg p)
Uses 6 · Used by 5
Statement usesParametrized link · Crossings of a link projection · Regular projections · Being the under-strand preimage of a crossing · The under-strand preimage exists and is unique · Parameter point
Used byThe over and under preimages exhaust a crossing · The under-strand lies strictly below the over-strand · The two preimages of a crossing have opposite status · The under-strand preimage lies over its crossing · Over and under preimages differ

TheoremOver and under preimages differ#✓fully proved

Let \(L\) be a parametrized link whose standard projection is regular, and let \(p\) be a crossing of this projection. Then the under-strand preimage of \(p\) and the over-strand preimage of \(p\) are distinct parameter points of \(L\).

theorem ParametrizedLink.underPoint_ne_overPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : L.underPoint hreg p ≠ L.overPoint hreg p
Uses 15 · Used by 3
Statement usesParametrized link · Crossings of a link projection · Regular projections · Over-strand preimage of a crossing · Under-strand preimage of a crossing · Parameter point
Proof usesBeing the over-strand preimage of a crossing · Being the under-strand preimage of a crossing · Double points of a link projection · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Double points have exactly two preimages · Height of a parameter point · Projected point of a link at a parameter point · Euclidean plane
Used byThe over and under preimages exhaust a crossing · The under-strand lies strictly below the over-strand · The two preimages of a crossing have opposite status

TheoremThe under-strand lies strictly below the over-strand#✓fully proved

Let \(L\) be a parametrized link with \(n\) components whose standard projection is regular, and let \(p\) be a crossing of that projection. The height of \(L\) at the under-strand preimage of \(p\) is strictly less than its height at the over-strand preimage of \(p\).

theorem ParametrizedLink.heightAt_underPoint_lt_overPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) :
    L.heightAt (L.underPoint hreg p) < L.heightAt (L.overPoint hreg p)
Uses 15
Statement usesParametrized link · Crossings of a link projection · Regular projections · Height of a parameter point · Over-strand preimage of a crossing · Under-strand preimage of a crossing
Proof usesBeing the over-strand preimage of a crossing · Being the under-strand preimage of a crossing · Double points of a link projection · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Projected point of a link at a parameter point · Over and under preimages differ · Parameter point · Euclidean plane

TheoremThe over-strand preimage lies over its crossing#✓fully proved

Let \(L\) be a parametrized link whose standard projection is regular, and let \(p\) be a crossing of \(L\), that is, a point of the double-point set of its projection. Then the projected point of the over-strand parameter point at \(p\) is \(p\).

theorem ParametrizedLink.projPoint_overPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : L.projPoint (L.overPoint hreg p) = p.1
Uses 11 · Used by 2
Statement usesParametrized link · Crossings of a link projection · Regular projections · Double points of a link projection · Over-strand preimage of a crossing · Projected point of a link at a parameter point · Euclidean plane
Proof usesBeing the over-strand preimage of a crossing · The over-strand preimage exists and is unique · Height of a parameter point · Parameter point
Used byThe over and under preimages exhaust a crossing · The two preimages of a crossing have opposite status

TheoremThe under-strand preimage lies over its crossing#✓fully proved

Let \(L\) be a parametrized link whose standard projection is regular, and let \(p\) be a crossing of \(L\), that is, a point of the double-point set of its projection. Then the projected point of the under-strand parameter point at \(p\) is \(p\).

theorem ParametrizedLink.projPoint_underPoint {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : L.projPoint (L.underPoint hreg p) = p.1
Uses 11 · Used by 2
Statement usesParametrized link · Crossings of a link projection · Regular projections · Double points of a link projection · Projected point of a link at a parameter point · Under-strand preimage of a crossing · Euclidean plane
Proof usesBeing the under-strand preimage of a crossing · The under-strand preimage exists and is unique · Height of a parameter point · Parameter point
Used byThe over and under preimages exhaust a crossing · The two preimages of a crossing have opposite status

TheoremThe over and under preimages exhaust a crossing#✓fully proved

Let \(L\) be a parametrized link with \(n\) components whose standard projection is regular, and let \(p\) be a crossing of that projection. Every parameter point of \(L\) whose projected point is \(p\) is either the over-strand preimage or the under-strand preimage of \(p\).

theorem ParametrizedLink.eq_overPoint_or_eq_underPoint_of_projPoint_eq {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) (c : RegularProjection.ParamPoint n)
    (hc : L.projPoint c = p.1) :
    c = L.overPoint hreg p ∨ c = L.underPoint hreg p
Uses 13 · Used by 1
Statement usesParametrized link · Crossings of a link projection · Regular projections · Double points of a link projection · Over-strand preimage of a crossing · Projected point of a link at a parameter point · Under-strand preimage of a crossing · Parameter point · Euclidean plane
Proof usesDouble points have exactly two preimages · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Over and under preimages differ
Used byThe two preimages of a crossing have opposite status

TheoremA crossing-free regular projection has crossing count zero#✓fully proved

If a parametrized link \(L\) has a regular standard projection whose double-point set is empty, then the crossing count of \(L\) is \(0\).

theorem ParametrizedLink.crossingCount_eq_zero_of_doublePointSet_eq_empty
    {n : ℕ} (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (h : L.doublePointSet = ∅) : L.crossingCount hreg = 0
Uses 6 · Used by 1
Statement usesParametrized link · Regular projections · Crossing count of a regular projection · Double points of a link projection · Euclidean plane
Proof usesCrossings of a link projection
Used byCrossing number zero from a crossing-free representative

TheoremA regular projection with a crossing has positive crossing count#✓fully proved

If a parametrized link \(L\) has a regular standard projection with at least one crossing, then the crossing count of \(L\) is positive.

theorem ParametrizedLink.crossingCount_pos_of_crossing {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (p : L.Crossing) : 0 < L.crossingCount hreg
Uses 6
Statement usesParametrized link · Crossings of a link projection · Regular projections · Crossing count of a regular projection
Proof usesDouble points of a link projection · Euclidean plane

DefinitionCrossing number of a link#✓fully proved

For an oriented labeled parametrized link \(L\) with \(n\) components, the crossing number of \(L\) is the infimum in \(\mathbb{N} \cup \{\infty\}\), over all parametrized links \(L'\) with \(n\) components that are ambient isotopic to \(L\) and whose standard projection to the plane is regular, of the number of crossings (double points) of that projection of \(L'\). It is \(\infty\) when no such \(L'\) exists.

Changing the projection direction is absorbed by varying the representative over its isotopy class.

noncomputable def ParametrizedLink.crossingNumber {n : ℕ}
    (L : ParametrizedLink n) : ℕ∞ :=
  ⨅ L' : ParametrizedLink n, ⨅ _ : L'.Isotopic L,
    ⨅ h : L'.IsRegularProjection, (L'.crossingCount h : ℕ∞)
Uses 4 · Used by 13
Statement usesParametrized link · Regular projections · Isotopy of parametrized links · Crossing count of a regular projection
Used byThe crossing number is an isotopy invariant · Crossing number zero from a crossing-free representative · Regular projections of isotopic links bound the crossing number · A link's own regular projection bounds its crossing number · Finiteness of the crossing number · Alternating link types have finite crossing number · Alternating link types have a natural-number crossing number · Admissible constants for the tight-knot inequality · Admissible constants for the tight alternating knot inequality · Zero is an admissible alternating constant · Zero is an admissible tight-knot constant · Admissible alternating constants are downward closed among nonnegative reals · Admissibility passes to smaller nonnegative constants

TheoremRegular projections of isotopic links bound the crossing number#✓fully proved

Let \(L\) and \(L'\) be oriented labeled parametrized links with \(n\) components, with \(L'\) ambient isotopic to \(L\), and suppose the standard projection of \(L'\) to the plane is regular. Then the crossing number of \(L\) is at most the number of crossings of this projection of \(L'\).

theorem ParametrizedLink.crossingNumber_le_of_isotopic_of_isRegularProjection
    {n : ℕ} {L L' : ParametrizedLink n} (h : L'.Isotopic L)
    (hreg : L'.IsRegularProjection) :
    L.crossingNumber ≤ (L'.crossingCount hreg : ℕ∞)
Uses 5 · Used by 4
Statement usesParametrized link · Regular projections · Isotopy of parametrized links · Crossing count of a regular projection · Crossing number of a link
Used byThe crossing number is an isotopy invariant · Crossing number zero from a crossing-free representative · A link's own regular projection bounds its crossing number · Finiteness of the crossing number

TheoremA link's own regular projection bounds its crossing number#✓fully proved

If the standard projection of an oriented labeled parametrized link \(L\) to the plane is regular, then the crossing number of \(L\) is at most the number of crossings of this projection.

theorem ParametrizedLink.crossingNumber_le_self_of_isRegularProjection
    {n : ℕ} (L : ParametrizedLink n) (hreg : L.IsRegularProjection) :
    L.crossingNumber ≤ (L.crossingCount hreg : ℕ∞)
Uses 12
Statement usesParametrized link · Regular projections · Crossing count of a regular projection · Crossing number of a link
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Identity ambient isotopy · Orientation-preserving reparametrization of the circle · Identity reparametrization of the circle · Parametrized knot · Isotopy of parametrized links · Regular projections of isotopic links bound the crossing number

TheoremFiniteness of the crossing number#✓fully proved

Let \(L\) and \(L'\) be oriented labeled parametrized links with \(n\) components. If \(L'\) is ambient isotopic to \(L\) and the standard projection of \(L'\) to the plane is regular, then the crossing number of \(L\) is finite.

theorem ParametrizedLink.crossingNumber_lt_top_of_isotopic_of_isRegularProjection
    {n : ℕ} {L L' : ParametrizedLink n} (h : L'.Isotopic L)
    (hreg : L'.IsRegularProjection) :
    L.crossingNumber < ⊤
Uses 6 · Used by 1
Statement usesParametrized link · Regular projections · Isotopy of parametrized links · Crossing number of a link
Proof usesCrossing count of a regular projection · Regular projections of isotopic links bound the crossing number
Used byAlternating link types have finite crossing number

TheoremThe crossing number is an isotopy invariant#✓fully proved

If two parametrized links \(L_1\) and \(L_2\) with \(n\) components are isotopic, then \(L_1\) and \(L_2\) have the same crossing number.

theorem ParametrizedLink.crossingNumber_eq_of_isotopic {n : ℕ}
    {L₁ L₂ : ParametrizedLink n} (h : L₁.Isotopic L₂) :
    L₁.crossingNumber = L₂.crossingNumber
Uses 14
Statement usesParametrized link · Isotopy of parametrized links · Crossing number of a link
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Composition of ambient isotopies · Inverse ambient isotopy · Orientation-preserving reparametrization of the circle · Composition of circle reparametrizations · Inverse circle reparametrization · Parametrized knot · Regular projections · Crossing count of a regular projection · Regular projections of isotopic links bound the crossing number

TheoremCrossing number zero from a crossing-free representative#✓fully proved

Let \(L\) and \(L'\) be parametrized links with \(n\) components such that \(L'\) is isotopic to \(L\). If the standard projection of \(L'\) is regular and its double-point set is empty, then the crossing number of \(L\) is \(0\).

theorem ParametrizedLink.crossingNumber_eq_zero_of_isotopic_of_doublePointSet_eq_empty
    {n : ℕ} {L L' : ParametrizedLink n} (h : L'.Isotopic L)
    (hreg : L'.IsRegularProjection) (hempty : L'.doublePointSet = ∅) :
    L.crossingNumber = 0
Uses 9
Statement usesParametrized link · Regular projections · Isotopy of parametrized links · Crossing number of a link · Double points of a link projection · Euclidean plane
Proof usesCrossing count of a regular projection · A crossing-free regular projection has crossing count zero · Regular projections of isotopic links bound the crossing number

DefinitionCrossing preimages#✓fully proved

A parameter point \(a\) of a parametrized link \(L\) (a component of \(L\) together with a parameter in \([0, 2\pi)\)) is a crossing preimage when its image under the standard projection to the plane lies in the double-point set of \(L\).

def ParametrizedLink.IsCrossingPreimage {n : ℕ} (L : ParametrizedLink n)
    (a : RegularProjection.ParamPoint n) : Prop :=
  L.projPoint a ∈ L.doublePointSet
Uses 5 · Used by 5
Statement usesParametrized link · Double points of a link projection · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Used byCyclically adjacent crossing preimages · Alternating regular projections · Crossingless regular projections are alternating · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status

DefinitionOver/under status at a crossing preimage#✓fully proved

Let \(L\) be a parametrized link whose standard projection to the plane is regular, and let \(a\) be a crossing preimage of \(L\). The over/under status at \(a\) is true when \(a\) is the over-strand preimage of the crossing at the projection of \(a\), that is, the preimage of that crossing of greatest height, and false otherwise.

noncomputable def ParametrizedLink.isOverAt {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (a : RegularProjection.ParamPoint n)
    (ha : L.IsCrossingPreimage a) : Bool :=
  if a = L.overPoint hreg ⟨L.projPoint a, ha⟩ then true else false
Uses 8 · Used by 3
Statement usesParametrized link · Crossing preimages · Regular projections · Double points of a link projection · Over-strand preimage of a crossing · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Used byAlternating regular projections · Crossingless regular projections are alternating · The two preimages of a crossing have opposite status

TheoremThe two preimages of a crossing have opposite status#✓fully proved

Let \(L\) be a parametrized link whose standard projection to the plane is regular. If \(a \ne b\) are crossing preimages of \(L\) with the same projection, then the over/under status at \(a\) differs from the over/under status at \(b\).

theorem ParametrizedLink.isOverAt_ne_of_ne_of_projPoint_eq {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    {a b : RegularProjection.ParamPoint n}
    (ha : L.IsCrossingPreimage a) (hb : L.IsCrossingPreimage b)
    (hab : a ≠ b) (hproj : L.projPoint a = L.projPoint b) :
    L.isOverAt hreg a ha ≠ L.isOverAt hreg b hb
Uses 15
Statement usesParametrized link · Crossing preimages · Regular projections · Over/under status at a crossing preimage · Projected point of a link at a parameter point · Parameter point · Euclidean plane
Proof usesCrossings of a link projection · Double points of a link projection · The over and under preimages exhaust a crossing · Over-strand preimage of a crossing · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Under-strand preimage of a crossing · Over and under preimages differ

DefinitionOpen arc on the parameter circle#✓fully proved

Let \(a\), \(b\), \(c\) be parameter points with parameters \(s\), \(u\), \(t \in [0, 2\pi)\) respectively. Then \(c\) lies in the open counterclockwise arc from \(a\) to \(b\) when \(s < t < u\) in case \(s < u\), and when \(s < t\) or \(t < u\) in case \(u \le s\). Only the parameters are compared; the components of \(a\), \(b\), \(c\) play no role.

def inOpenArc {n : ℕ} (a b c : RegularProjection.ParamPoint n) : Prop :=
  if a.t < b.t then a.t < c.t ∧ c.t < b.t else a.t < c.t ∨ c.t < b.t
Uses 1 · Used by 3
Statement usesParameter point
Used byCyclically adjacent crossing preimages · Alternating regular projections · Crossingless regular projections are alternating

DefinitionCyclically adjacent crossing preimages#✓fully proved

Let \(L\) be an oriented labeled parametrized link, with each component parametrized by \(t \in [0, 2\pi)\). Two distinct parameter points \(a\) and \(b\) of \(L\) on the same component are cyclically adjacent, in this order, when both are crossing preimages (they project to double points of the standard projection) and no crossing preimage on that component lies in the open arc from \(a\) to \(b\) in the direction of increasing parameter, wrapping around from \(2\pi\) to \(0\) when the parameter of \(b\) is smaller than that of \(a\).

def ParametrizedLink.CyclicallyAdjacent {n : ℕ}
    (L : ParametrizedLink n) (a b : RegularProjection.ParamPoint n) :
    Prop :=
  a.comp = b.comp ∧ a ≠ b ∧ L.IsCrossingPreimage a ∧
    L.IsCrossingPreimage b ∧
    ∀ c : RegularProjection.ParamPoint n, L.IsCrossingPreimage c →
      c.comp = a.comp → ¬ inOpenArc a b c
Uses 4 · Used by 2
Statement usesParametrized link · Crossing preimages · Open arc on the parameter circle · Parameter point
Used byAlternating regular projections · Crossingless regular projections are alternating

DefinitionAlternating regular projections#✓fully proved

Let \(L\) be a parametrized link whose standard projection to the plane is regular. The projection is alternating when, for any two cyclically adjacent crossing preimages \(a\) and \(b\) of \(L\) (distinct, on the same component, with no other crossing preimage of that component in the open arc of parameters from \(a\) to \(b\)), the over/under status at \(a\) differs from the over/under status at \(b\).

A component with at most one crossing preimage imposes no condition.

def ParametrizedLink.IsAlternatingProjection {n : ℕ}
    (L : ParametrizedLink n) (hreg : L.IsRegularProjection) : Prop :=
  ∀ a b : RegularProjection.ParamPoint n,
    ∀ hadj : L.CyclicallyAdjacent a b,
      L.isOverAt hreg a hadj.2.2.1 ≠ L.isOverAt hreg b hadj.2.2.2.1
Uses 7 · Used by 5
Statement usesParametrized link · Cyclically adjacent crossing preimages · Crossing preimages · Regular projections · Over/under status at a crossing preimage · Open arc on the parameter circle · Parameter point
Used byLinks admitting an alternating diagram · Links with a crossing-free regular projection admit alternating diagrams · Crossingless regular projections are alternating · Admitting an alternating diagram is an isotopy invariant · Alternating link types have finite crossing number

TheoremCrossingless regular projections are alternating#✓fully proved

Let \(L\) be a parametrized link whose standard projection to the plane is regular. If the double-point set of this projection is empty, then the projection is alternating.

theorem ParametrizedLink.isAlternatingProjection_of_doublePointSet_eq_empty
    {n : ℕ} (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (hempty : L.doublePointSet = ∅) :
    L.IsAlternatingProjection hreg
Uses 11 · Used by 1
Statement usesParametrized link · Alternating regular projections · Regular projections · Double points of a link projection · Euclidean plane
Proof usesCyclically adjacent crossing preimages · Crossing preimages · Over/under status at a crossing preimage · Projected point of a link at a parameter point · Open arc on the parameter circle · Parameter point
Used byLinks with a crossing-free regular projection admit alternating diagrams

DefinitionLinks admitting an alternating diagram#✓fully proved

A parametrized link \(L\) with \(n\) components admits an alternating diagram when there is a parametrized link \(L'\) isotopic to \(L\) whose standard projection is regular and alternating.

def ParametrizedLink.AdmitsAlternatingDiagram {n : ℕ}
    (L : ParametrizedLink n) : Prop :=
  ∃ L' : ParametrizedLink n, L'.Isotopic L ∧
    ∃ hreg : L'.IsRegularProjection, L'.IsAlternatingProjection hreg
Uses 4 · Used by 7
Statement usesParametrized link · Alternating regular projections · Regular projections · Isotopy of parametrized links
Used byLinks with a crossing-free regular projection admit alternating diagrams · Admitting an alternating diagram is an isotopy invariant · Alternating link types have finite crossing number · Alternating link types have a natural-number crossing number · Admissible constants for the tight alternating knot inequality · Zero is an admissible alternating constant · Admissible alternating constants are downward closed among nonnegative reals

TheoremAdmitting an alternating diagram is an isotopy invariant#✓fully proved

Let \(L_1\) and \(L_2\) be parametrized links with \(n\) components. If \(L_1\) is isotopic to \(L_2\) and \(L_1\) admits an alternating diagram, then \(L_2\) admits an alternating diagram.

theorem ParametrizedLink.AdmitsAlternatingDiagram.of_isotopic {n : ℕ}
    {L₁ L₂ : ParametrizedLink n} (h : L₁.Isotopic L₂)
    (hL : L₁.AdmitsAlternatingDiagram) :
    L₂.AdmitsAlternatingDiagram
Uses 11
Statement usesParametrized link · Links admitting an alternating diagram · Isotopy of parametrized links
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Composition of ambient isotopies · Orientation-preserving reparametrization of the circle · Composition of circle reparametrizations · Parametrized knot · Alternating regular projections · Regular projections

TheoremLinks with a crossing-free regular projection admit alternating diagrams#✓fully proved

If a parametrized link \(L\) has a regular standard projection whose double-point set is empty, then \(L\) admits an alternating diagram.

The witness is \(L\) itself, whose projection is alternating vacuously since it has no crossings.

theorem ParametrizedLink.admitsAlternatingDiagram_of_doublePointSet_eq_empty
    {n : ℕ} (L : ParametrizedLink n) (hreg : L.IsRegularProjection)
    (hempty : L.doublePointSet = ∅) :
    L.AdmitsAlternatingDiagram
Uses 14
Statement usesParametrized link · Links admitting an alternating diagram · Regular projections · Double points of a link projection · Euclidean plane
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Identity ambient isotopy · Orientation-preserving reparametrization of the circle · Identity reparametrization of the circle · Parametrized knot · Alternating regular projections · Isotopy of parametrized links · Crossingless regular projections are alternating

TheoremThe projected trace is the union of the projected components#✓fully proved

For a parametrized link \(L\) with \(n\) components, the union over all components \(i\) of the images of the projected curves of \(L\) equals the image of the trace of \(L\) under the standard projection to the plane.

theorem ParametrizedLink.iUnion_range_projCurve {n : ℕ}
    (L : ParametrizedLink n) :
    ⋃ i, Set.range (L.projCurve i) = RegularProjection.plane '' L.trace
Uses 7
Statement usesEuclidean 3-space · Parametrized link · Projected curve of a link component · Trace of a parametrized link · Euclidean plane · Standard projection to the plane
Proof usesParametrized knot

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.