Anosov plugs VII: embedded tori transverse to a flow, isotopy of tori

Definition

AnosovPlugs_Tori

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Let $\mathbb T^2=S^1\times S^1$ with its standard smooth structure and $M$ a 3-manifold.

Embedded torus: an injective C¹ immersion $f:\mathbb T^2\to M$ (a C¹ embedding, $\mathbb T^2$ being compact).
Transverse torus: an embedded torus such that the vector field $X$ is nowhere tangent to it: $X(f(p))\notin \operatorname{im} Df_p$ .
Isotopic tori: $f_1,f_2$ are isotopic if there is a C¹ family $(F_t)_{t\in[0,1]}$ of embedded tori with $F_0=f_1$ and $F_1(\mathbb T^2)=f_2(\mathbb T^2)$ .

Formalization Note Isotopy is between embedded surfaces (images), in the C¹ category.

Definition code

import Mathlib
import Definitions.Def_AnosovPlugs_Flows

/-!
Béguin–Bonatti–Yu, *Building Anosov flows on 3-manifolds*, Geom. Topol. 21 (2017).
Embedded tori transverse to a vector field, and isotopy of embedded tori (§1.4.5).
The torus is `𝕋² = S¹ × S¹` with its standard smooth structure.
-/

open scoped Manifold ContDiff Topology
open Set Function

namespace AnosovPlugs

/-- The model of the torus `S¹ × S¹`. -/
noncomputable abbrev ITorus := (𝓡 1).prod (𝓡 1)

variable {M : Type} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M]
  [IsManifold I3 ∞ M]

/-- `f : S¹ × S¹ → M` is an embedded torus: an injective C¹ immersion (hence, the torus being
compact, a C¹ embedding). -/
def IsEmbeddedTorus (f : Circle × Circle → M) : Prop :=
  ContMDiff ITorus I3 1 f ∧ Injective f ∧ ∀ p, Injective (mfderiv ITorus I3 f p)

/-- The embedded torus `f` is transverse to the vector field `X`: at every point of the torus,
`X` is not tangent to the torus. -/
def IsTransverseTorus (X : (x : M) → TangentSpace I3 x) (f : Circle × Circle → M) : Prop :=
  IsEmbeddedTorus f ∧ ∀ p, X (f p) ∉ LinearMap.range (mfderiv ITorus I3 f p).toLinearMap

/-- The embedded tori `f₁` and `f₂` are isotopic: there is a C¹ family `(F_t)_{t ∈ [0,1]}` of
embedded tori with `F₀ = f₁` and `F₁` having the same image as `f₂`. -/
def ToriIsotopic (f₁ f₂ : Circle × Circle → M) : Prop :=
  ∃ F : ℝ × (Circle × Circle) → M, ContMDiff (𝓘(ℝ, ℝ).prod ITorus) I3 1 F ∧
    (∀ t ∈ Icc (0 : ℝ) 1, IsEmbeddedTorus fun p => F (t, p)) ∧
    (∀ p, F (0, p) = f₁ p) ∧ range (fun p => F (1, p)) = range f₂

end AnosovPlugs

Source

F. Béguin, C. Bonatti, B. Yu, *Building Anosov flows on 3-manifolds*, Geom. Topol. 21 (2017) 1837–1930, https://doi.org/10.2140/gt.2017.21.1837, §1.4.5, Theorem 1.15 (p. 1847)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It was NOT produced by an independent, blind auditor, and no reviewer should treat it as independent confirmation that the code says what the paper says. Compare it against the Lean code yourself.

$\mathbb T^2$ is Mathlib's Circle × Circle with the product manifold structure (model $\mathcal R^1\times\mathcal R^1$ ); $M$ is a charted space over the half-space in $\mathbb R^3$ with $C^\infty$ structure.

IsEmbeddedTorus $f$ ( $f:\mathbb T^2\to M$ ): $f$ is $C^1$ , injective, and its derivative $Df_p$ is injective at every $p$ .
IsTransverseTorus $X\,f$ : IsEmbeddedTorus $f$ and for every $p$ , $X(f(p))$ is not in the image of $Df_p$ .
ToriIsotopic $f_1\,f_2$ : there is $F:\mathbb R\times\mathbb T^2\to M$ , $C^1$ on all of $\mathbb R\times\mathbb T^2$ , such that $p\mapsto F(t,p)$ is an embedded torus for every $t\in[0,1]$ , $F(0,p)=f_1(p)$ for all $p$ , and the image of $p\mapsto F(1,p)$ equals the image of $f_2$ .

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph