A loop crossing a disk transversally crosses it at only finitely many points
ProvedHryniewiczCriterion.finite_transverse_disk_crossingsdynamical-systemsgeometry-topologysymplectic-geometry
Let be on an open neighbourhood of the closed unit disk and let be a loop of period . Suppose that at every crossing with ,
(rows of a matrix). Then the set of crossing points is finite.
Proof. At a crossing the three vectors are linearly independent, so the map from to has injective differential there and is injective near (inverse function theorem / local left inverse). Hence crossings are isolated in , a compact set, so there are finitely many pairs with , and by periodicity every crossing point arises from such a pair.
Preamble
import Definitions.Def_HryniewiczCriterion_GlobalSection import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion
Formal statement
theorem HryniewiczCriterion.finite_transverse_disk_crossings (E : Plane → R4) (U : Set Plane) (hU : IsOpen U) (hDU : closedUnitDisk ⊆ U)
(hE : ContDiffOn ℝ 1 E U)
(γ : ℝ → R4) (hγ : ContDiff ℝ 1 γ) (hγper : ∀ t, γ (t + 1) = γ t)
(htr : ∀ t, ∀ v ∈ closedUnitDisk, E v = γ t →
Matrix.det (Matrix.of ![γ t, deriv γ t,
fderiv ℝ E v (Pi.single 0 1), fderiv ℝ E v (Pi.single 1 1)]) ≠ 0) :
{v : Plane | v ∈ closedUnitDisk ∧ ∃ t, E v = γ t}.Finite := by sorrySource
Standard transversality and compactness argument, e.g. D. Rolfsen, Knots and Links, Publish or Perish 1976, Ch. 5D (linking number = algebraic intersection number with a Seifert surface)