Maps tangent to a distribution

A map f : N → M is horizontal for a distribution D on M, or tangent to D, when every tangent image df_y(T_y N) lies in D (f y) (TauCeti.IsHorizontalMap). Integral manifolds (TauCeti.IsIntegralManifold) are the immersions whose tangent images are all of D; horizontal maps only ask for containment, so they include horizontal curves of sub-Riemannian geometry and, for a contact structure, the isotropic maps. The source is an arbitrary charted space and f need not be injective. The differential is mfderiv, which is 0 where f is not differentiable, so the predicate is meaningful for differentiable maps.

Main declarations

• TauCeti.IsHorizontalMap: maps whose tangent images lie in a distribution.
• TauCeti.IsHorizontalMap.comp: precomposing a horizontal map keeps it horizontal.
• TauCeti.IsHorizontalMap.eventually_sub_mem: coordinates whose differential takes the distribution into a closed subspace are locally constant modulo that subspace along horizontal differentiable maps.
• TauCeti.isHorizontalMap_comp_diffeomorph_iff, TauCeti.isHorizontalMap_diffeomorph_comp_iff: independence of the parametrization and transport by diffeomorphisms preserving the distributions.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Proposition 19.16, p. 500 (local containment in a slice).

def TauCeti.IsHorizontalMap {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] (J : ModelWithCorners 𝕜 E' H') [TopologicalSpace N] [ChartedSpace H' N] (D : (x : M) → Submodule 𝕜 (TangentSpace I x)) (f : N → M) : Prop

A map f : N → M is horizontal for a distribution D, or tangent to D, when every tangent image df_y(T_y N) lies in D (f y). For a contact structure D these are the isotropic maps; when f is moreover a smooth immersion, it parametrizes an immersed isotropic submanifold.

The tangent image is taken with mfderiv, which is 0 at points where f is not differentiable, so there the condition holds trivially.

theorem TauCeti.isHorizontalMap_iff_range_mfderiv_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} : IsHorizontalMap J D f ↔ ∀ (y : N), (↑(mfderiv% f y)).range ≤ D (f y)

A map is horizontal exactly when every tangent image lies in the distribution.

theorem TauCeti.IsHorizontalMap.range_mfderiv_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} (hf : IsHorizontalMap J D f) (y : N) : (↑(mfderiv% f y)).range ≤ D (f y)

The tangent images of a horizontal map lie in the distribution.

theorem TauCeti.isHorizontalMap_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} : IsHorizontalMap J D f ↔ ∀ (y : N) (v : TangentSpace J y), (mfderiv% f y) v ∈ D (f y)

A map is horizontal exactly when its differential sends every tangent vector into the distribution.

theorem TauCeti.IsHorizontalMap.mfderiv_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} (hf : IsHorizontalMap J D f) (y : N) (v : TangentSpace J y) : (mfderiv% f y) v ∈ D (f y)

The differential of a horizontal map takes values in the distribution.

theorem TauCeti.IsHorizontalMap.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} {D' : (x : M) → Submodule 𝕜 (TangentSpace I x)} (hf : IsHorizontalMap J D f) (hDD' : ∀ (x : M), D x ≤ D' x) : IsHorizontalMap J D' f

A map horizontal for a smaller distribution is horizontal for a larger one.

theorem TauCeti.IsHorizontalMap.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} {E'' : Type u_8} {H'' : Type u_9} {P : Type u_10} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E'' H''} [TopologicalSpace P] [ChartedSpace H'' P] {g : P → N} (hf : IsHorizontalMap J D f) (hg : ∀ (x : P), MDiffAt g x) (hfg : ∀ (x : P), MDiffAt f (g x)) : IsHorizontalMap K D (f ∘ g)

Precomposing a horizontal map with a map g keeps it horizontal, wherever g and f are differentiable, since the tangent image of f ∘ g lies in that of f.

theorem TauCeti.isHorizontalMap_comp_diffeomorph_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} {E'' : Type u_8} {H'' : Type u_9} {P : Type u_10} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E'' H''} [TopologicalSpace P] [ChartedSpace H'' P] {n : WithTop ℕ∞} (φ : Diffeomorph K J P N n) (hn : n ≠ 0) : IsHorizontalMap K D (f ∘ ⇑φ) ↔ IsHorizontalMap J D f

Independence of the parametrization. Precomposing with a diffeomorphism of the source does not change whether a map is horizontal.

theorem TauCeti.isHorizontalMap_diffeomorph_comp_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_5} {H' : Type u_6} {N : Type u_7} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [TopologicalSpace H'] {J : ModelWithCorners 𝕜 E' H'} [TopologicalSpace N] [ChartedSpace H' N] {D : (x : M) → Submodule 𝕜 (TangentSpace I x)} {f : N → M} {E'' : Type u_8} {H'' : Type u_9} {P : Type u_10} [NormedAddCommGroup E''] [NormedSpace 𝕜 E''] [TopologicalSpace H''] {K : ModelWithCorners 𝕜 E'' H''} [TopologicalSpace P] [ChartedSpace H'' P] {n : WithTop ℕ∞} {D' : (z : P) → Submodule 𝕜 (TangentSpace K z)} (ψ : Diffeomorph I K M P n) (hn : n ≠ 0) (hψ : ∀ (x : M) (v : TangentSpace I x), v ∈ D x ↔ (mfderiv% ⇑ψ x) v ∈ D' (ψ x)) : IsHorizontalMap J D' (⇑ψ ∘ f) ↔ IsHorizontalMap J D f

Transport by diffeomorphisms. If the differential of a diffeomorphism ψ : M → P carries the distribution D onto the distribution D', then ψ ∘ f is horizontal for D' exactly when f is horizontal for D.

theorem TauCeti.IsHorizontalMap.eventually_sub_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {H' : Type u_5} [TopologicalSpace H'] {J : ModelWithCorners ℝ F H'} {N : Type u_6} [TopologicalSpace N] [ChartedSpace H' N] [IsManifold J 1 N] {D : (z : M) → Submodule ℝ (TangentSpace I z)} {f : N → M} {V : Type u_7} [NormedAddCommGroup V] [NormedSpace ℝ V] (hf : IsHorizontalMap J D f) {s : Set N} (hfd : MDiff[s] f) (hs : IsOpen s) {p : M → V} {U : Set M} (hp : MDiff[U] p) (hU : IsOpen U) {W : Submodule ℝ V} (hW : IsClosed ↑W) (hDp : ∀ z ∈ U, Submodule.map (↑(d% p z)) (D z) ≤ W) {x : N} (hxs : x ∈ s) (hx : f x ∈ U) : ∀ᶠ (y : N) in nhds x, p (f y) - p (f x) ∈ W

Along a horizontal differentiable map, coordinates are locally constant modulo any closed subspace containing the coordinate image of the distribution.