Transversals and taut foliations

A closed transversal to a foliation is a C¹ periodic curve whose velocity is everywhere transverse to the tangent distribution. The definition uses complementary submodules, so it does not silently assume a codimension: a one-dimensional transversal can exist only when the distribution has the corresponding codimension. A foliation is taut when every leaf meets one of these curves.

The obstruction theorem gives a concrete example. The foliation of a finite-dimensional normed space by the affine cosets of the kernel of a continuous linear functional has a global first integral. Rolle's theorem forces every closed C¹ curve to have velocity in that kernel somewhere, so this foliation is not taut.

The terminology follows Calegari, Foliations and the Geometry of 3-Manifolds, Chapter 4.

def TauCeti.Foliation.IsClosedTransversal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] (F : Foliation I n M k) (γ : ℝ → M) : Prop

A C¹ closed curve is transverse to F when its velocity and the leaf tangent space are complementary at every parameter value.

@[simp]

theorem TauCeti.Foliation.isClosedTransversal_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] (F : Foliation I n M k) (γ : ℝ → M) : F.IsClosedTransversal γ ↔ ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ ∧ (∀ (t : ℝ), γ (t + 1) = γ t) ∧ ∀ (t : ℝ), Manifold.curveVelocity I γ t ≠ 0 ∧ IsCompl (ℝ ∙ Manifold.curveVelocity I γ t) (F.distribution (γ t))

A closed transversal is characterized by pointwise periodicity and its defining fields.

def TauCeti.Foliation.Taut {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] (F : Foliation I n M k) : Prop

A foliation is taut when every leaf meets a C¹ closed transversal.

theorem TauCeti.Foliation.Taut.mk {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} (h : ∀ (x : M), ∃ (γ : ℝ → M), F.IsClosedTransversal γ ∧ ∃ (t : ℝ), γ t ∈ F.leaf x) : F.Taut

Construct a taut foliation from a closed transversal meeting every leaf.

theorem TauCeti.Foliation.Taut.exists_transversal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} (h : F.Taut) (x : M) : ∃ (γ : ℝ → M), F.IsClosedTransversal γ ∧ ∃ (t : ℝ), γ t ∈ F.leaf x

A taut foliation has a closed transversal meeting each specified leaf.

theorem TauCeti.Foliation.IsClosedTransversal.contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} {γ : ℝ → M} (hγ : F.IsClosedTransversal γ) : ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ

The C¹ regularity field of a closed transversal.

theorem TauCeti.Foliation.IsClosedTransversal.velocity_ne_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} {γ : ℝ → M} (hγ : F.IsClosedTransversal γ) (t : ℝ) : Manifold.curveVelocity I γ t ≠ 0

The nonzero velocity field of a closed transversal.

theorem TauCeti.Foliation.IsClosedTransversal.isCompl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} {γ : ℝ → M} (hγ : F.IsClosedTransversal γ) (t : ℝ) : IsCompl (ℝ ∙ Manifold.curveVelocity I γ t) (F.distribution (γ t))

The complementary-distribution field of a closed transversal.

theorem TauCeti.Foliation.IsClosedTransversal.periodic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} {γ : ℝ → M} (hγ : F.IsClosedTransversal γ) : Function.Periodic γ 1

A closed transversal is 1-periodic.

theorem TauCeti.Foliation.IsClosedTransversal.velocity_not_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] {F : Foliation I n M k} {γ : ℝ → M} (hγ : F.IsClosedTransversal γ) (t : ℝ) : Manifold.curveVelocity I γ t ∉ F.distribution (γ t)

The velocity of a closed transversal never belongs to the leaf distribution.

theorem TauCeti.Foliation.not_isClosedTransversal_ofSubmodule_ker {n : WithTop ℕ∞} {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ℓ : V →L[ℝ] ℝ) (hn : 1 ≤ n) {γ : ℝ → V} (hγ : (ofSubmodule (↑ℓ).ker hn).IsClosedTransversal γ) : False

The foliation by kernels of a continuous linear functional admits no closed transversal.

theorem TauCeti.Foliation.not_taut_ofSubmodule_ker {n : WithTop ℕ∞} {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ℓ : V →L[ℝ] ℝ) (hn : 1 ≤ n) : ¬(ofSubmodule (↑ℓ).ker hn).Taut

The foliation by affine cosets of the kernel of a continuous linear functional is not taut.