Integral manifolds of a distribution

An integral manifold of a tangent distribution D is a C^n immersion of a nonempty charted space whose differential has image exactly D at every point. The source has its own topology and charted-space structure: it is not given the subspace topology from the ambient manifold, and the immersion need not be injective. This is the notion needed by the Frobenius theorem and by the construction of immersed Lie subgroups.

This file provides both the unbundled predicate TauCeti.IsIntegralManifold for a specified immersion and TauCeti.IntegralManifold, which packages a k-dimensional source manifold and its parametrization. The rank theorem shows that, for regularity n ≠ 0, the dimension of any finite-dimensional source equals the rank of the distribution at any image point; it is not extra data hidden in the definition. For regularity at least one, integral immersions of a finite-dimensional constant distribution have partial-diffeomorphism charts into its direction subspace near interior source points. These charts give local changes of parameter between interior source points with the same ambient image, intertwining the two integral immersions.

Main definitions

• TauCeti.IsIntegralManifold: an immersion of a nonempty charted space whose tangent image equals the given distribution.
• TauCeti.IntegralManifold: a packaged integral manifold with Euclidean model of dimension k.

Main results

• TauCeti.IsIntegralManifold.finrank_model_eq: for regularity n ≠ 0, the source model dimension equals the rank of the distribution at any image point.
• TauCeti.isIntegralManifold_id: the identity is an integral manifold of the full tangent distribution.
• TauCeti.IsIntegralManifold.eventually_sub_mem: an integral immersion, of regularity at least one, of a finite-dimensional constant distribution locally stays in one affine plaque, including at boundary source points.
• TauCeti.IsIntegralManifold.exists_plaque_chart: a local chart in an affine plaque with the prescribed ambient inclusion.
• TauCeti.IsIntegralManifold.exists_plaque_transition: a local change of integral parameters intertwining their ambient maps.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19, Proposition 19.16 (Local Structure of Integral Manifolds), p. 500.

def TauCeti.IsIntegralManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] (J : ModelWithCorners ℝ E' H') (n : WithTop ℕ∞) {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] (D : (x : M) → Submodule ℝ (TangentSpace I x)) (f : N → M) : Prop

A map is an integral manifold of D when its source is a nonempty charted space, it is a C^n immersion, and the image of its differential at every point is exactly the prescribed tangent subspace.

Nonemptiness rules out the empty map, which would otherwise satisfy the remaining conditions vacuously for every distribution.

The source topology and charted-space structure are independent of the ambient topology. In particular, this predicate neither requires the map to be injective nor equips its range with the subspace topology.

theorem TauCeti.isIntegralManifold_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule ℝ (TangentSpace I x)} {f : N → M} : IsIntegralManifold J n D f ↔ Nonempty N ∧ Manifold.IsImmersion J I n f ∧ ∀ (y : N), (↑(mfderiv% f y)).range = D (f y)

Characterization of an integral manifold as an immersion of a nonempty charted space with the prescribed differential range.

theorem TauCeti.IsIntegralManifold.nonempty {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule ℝ (TangentSpace I x)} {f : N → M} (hf : IsIntegralManifold J n D f) : Nonempty N

The source of an integral manifold is nonempty.

theorem TauCeti.IsIntegralManifold.isImmersion {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule ℝ (TangentSpace I x)} {f : N → M} (hf : IsIntegralManifold J n D f) : Manifold.IsImmersion J I n f

The parametrization of an integral manifold is an immersion.

theorem TauCeti.IsIntegralManifold.range_mfderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule ℝ (TangentSpace I x)} {f : N → M} (hf : IsIntegralManifold J n D f) (y : N) : (↑(mfderiv% f y)).range = D (f y)

The tangent image of an integral manifold is the prescribed distribution fiber.

theorem TauCeti.IsIntegralManifold.contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule ℝ (TangentSpace I x)} {f : N → M} (hf : IsIntegralManifold J n D f) : ContMDiff J I n f

The parametrization of an integral manifold is of class C^n.

theorem TauCeti.IsIntegralManifold.finrank_model_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {k : ℕ} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {N : Type v} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule ℝ (TangentSpace I x)} {f : N → M} (hf : IsIntegralManifold J n D f) (hn : n ≠ 0) (y : N) (hD : Module.finrank ℝ ↥(D (f y)) = k) : Module.finrank ℝ E' = k

For regularity n ≠ 0, the model dimension of an integral manifold f equals the rank of the distribution at the image point f y of any source point y.

theorem TauCeti.isIntegralManifold_id {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M] [Nonempty M] : IsIntegralManifold I n (fun (x : M) => ⊤) id

The identity map of a nonempty manifold is an integral manifold of the full tangent distribution.

structure TauCeti.IntegralManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] (n : WithTop ℕ∞) (D : (x : M) → Submodule ℝ (TangentSpace I x)) (k : ℕ) : Type (max u (v + 1))

A packaged k-dimensional integral manifold of D.

Its carrier is nonempty and has an independent C^n manifold structure modelled on ℝ^k; the map into the ambient manifold is only required to be an immersion. Injectivity, embeddedness, connectedness, and maximality are deliberately separate properties.

• carrier : Type v

  The carrier of the integral manifold.

• topologicalSpace : TopologicalSpace self.carrier

  The topology of the carrier, which need not be the subspace topology from M.

• chartedSpace : ChartedSpace (EuclideanSpace ℝ (Fin k)) self.carrier

  The carrier is charted by the k-dimensional Euclidean model.

• isManifold : IsManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) n self.carrier

  The carrier is a manifold of regularity n.

• nonempty : Nonempty self.carrier

  The carrier is nonempty, so a packaged integral manifold is never vacuous.

• map : self.carrier → M

  The parametrizing immersion into the ambient manifold.

• isImmersion : Manifold.IsImmersion (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) I n self.map

  The parametrization is a C^n immersion.

• range_mfderiv (y : self.carrier) : (↑(mfderiv% self.map y)).range = D (self.map y)

  The image of the differential is exactly the distribution fiber.

theorem TauCeti.IntegralManifold.isIntegralManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule ℝ (TangentSpace I x)} (N : IntegralManifold n D k) : IsIntegralManifold (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) n D N.map

The map of a packaged integral manifold satisfies the unbundled integral-manifold predicate.

theorem TauCeti.IntegralManifold.contMDiff_map {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u} [TopologicalSpace M] [ChartedSpace H M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule ℝ (TangentSpace I x)} (N : IntegralManifold n D k) : ContMDiff (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) I n N.map

The map of a packaged integral manifold is of class C^n.

theorem TauCeti.IsIntegralManifold.eventually_sub_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {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 n N] {W : Submodule ℝ E} [FiniteDimensional ℝ ↥W] {f : N → E} {x : N} (hf : IsIntegralManifold J n (fun (x : E) => W) f) (hn : 1 ≤ n) : ∀ᶠ (z : N) in nhds x, f z - f x ∈ W

An integral immersion, of regularity at least one, of a finite-dimensional constant distribution locally stays in one affine plaque.

theorem TauCeti.IsIntegralManifold.exists_plaque_chart {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {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 n N] {W : Submodule ℝ E} [FiniteDimensional ℝ ↥W] {f : N → E} {x : N} {s : Set N} (hf : IsIntegralManifold J n (fun (x : E) => W) f) (hn : 1 ≤ n) (hx : J.IsInteriorPoint x) (hs : IsOpen s) (hxs : x ∈ s) : ∃ (e : PartialDiffeomorph J (modelWithCornersSelf ℝ ↥W) N (↥W) n), x ∈ e.source ∧ ↑e.toPartialEquiv x = 0 ∧ e.source ⊆ s ∧ ∀ y ∈ e.source, f y = f x + ↑(↑e.toPartialEquiv y)

An integral immersion of a finite-dimensional constant distribution has a partial-diffeomorphism chart into its direction subspace at every interior source point. The chart sends the point to zero and identifies the immersion with translation of the subtype inclusion. Its source lies inside the specified open neighborhood.

theorem TauCeti.IsIntegralManifold.exists_plaque_transition {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : WithTop ℕ∞} {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 n N] {W : Submodule ℝ E} [FiniteDimensional ℝ ↥W] {f : N → E} {x : N} {F' : Type u_6} [NormedAddCommGroup F'] [NormedSpace ℝ F'] {H'' : Type u_7} [TopologicalSpace H''] {K : ModelWithCorners ℝ F' H''} {P : Type u_8} [TopologicalSpace P] [ChartedSpace H'' P] [IsManifold K n P] {g : P → E} {y : P} (hf : IsIntegralManifold J n (fun (x : E) => W) f) (hg : IsIntegralManifold K n (fun (x : E) => W) g) (hn : 1 ≤ n) (hx : J.IsInteriorPoint x) (hy : K.IsInteriorPoint y) (hfg : f x = g y) : ∃ (e : PartialDiffeomorph J K N P n), x ∈ e.source ∧ ↑e.toPartialEquiv x = y ∧ ∀ z ∈ e.source, f z = g (↑e.toPartialEquiv z)

Two integral immersions of the same finite-dimensional constant distribution, through the same ambient point, are related near interior source points by a partial diffeomorphism intertwining their ambient maps.