Flat charts of an involutive distribution

The local Frobenius theorem on a manifold: an involutive C^m distribution D of rank k on a manifold modelled on a finite-dimensional real space has a flat chart around every interior point, a chart e of the C^m maximal atlas in which D is constant. That is, the differential of I ∘ e carries the fibre of D at every point of the domain onto one fixed k-dimensional subspace W of the model space. The slices of I ∘ e in the direction of W are therefore integral manifolds of D, and these are the plaques from which the leaves of D are built.

The manifold is C^n with m + 1 ≤ n, because reading a vector field in a chart loses one derivative of the chart's regularity. This covers a C¹ distribution on a C² manifold, the lowest regularity at which involutivity constrains the distribution. At a boundary point the statement fails: a chart preserves the boundary, while a distribution may be tangent to the boundary at one boundary point and transverse to it at nearby ones. The model I itself may have a boundary, since only the base point has to be interior, and on a boundaryless manifold BoundarylessManifold.isInteriorPoint supplies this at every point. No Hausdorff or second-countability assumption on the manifold is used.

The proof reads D near x in the chart TauCeti.extChartPartialDiffeomorph, followed by a linear splitting E ≃ W × T with W the fibre of D at x read in that chart. The distribution is transverse to the vertical factor at the base point, so TauCeti.IsDistributionFrameOn.exists_openPartialHomeomorph_map_fderiv_eq_ker_snd applies.

Main results

• TauCeti.IsInvolutiveDistribution.exists_flatChart: the local Frobenius theorem.
• TauCeti.IsInvolutiveDistribution.exists_flatChart_extend: flat extended coordinates with open source and injective differential.
• TauCeti.IsInvolutiveDistribution.exists_flatChart_eventually_sub_mem: a horizontal differentiable map stays locally in a single affine slice of a Frobenius chart.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Theorem 19.12 and Proposition 19.16 (local containment in a slice).
• S. Lang, Fundamentals of Differential Geometry, Springer GTM 191 (1999), Chapter VI, §1.

theorem TauCeti.IsInvolutiveDistribution.exists_flatChart {E : Type u} {H : Type u_1} {M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I 1 M] {m : ℕ∞} (hm : 1 ≤ m) {n : WithTop ℕ∞} (hmn : ↑m + 1 ≤ n) [IsManifold I n M] {k : ℕ} {D : (x : M) → Submodule ℝ (TangentSpace I x)} (hinv : IsInvolutiveDistribution I D) (hD : IsContMDiffDistribution I (↑m) k D) {x : M} (hx : I.IsInteriorPoint x) : ∃ (e : OpenPartialHomeomorph M H) (W : Submodule ℝ E), e ∈ IsManifold.maximalAtlas I (↑m) M ∧ x ∈ e.source ∧ Module.finrank ℝ ↥W = k ∧ ∀ y ∈ e.source, Submodule.map (↑(mfderiv% (↑I ∘ ↑e) y)) (D y) = W

The local Frobenius theorem. An involutive C^m distribution D of rank k, for 1 ≤ m, on a C^n manifold with m + 1 ≤ n, modelled on a finite-dimensional real space, is constant in a suitable chart around any interior point x: there are a chart e of the C^m maximal atlas whose domain contains x and a k-dimensional subspace W of the model space such that the differential of I ∘ e carries D y onto W at every point y of the domain of e. On a boundaryless manifold BoundarylessManifold.isInteriorPoint gives the interior hypothesis at every point.

theorem TauCeti.IsInvolutiveDistribution.exists_flatChart_extend {E : Type u} {H : Type u_1} {M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I 1 M] {m : ℕ∞} (hm : 1 ≤ m) {n : WithTop ℕ∞} (hmn : ↑m + 1 ≤ n) [IsManifold I n M] {k : ℕ} {D : (x : M) → Submodule ℝ (TangentSpace I x)} (hinv : IsInvolutiveDistribution I D) (hD : IsContMDiffDistribution I (↑m) k D) {x : M} (hx : I.IsInteriorPoint x) : ∃ (Φ : PartialEquiv M E) (W : Submodule ℝ E), IsOpen Φ.source ∧ x ∈ Φ.source ∧ Module.finrank ℝ ↥W = k ∧ ContMDiffOn I (modelWithCornersSelf ℝ E) (↑m) (↑Φ) Φ.source ∧ (∀ z ∈ Φ.source, Submodule.map (↑(mfderiv% ↑Φ z)) (D z) = W) ∧ ∀ z ∈ Φ.source, Function.Injective ⇑(mfderiv% ↑Φ z)

An involutive C^m distribution admits extended flat coordinates near each interior point, for 1 ≤ m and ambient regularity n ≥ m + 1. The coordinate source is open, its differential is injective there, and it carries the distribution onto a fixed rank-k subspace.

theorem TauCeti.IsInvolutiveDistribution.exists_flatChart_eventually_sub_mem {E : Type u} {H : Type u_1} {M : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_5} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {D : (z : M) → Submodule ℝ (TangentSpace I z)} {f : N → M} [FiniteDimensional ℝ E] [IsManifold I 1 M] {m : ℕ∞} (hm : 1 ≤ m) {n : WithTop ℕ∞} (hmn : ↑m + 1 ≤ n) [IsManifold I n M] (hinv : IsInvolutiveDistribution I D) {k : ℕ} (hD : IsContMDiffDistribution I (↑m) k D) (hf : IsHorizontalMap J D f) {s : Set N} (hfd : MDiff[s] f) (hs : IsOpen s) {x : N} (hxs : x ∈ s) (hx : I.IsInteriorPoint (f x)) : ∃ (e : OpenPartialHomeomorph M H) (W : Submodule ℝ E), e ∈ IsManifold.maximalAtlas I (↑m) M ∧ f x ∈ e.source ∧ Module.finrank ℝ ↥W = k ∧ (∀ z ∈ e.source, Submodule.map (↑(mfderiv% (↑I ∘ ↑e) z)) (D z) = W) ∧ ∀ᶠ (y : N) in nhds x, f y ∈ e.source ∧ (↑I ∘ ↑e) (f y) - (↑I ∘ ↑e) (f x) ∈ W

A Frobenius chart near an interior image point of a horizontal differentiable map puts that map locally in the affine slice parallel to the flattened distribution.