Vector fields transverse to a map

A vector field Z on a manifold M is transverse along a map ι : S → M (TauCeti.IsTransverseAlong) when at every point s of S the vector Z (ι s) is not tangent to ι: it does not lie in the range of the differential dι_s. When ι is an embedded hypersurface, so that this range has codimension one, this is transversality of Z to the hypersurface in the usual sense: Z (ι s) and the tangent space of the hypersurface at s span the tangent space of M at ι s. A transverse vector field does not vanish along ι (TauCeti.IsTransverseAlong.ne_zero).

For a regular level f⁻¹(c) of a scalar function, with its preferred atlas TauCeti.regularLevelChartedSpace, the tangent space at x is the kernel of df_x (TauCeti.range_mfderiv_coe_regularLevel). So a vector field is transverse along the inclusion of the level exactly when df(Z) ≠ 0 at every point of the level (TauCeti.isTransverseAlong_coe_scalarRegularLevel_iff). This is how transversality to the hypersurfaces of symplectic geometry (energy levels, boundaries of domains, cosphere bundles) is checked in practice.

A vector field crossing a level of f in the direction of increasing f, df(Z) > 0, leaves the sublevel set there: a point where df does not vanish is not a local maximum, by Fermat's theorem, so every point of the level is a limit of points where f is larger (TauCeti.mem_closure_setOf_lt_of_mvfderiv_pos). Hence the frontier of the sublevel set {f ≤ c} is exactly the level f⁻¹(c) when df(Z) > 0 along it (TauCeti.frontier_setOf_le_eq_of_mvfderiv_pos). This identifies the boundary of a domain whose boundary is crossed outwards by a vector field, as for Liouville domains.

Main definitions

• TauCeti.IsTransverseAlong: Z (ι s) is outside the range of dι_s for every s.

Main results

• TauCeti.isTransverseAlong_coe_scalarRegularLevel_iff: transversality along a regular level is the nonvanishing of df(Z) on the level.
• TauCeti.frontier_setOf_le_eq_of_mvfderiv_pos: the frontier of a sublevel set whose level is crossed outwards by a vector field is the level.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 5 (vector fields transverse to a hypersurface).

def TauCeti.IsTransverseAlong {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] (J : ModelWithCorners ℝ E' H') [TopologicalSpace S] [ChartedSpace H' S] (Z : (x : M) → TangentSpace I x) (ι : S → M) : Prop

A vector field Z on M is transverse along a map ι : S → M when at every point s the vector Z (ι s) is not tangent to ι, that is, not in the range of the differential dι_s. For an embedded hypersurface this is transversality of Z to the hypersurface.

theorem TauCeti.isTransverseAlong_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] {Z : (x : M) → TangentSpace I x} {ι : S → M} : IsTransverseAlong J Z ι ↔ ∀ (s : S), Z (ι s) ∉ (↑(mfderiv% ι s)).range

The defining characterization of a vector field transverse along a map.

theorem TauCeti.IsTransverseAlong.ne_zero {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} {H' : Type u_5} {S : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} [TopologicalSpace S] [ChartedSpace H' S] {Z : (x : M) → TangentSpace I x} {ι : S → M} (h : IsTransverseAlong J Z ι) (s : S) : Z (ι s) ≠ 0

A vector field transverse along ι does not vanish at the points of the image of ι.

Vector fields crossing a level outwards

theorem TauCeti.mem_closure_setOf_lt_of_mvfderiv_pos {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] {f : M → ℝ} {x : M} {v : TangentSpace I x} (hpos : 0 < (d% f x) v) : x ∈ closure {y : M | f x < f y}

A direction increasing a function leaves its sublevel set. If a tangent vector v at a point x of a boundaryless manifold satisfies df_x(v) > 0, then x lies in the closure of the set {y | f x < f y}: otherwise x would be a local maximum of f, hence a critical point by Fermat's theorem (IsLocalMax.mem_criticalPoints), and df_x would vanish.

theorem TauCeti.frontier_setOf_le_eq_of_mvfderiv_pos {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [I.Boundaryless] {Z : (x : M) → TangentSpace I x} {f : M → ℝ} {c : ℝ} (hfc : Continuous f) (hpos : ∀ (x : M), f x = c → 0 < (d% f x) (Z x)) : frontier {x : M | f x ≤ c} = {x : M | f x = c}

The frontier of a sublevel set crossed outwards by a vector field. Let f be continuous, and let Z be a vector field with df(Z) > 0 along the level f⁻¹(c). Then the frontier of the sublevel set {f ≤ c} is exactly the level f⁻¹(c).

theorem TauCeti.isTransverseAlong_coe_scalarRegularLevel_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {f : M → ℝ} {c : ℝ} [I.Boundaryless] [FiniteDimensional ℝ E] [IsManifold I 1 M] (hf : ∀ (x : M), f x = c → ContMDiffAt I (modelWithCornersSelf ℝ ℝ) 1 f x) (hreg : IsRegularValue I (modelWithCornersSelf ℝ ℝ) f c) {Z : (x : M) → TangentSpace I x} : IsTransverseAlong (modelWithCornersSelf ℝ (Fin (Module.finrank ℝ E - 1) → ℝ)) Z Subtype.val ↔ ∀ (x : M), f x = c → (mfderiv% f x) (Z x) ≠ 0

Transversality to a regular level. A vector field Z is transverse along the inclusion of a regular level f⁻¹(c), with its preferred atlas TauCeti.regularLevelChartedSpace, exactly when df(Z) ≠ 0 at every point of the level.