Prove2Me

Strict pullback of the Hopf family intertwines its Reeb fields

Proved
ContactCalculus.strict_hopf_pullback_intertwines

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrydifferential-geometrydynamical-systems

Let S3S^3 be the unit sphere in R4\mathbb R^4, and set

αt=x1 dy1−y1 dx1+(1+t)(x2 dy2−y2 dx2).\alpha_t=x_1\,dy_1-y_1\,dx_1+(1+t)(x_2\,dy_2-y_2\,dx_2).

For t≥0t\ge0, let ff be a smooth ambient map restricting to a bijection of the sphere, with injective tangent differential, and suppose f∗αt=α0f^*\alpha_t=\alpha_0 on its tangent bundle. Then

DfyR0(y)=Rt(f(y))(y∈S3),Df_y R_0(y)=R_t(f(y))\qquad(y\in S^3),

where Rt=(−y1,y0,−y3/(1+t),y2/(1+t))R_t=(-y_1,y_0,-y_3/(1+t),y_2/(1+t)). This is the strict contact naturality of the Reeb vector field for Geiges's family, and can be reused to compare its dynamics.

Preamble
import Definitions.Def_GrayStability_HopfFamily
import Mathlib.Data.Fin.VecNotation

set_option autoImplicit false
open GrayStability
open scoped ContDiff
Formal statement
theorem ContactCalculus.strict_hopf_pullback_intertwines (t : ℝ) (ht : 0 ≤ t)
    (f : E 4 → E 4) (hf : ContDiff ℝ ∞ f)
    (hbij : Set.BijOn f (levelSet unitSphereEquation) (levelSet unitSphereEquation))
    (hinj : ∀ y ∈ levelSet unitSphereEquation,
      Set.InjOn (fderiv ℝ f y) (tangentSpace unitSphereEquation y))
    (hα : ∀ y ∈ levelSet unitSphereEquation, ∀ v ∈ tangentSpace unitSphereEquation y,
      pullback f (hopfFamily t) y v = hopfFamily 0 y v) :
    ∀ y ∈ levelSet unitSphereEquation,
      fderiv ℝ f y ![-y 1, y 0, -y 3, y 2] =
        ![-(f y) 1, (f y) 0, -(f y) 3 / (1 + t), (f y) 2 / (1 + t)] := by sorry
Source
Geiges, Contact geometry, https://arxiv.org/pdf/math/0307242, Remark 2.21(1), printed p. 15. The displayed Reeb field and its naturality under strict pullback.

View graph