Foliations

A foliation of rank k of a manifold M decomposes M into k-dimensional immersed submanifolds, its leaves. This library defines a foliation by its tangent distribution, the field of tangent spaces of the leaves: here a C^n foliation of rank k, for 1 ≤ n, is by definition a C^n involutive distribution of rank k, over any nontrivially normed field and model space. In the classical setting of a real manifold modelled on a finite-dimensional space, the Frobenius theorem, which is not proved here, makes such a distribution the tangent field of a unique foliation in the chart sense, the leaves being its maximal connected integral manifolds, so that there the distribution is the data of the foliation. The regularity 1 ≤ n is required: a C⁰ foliation need not have a continuous tangent field, and for a merely continuous distribution the involutivity condition, which tests only differentiable tangent vector fields, need not constrain it. The manifold M is required to be C^(n+1), so that its tangent bundle is a C^n vector bundle and a C^n distribution is a C^n subbundle of it; on a less regular manifold the regularity of the distribution would not be meaningful (the rank-zero distribution, for instance, would be C^n for every n).

A foliation is data rather than a property of M, so it is a structure, bundling the distribution with its regularity and involutivity. The foliation of a normed space by the translates of a finite-dimensional subspace is the basic example.

Main definitions

• TauCeti.Foliation I n M k: the C^n foliations of rank k of a C^(n+1) manifold M.
• TauCeti.Foliation.ofSubmodule S hn: the foliation of a normed space E by the translates of a finite-dimensional subspace S.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19.
• A. Candel, L. Conlon, Foliations I, AMS GSM 23 (2000), Chapter 1.
• D. Calegari, Foliations and the Geometry of 3-Manifolds, Oxford (2007), Chapter 4.

structure TauCeti.Foliation {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (k : ℕ) [IsManifold I (n + 1) M] : Type (max u_2 u_4)

A C^n foliation of the C^(n+1) manifold M of rank k, for 1 ≤ n, recorded by the tangent spaces of its leaves: a C^n involutive distribution of rank k.

• one_le : 1 ≤ n

  The foliation is at least C¹, so that its tangent distribution is locally spanned by differentiable vector fields and involutivity is a condition on it.

• distribution (x : M) : Submodule 𝕜 (TangentSpace I x)

  The tangent distribution of the foliation: at each point, the tangent space of the leaf through it.

• isContMDiffDistribution : let x := ⋯; IsContMDiffDistribution I n k self.distribution

  The tangent distribution is a C^n distribution of rank k.

• isInvolutiveDistribution : let x := ⋯; IsInvolutiveDistribution I self.distribution

  The tangent distribution is involutive.

theorem TauCeti.Foliation.ext {𝕜 : Type u_1} {inst✝ : NontriviallyNormedField 𝕜} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : ChartedSpace H M} {k : ℕ} {inst✝⁶ : IsManifold I (n + 1) M} {x y : Foliation I n M k} (distribution : x.distribution = y.distribution) : x = y

theorem TauCeti.Foliation.ext_iff {𝕜 : Type u_1} {inst✝ : NontriviallyNormedField 𝕜} {E : Type u_2} {inst✝¹ : NormedAddCommGroup E} {inst✝² : NormedSpace 𝕜 E} {H : Type u_3} {inst✝³ : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} {inst✝⁴ : TopologicalSpace M} {inst✝⁵ : ChartedSpace H M} {k : ℕ} {inst✝⁶ : IsManifold I (n + 1) M} {x y : Foliation I n M k} : x = y ↔ x.distribution = y.distribution

theorem TauCeti.Foliation.finrank_distribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {k : ℕ} [IsManifold I (n + 1) M] (F : Foliation I n M k) (x : M) : Module.finrank 𝕜 ↥(F.distribution x) = k

The leaves of a foliation of rank k have k-dimensional tangent spaces.

def TauCeti.Foliation.ofSubmodule {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (S : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥S] (hn : 1 ≤ n) : Foliation (modelWithCornersSelf 𝕜 E) n E (Module.finrank 𝕜 ↥S)

The C^n foliation, for 1 ≤ n, of a normed space E whose leaves are the translates x + S of a finite-dimensional subspace S: its tangent space at every point is S.

@[simp]

theorem TauCeti.Foliation.ofSubmodule_distribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : WithTop ℕ∞} [CompleteSpace 𝕜] (S : Submodule 𝕜 E) [FiniteDimensional 𝕜 ↥S] (hn : 1 ≤ n) (x : E) : (ofSubmodule S hn).distribution x = S