Distributions transverse to the vertical subspace

Let D be a C^n distribution on E × F whose rank is finrank 𝕜 E, and suppose that at a point p₀ the subspace D p₀ contains no nonzero vertical vector, that is, meets the kernel 0 × F of the first projection only in 0. Then near p₀ the distribution is the graph distribution TauCeti.graphDistribution f of a C^n family f : E × F → (E →L[𝕜] F) (TauCeti.IsContMDiffDistribution.exists_eventually_eq_graphDistribution). This is the local normal form in which the Frobenius theorem is proved: in the graph form, involutivity of D is the Frobenius integrability condition on f, and the graphs of solutions of the total differential equation D u x = f (x, u x) are integral manifolds.

The family f is written down from a local frame X₁, …, Xₖ of D near p₀. Let Φ p be the linear map c ↦ ∑ᵢ cᵢ • Xᵢ p from 𝕜ᵏ to E × F, which is injective with range D p. Its first component A p is injective at p₀, since D p₀ has no vertical vector, hence invertible because k = finrank 𝕜 E; invertibility persists near p₀, and there D p is the graph of f p = (snd ∘ Φ p) ∘ (A p)⁻¹. Smoothness of f is smoothness of inversion of continuous linear equivalences (contDiffAt_map_inverse).

Combined with the Frobenius theorem in coordinates (TauCeti.exists_eventually_hasFDerivAt_of_isFrobeniusIntegrableAt), this gives the Frobenius theorem for a distribution transverse to the vertical subspace at one point (TauCeti.IsInvolutiveDistribution.exists_eventually_eq_graph_fderiv): over finite-dimensional real spaces, a C^(n+1) involutive distribution of rank finrank ℝ E with D (x₀, y₀) transverse to 0 × F has an integral manifold through (x₀, y₀), the graph of a function u : E → F whose graph has tangent space D (x, u x) at every point (x, u x) near (x₀, y₀).

Main results

• TauCeti.IsContMDiffDistribution.exists_eventually_eq_graphDistribution: a C^n distribution of rank finrank 𝕜 E on E × F, transverse to 0 × F at p₀, is the graph distribution of a family f near p₀, and f is C^n near p₀.
• TauCeti.IsInvolutiveDistribution.exists_eventually_eq_graph_fderiv: the Frobenius theorem for transverse distributions. A C^(n+1) involutive distribution of rank finrank ℝ E on E × F, transverse to 0 × F at (x₀, y₀), is tangent to the graph of a function u with u x₀ = y₀, C^(n+1) at x₀: D (x, u x) is the graph of fderiv ℝ u x for x near x₀.
• TauCeti.IsDistributionFrameOn.exists_openPartialHomeomorph_map_fderiv_eq_ker_snd: the local Frobenius theorem in product coordinates. A C^(n+1) change of coordinates carries D onto the horizontal subspace at each point of its domain.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 19, proof of Theorem 19.12.
• S. Lang, Fundamentals of Differential Geometry, Springer GTM 191 (1999), Chapter VI, §1.

theorem TauCeti.IsDistributionFrameOn.exists_eventually_eq_graphDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {D : E × F → Submodule 𝕜 (E × F)} {U : Set (E × F)} (hU : IsOpen U) {X : Fin (Module.finrank 𝕜 E) → (p : E × F) → TangentSpace (modelWithCornersSelf 𝕜 (E × F)) p} (hX : IsDistributionFrameOn (modelWithCornersSelf 𝕜 (E × F)) n D X U) {p₀ : E × F} (hp₀U : p₀ ∈ U) (hp₀ : Disjoint (D p₀) (LinearMap.fst 𝕜 E F).ker) : ∃ (f : E × F → E →L[𝕜] F), ∀ᶠ (p : E × F) in nhds p₀, ContDiffAt 𝕜 n f p ∧ D p = graphDistribution f p

A transverse distribution with a local frame is locally a graph distribution. Let D be a family of subspaces of E × F with a C^n local frame of finrank 𝕜 E vector fields on an open neighbourhood U of p₀, such that D p₀ meets the vertical subspace 0 × F, the kernel of the first projection, only in 0. Then near p₀ the distribution is the graph distribution of a family f : E × F → (E →L[𝕜] F) that is C^n near p₀.

theorem TauCeti.IsContMDiffDistribution.exists_eventually_eq_graphDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [CompleteSpace 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {D : E × F → Submodule 𝕜 (E × F)} (hD : IsContMDiffDistribution (modelWithCornersSelf 𝕜 (E × F)) n (Module.finrank 𝕜 E) D) {p₀ : E × F} (hp₀ : Disjoint (D p₀) (LinearMap.fst 𝕜 E F).ker) : ∃ (f : E × F → E →L[𝕜] F), ∀ᶠ (p : E × F) in nhds p₀, ContDiffAt 𝕜 n f p ∧ D p = graphDistribution f p

A transverse distribution is locally a graph distribution. Let D be a C^n distribution on E × F of rank finrank 𝕜 E such that D p₀ meets the vertical subspace 0 × F, the kernel of the first projection, only in 0. Then near p₀ the distribution is the graph distribution of a family f : E × F → (E →L[𝕜] F) that is C^n near p₀.

theorem TauCeti.IsInvolutiveDistribution.exists_eventually_eq_graph_fderiv {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ∞} {D : E × F → Submodule ℝ (E × F)} (hinv : IsInvolutiveDistribution (modelWithCornersSelf ℝ (E × F)) D) (hD : IsContMDiffDistribution (modelWithCornersSelf ℝ (E × F)) (↑n + 1) (Module.finrank ℝ E) D) {x₀ : E} {y₀ : F} (h₀ : Disjoint (D (x₀, y₀)) (LinearMap.fst ℝ E F).ker) : ∃ (u : E → F), u x₀ = y₀ ∧ ContDiffAt ℝ (↑n + 1) u x₀ ∧ ∀ᶠ (x : E) in nhds x₀, DifferentiableAt ℝ u x ∧ D (x, u x) = (↑(fderiv ℝ u x)).graph

The Frobenius theorem for transverse distributions. Let D be an involutive C^(n+1) distribution of rank finrank ℝ E on E × F such that D (x₀, y₀) meets the vertical subspace 0 × F only in 0. Then D has an integral manifold through (x₀, y₀): the graph of a function u, of class C^(n+1) at x₀, with u x₀ = y₀, whose tangent space at (x, u x), the graph of fderiv ℝ u x, is D (x, u x) for every x near x₀.

theorem TauCeti.IsDistributionFrameOn.exists_openPartialHomeomorph_map_fderiv_eq_ker_snd {E F : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ∞} {D : E × F → Submodule ℝ (E × F)} {U : Set (E × F)} (hU : IsOpen U) {X : Fin (Module.finrank ℝ E) → (p : E × F) → TangentSpace (modelWithCornersSelf ℝ (E × F)) p} (hX : IsDistributionFrameOn (modelWithCornersSelf ℝ (E × F)) (↑n + 1) D X U) (hinv : IsInvolutiveDistributionOn (modelWithCornersSelf ℝ (E × F)) D U) {p₀ : E × F} (hp₀U : p₀ ∈ U) (hp₀ : Disjoint (D p₀) (LinearMap.fst ℝ E F).ker) : ∃ (φ : OpenPartialHomeomorph (E × F) (E × F)), p₀ ∈ φ.source ∧ ↑φ p₀ = p₀ ∧ ContDiffOn ℝ (↑n + 1) (↑φ) φ.source ∧ ContDiffOn ℝ (↑n + 1) (↑φ.symm) φ.target ∧ ∀ p ∈ φ.source, Submodule.map (↑(fderiv ℝ (↑φ) p)) (D p) = (LinearMap.snd ℝ E F).ker

The local Frobenius theorem in product coordinates. Let D be a family of subspaces of E × F with a C^(n+1) local frame of finrank ℝ E vector fields on an open neighbourhood U of p₀, involutive on U, such that D p₀ meets the vertical subspace 0 × F only in 0. Then some C^(n+1) change of coordinates φ, with C^(n+1) inverse and fixing p₀, carries D onto the horizontal subspace E × 0, the kernel of the second projection, at each point of its domain. So φ is a flat chart of D, and the preimages under φ of the horizontal slices are integral manifolds of D.