Distributions as vector bundles

A distribution D on a manifold M assigns to every point x a subspace D x of the tangent space. Its total space, the pairs (x, v) with v ∈ D x, carries the topology of a subspace of the tangent bundle (TauCeti.instTopologicalSpaceTotalSpaceDistribution). This file shows that over ℝ or ℂ a continuous distribution of rank k (a C^n distribution of rank k, for any n), with this topology, is a topological vector bundle with model fibre Fin k → 𝕜: a subbundle of the tangent bundle. Constructions on real vector bundles, such as the Euler class TauCeti.eulerClass, can then be applied to the tangent field of a foliation.

The local trivializations come from local frames. A C^n local frame of D is a local frame of D, as a family of subspaces of the tangent bundle, whose members are C^n sections (TauCeti.IsDistributionFrameOn.isSubbundleFrameOn). So D has C^n local frames near every point (TauCeti.IsContMDiffDistribution.hasLocalContMDiffSubbundleFrames), and the general local frame criterion for subbundles (TauCeti.HasLocalContMDiffSubbundleFrames.fiberBundle) applies. The atlas consists of the trivializations of the C^n local frames.

The argument for continuity of the coordinates in a frame, with the derivative of operator inversion in place of its continuity, shows that the coordinates of a tangent vector field differentiable at a point are differentiable there (TauCeti.IsDistributionFrameOn.exists_mdifferentiableAt_coeff).

For a continuous distribution hD : IsContMDiffDistribution I n k D, install hD.fiberBundle with letI; hD.vectorBundle then shows that it is a vector bundle.

On a C^(n+1) manifold, the tangent bundle is a C^n vector bundle and the C^n local frames of D are C^n sections of it, so the smooth local frame criterion (TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle) applies. Hence a C^n distribution of rank k is a C^n vector bundle with model fibre Fin k → 𝕜 (hD.contMDiffVectorBundle), a C^n subbundle of the tangent bundle.

Main definitions

• TauCeti.instTopologicalSpaceTotalSpaceDistribution: the subspace topology on the total space of a distribution.
• TauCeti.IsContMDiffDistribution.fiberBundle: a continuous distribution of rank k is a fibre bundle with fibre Fin k → 𝕜.

Main results

• TauCeti.IsContMDiffDistribution.hasLocalContMDiffSubbundleFrames: a C^n distribution of rank k has C^n local frames of size k near every point.
• TauCeti.IsContMDiffDistribution.mem_trivializationAtlas_fiberBundle_iff: the trivializations of this fibre bundle are those of the C^n local frames of D.
• TauCeti.IsContMDiffDistribution.vectorBundle: a continuous distribution of rank k is a topological vector bundle.
• TauCeti.IsContMDiffDistribution.contMDiffVectorBundle: on a C^(n+1) manifold, a C^n distribution of rank k is a C^n vector bundle.
• TauCeti.IsDistributionFrameOn.exists_mdifferentiableAt_coeff: a vector field tangent to D and differentiable at x is, near x, a combination of a C¹ local frame with coefficients differentiable at x.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 10 (the local frame criterion for smooth subbundles, Lemma 10.32, and its continuous counterpart) and Chapter 19 (distributions).

@[instance_reducible]

noncomputable instance TauCeti.instTopologicalSpaceTotalSpaceDistribution {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {F : Type u_5} (D : (x : M) → Submodule 𝕜 (TangentSpace I x)) : TopologicalSpace (Bundle.TotalSpace F fun (x : M) => ↥(D x))

The total space of a distribution D, the pairs (x, v) with v ∈ D x, carries the topology of a subspace of the tangent bundle (TauCeti.subbundleTopology). The model-fibre parameter F of Bundle.TotalSpace plays no role.

theorem TauCeti.IsDistributionFrameOn.exists_mdifferentiableAt_coeff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {ι : Type u_5} [Fintype ι] [IsManifold I 2 M] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {X : ι → (x : M) → TangentSpace I x} {U : Set M} [IsRCLikeNormedField 𝕜] (hX : IsDistributionFrameOn I n D X U) (hn : 1 ≤ n) {x : M} (hU : U ∈ nhds x) {V : (y : M) → TangentSpace I y} (hV : (MDiffAt fun (y : M) => ⟨y, V y⟩) x) (hVD : ∀ᶠ (y : M) in nhds x, V y ∈ D y) : ∃ (c : ι → M → 𝕜), (∀ (i : ι), MDiffAt (c i) x) ∧ ∀ᶠ (y : M) in nhds x, V y = ∑ i : ι, c i y • X i y

Coefficients in a frame are differentiable. Let X be a C^n local frame of D, with 1 ≤ n, on a neighbourhood of x, and let V be a vector field, differentiable at x, which is tangent to D near x. Then near x the field V is a combination ∑ i, c i • X i of the frame whose coefficients c i are differentiable at x.

theorem TauCeti.IsContMDiffDistribution.hasLocalContMDiffSubbundleFrames {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) : HasLocalContMDiffSubbundleFrames I n E (Fin k) D

A C^n distribution of rank k has C^n local frames of size k near every point, as a family of subspaces of the tangent bundle.

@[instance_reducible]

noncomputable def TauCeti.IsContMDiffDistribution.fiberBundle {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} [IsRCLikeNormedField 𝕜] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) : FiberBundle (Fin k → 𝕜) fun (x : M) => ↥(D x)

A continuous distribution of rank k is a fibre bundle with fibre Fin k → 𝕜, the topology of its total space being that of a subspace of the tangent bundle. Its trivializations are those of the C^n local frames of D (TauCeti.HasLocalContMDiffSubbundleFrames.fiberBundle). Use this definition as a local instance, which chooses a local frame at every point.

theorem TauCeti.IsContMDiffDistribution.mem_trivializationAtlas_fiberBundle_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} [IsRCLikeNormedField 𝕜] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) (e : Bundle.Trivialization (Fin k → 𝕜) Bundle.TotalSpace.proj) : (e ∈ trivializationAtlas (Fin k → 𝕜) fun (x : M) => ↥(D x)) ↔ ∃ (V : Set M) (hV : IsOpen V) (Y : Fin k → (y : M) → TangentSpace I y) (hY : IsDistributionFrameOn I n D Y V), ⋯.trivialization hV = e

The trivializations of hD.fiberBundle are the trivializations of the C^n local frames of D.

theorem TauCeti.IsContMDiffDistribution.vectorBundle {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} [IsRCLikeNormedField 𝕜] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hD : IsContMDiffDistribution I n k D) : VectorBundle 𝕜 (Fin k → 𝕜) fun (x : M) => ↥(D x)

A continuous distribution of rank k is a vector bundle: with the subspace topology of the tangent bundle, its local frame trivializations are linear, with continuous coordinate changes.

theorem TauCeti.IsContMDiffDistribution.contMDiffVectorBundle {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : Type u_3} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {n : WithTop ℕ∞} {k : ℕ} [IsRCLikeNormedField 𝕜] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} [IsManifold I (n + 1) M] (hD : IsContMDiffDistribution I n k D) : ContMDiffVectorBundle n (Fin k → 𝕜) (fun (x : M) => ↥(D x)) I

A C^n distribution of rank k is a C^n vector bundle. On a C^(n+1) manifold, whose tangent bundle is a C^n vector bundle, the C^n local frames of D are C^n sections of it. So D, with the subspace topology of the tangent bundle and the atlas of hD.fiberBundle, is a C^n subbundle of the tangent bundle (TauCeti.HasLocalContMDiffSubbundleFrames.contMDiffVectorBundle).