Leaves of a foliation

This file defines the leaves of a foliation of a real manifold through the curves tangent to the foliation: two points lie on the same leaf when they are joined by a finite chain of curves, each C¹ on a compact interval, whose velocities lie in the tangent distribution. On a boundaryless real manifold modelled on a finite-dimensional space, the flat charts of the Frobenius theorem make a curve tangent to the foliation have locally constant transverse coordinates, so that there these leaves are the leaves in the chart sense, the maximal connected integral manifolds of the tangent distribution; conversely, any two points of a connected integral manifold are joined by such a chain inside it.

The leaves partition the manifold, and each leaf is path-connected. For the foliation of a real normed space E by the translates of a finite-dimensional subspace S, the leaf through x is the affine subspace x + S.

Leaves are the objects that tautness of a codimension-one foliation (a closed transversal meeting every leaf) and the Euler-class bound on its leaves refer to.

Main definitions

• TauCeti.Foliation.JoinedByTangentCurve F x y: some curve, C¹ on [0, 1], runs from x to y with velocity in the tangent distribution of F throughout; this is unfolded by TauCeti.Foliation.joinedByTangentCurve_iff.
• TauCeti.Foliation.SameLeaf F: the equivalence relation generated by JoinedByTangentCurve F.
• TauCeti.Foliation.leaf F x: the leaf of F through x.

Main results

• TauCeti.Foliation.sameLeaf_equivalence: lying on the same leaf is an equivalence relation, and TauCeti.Foliation.sameLeaf_le says it is the least one relating the ends of tangent curves.
• TauCeti.Foliation.sameLeaf_of_contMDiffOn_of_tangent: a curve tangent to F on a compact interval stays in one leaf.
• TauCeti.Foliation.leaf_eq_leaf_iff and TauCeti.Foliation.disjoint_leaf_iff: two leaves are equal or disjoint.
• TauCeti.Foliation.isPathConnected_leaf: every leaf is path-connected.
• TauCeti.Foliation.leaf_ofSubmodule: the leaves of the foliation of E by the translates of S are these translates.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19 (integral manifolds, the Frobenius theorem, and the leaves of a foliation).
• A. Candel, L. Conlon, Foliations I, AMS GSM 23 (2000), Chapter 1.

def TauCeti.Foliation.JoinedByTangentCurve {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) (x y : M) : Prop

The points x and y are the ends of a curve tangent to the foliation F: some curve γ, C¹ on [0, 1], runs from γ 0 = x to γ 1 = y, and at every parameter of [0, 1] its velocity within [0, 1] lies in the tangent space of F.

def TauCeti.Foliation.SameLeaf {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) (x y : M) : Prop

The points x and y lie on the same leaf of the foliation F: they are related by the equivalence relation generated by JoinedByTangentCurve F, that is, joined by a finite chain of curves tangent to F.

def TauCeti.Foliation.leaf {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) (x : M) : Set M

The leaf of the foliation F through x: the points lying on the same leaf as x.

theorem TauCeti.Foliation.joinedByTangentCurve_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} {x y : M} : F.JoinedByTangentCurve x y ↔ ∃ (γ : ℝ → M), ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1) ∧ (∀ t ∈ Set.Icc 0 1, Manifold.curveVelocityWithin I γ (Set.Icc 0 1) t ∈ F.distribution (γ t)) ∧ γ 0 = x ∧ γ 1 = y

The points x and y are the ends of a curve tangent to F exactly when some curve γ, C¹ on [0, 1] with velocity within [0, 1] in the tangent space of F throughout, runs from γ 0 = x to γ 1 = y.

theorem TauCeti.Foliation.JoinedByTangentCurve.sameLeaf {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} {x y : M} (h : F.JoinedByTangentCurve x y) : F.SameLeaf x y

The ends of a curve tangent to F lie on the same leaf.

theorem TauCeti.Foliation.sameLeaf_equivalence {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) : Equivalence F.SameLeaf

Lying on the same leaf of F is an equivalence relation.

theorem TauCeti.Foliation.sameLeaf_le {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} {r : M → M → Prop} (hr : Equivalence r) (h : F.JoinedByTangentCurve ≤ r) : F.SameLeaf ≤ r

Lying on the same leaf of F is the least equivalence relation relating the ends of every curve tangent to F.

@[simp]

theorem TauCeti.Foliation.SameLeaf.refl {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) (x : M) : F.SameLeaf x x

Every point lies on its own leaf.

theorem TauCeti.Foliation.SameLeaf.symm {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} {x y : M} (h : F.SameLeaf x y) : F.SameLeaf y x

Lying on the same leaf is symmetric.

theorem TauCeti.Foliation.SameLeaf.trans {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} {x y z : M} (hxy : F.SameLeaf x y) (hyz : F.SameLeaf y z) : F.SameLeaf x z

Lying on the same leaf is transitive.

theorem TauCeti.Foliation.SameLeaf.induction_on {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} {x y : M} {motive : M → M → Prop} (h : F.SameLeaf x y) (rel : ∀ (x y : M), F.JoinedByTangentCurve x y → motive x y) (refl : ∀ (x : M), motive x x) (symm : ∀ (x y : M), F.SameLeaf x y → motive x y → motive y x) (trans : ∀ (x y z : M), F.SameLeaf x y → F.SameLeaf y z → motive x y → motive y z → motive x z) : motive x y

Induction principle for lying on the same leaf of F: a property of pairs of points holds for all pairs on the same leaf once it holds for the ends of every curve tangent to F and is preserved by reflexivity, symmetry, and transitivity.

theorem TauCeti.Foliation.sameLeaf_comm {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} {x y : M} : F.SameLeaf x y ↔ F.SameLeaf y x

Lying on the same leaf is symmetric, as an equivalence.

@[simp]

theorem TauCeti.Foliation.mem_leaf {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} {x y : M} : y ∈ F.leaf x ↔ F.SameLeaf x y

The leaf through x consists of the points lying on the same leaf as x.

theorem TauCeti.Foliation.mem_leaf_self {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) (x : M) : x ∈ F.leaf x

Every point lies on the leaf through it.

@[simp]

theorem TauCeti.Foliation.leaf_eq_leaf_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} {x y : M} : F.leaf x = F.leaf y ↔ F.SameLeaf x y

Two leaves are equal exactly when their base points lie on the same leaf.

theorem TauCeti.Foliation.leaf_eq_of_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} {x y : M} (h : y ∈ F.leaf x) : F.leaf y = F.leaf x

The leaf through any point of a leaf is that leaf.

@[simp]

theorem TauCeti.Foliation.disjoint_leaf_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} {x y : M} : Disjoint (F.leaf x) (F.leaf y) ↔ ¬F.SameLeaf x y

Two leaves are disjoint exactly when their base points do not lie on the same leaf; so the leaves of a foliation partition the manifold.

theorem TauCeti.Foliation.sameLeaf_of_contMDiffOn_of_tangent {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} {a b s t : ℝ} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc a b)) (htan : ∀ u ∈ Set.Icc a b, Manifold.curveVelocityWithin I γ (Set.Icc a b) u ∈ F.distribution (γ u)) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : F.SameLeaf (γ s) (γ t)

A curve which is C¹ on a compact interval [a, b] and tangent to F there stays in one leaf of F.

theorem TauCeti.Foliation.isPathConnected_leaf {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) (x : M) : IsPathConnected (F.leaf x)

Every leaf of a foliation is path-connected.

@[simp]

theorem TauCeti.Foliation.sameLeaf_ofSubmodule_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} (S : Submodule ℝ E) [FiniteDimensional ℝ ↥S] (hn : 1 ≤ n) {x y : E} : (ofSubmodule S hn).SameLeaf x y ↔ y - x ∈ S

In the foliation of E by the translates of S, two points lie on the same leaf exactly when their difference lies in S.

@[simp]

theorem TauCeti.Foliation.leaf_ofSubmodule {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} (S : Submodule ℝ E) [FiniteDimensional ℝ ↥S] (hn : 1 ≤ n) (x : E) : (ofSubmodule S hn).leaf x = {y : E | y - x ∈ S}

The leaf through x of the foliation of E by the translates of S is the translate x + S.