Vector fields in manifolds

We study functions of the form V : Π (x : M) → TangentSpace I x on a manifold, i.e., vector fields.

We define the pullback of a vector field under a map, as VectorField.mpullback I I' f V x := (mfderiv I I' f x).inverse (V (f x)) (together with the same notion within a set). Note that the pullback uses the junk-value pattern: if the derivative of the map is not invertible, then pullback is given the junk value zero.

We start developing API around this notion.

All these are given in the VectorField namespace because pullbacks, Lie brackets, and so on, are notions that make sense in a variety of contexts. We also prefix the notions with m to distinguish the manifold notions from the vector space notions.

For notions that come naturally in other namespaces for dot notation, we specify vectorField in the name to lift ambiguities. For instance, the fact that the Lie bracket of two smooth vector fields is smooth will be ContMDiffAt.mlieBracket_vectorField.

Note that a smoothness assumption for a vector field is written by seeing the vector field as a function from M to its tangent bundle through a coercion, as in: MDifferentiableWithinAt I I.tangent (fun y ↦ (V y : TangentBundle I M)) s x.

instance instIsManifoldOfNatWithTopENatOfMinSmoothness {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {n : ℕ} [n.AtLeastTwo] [IsManifold I (minSmoothness 𝕜 (OfNat.ofNat n)) M] : IsManifold I (OfNat.ofNat n) M

instance instIsManifoldOfNatWithTopENatOfMinSmoothness_1 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 1) M] : IsManifold I 1 M

instance instIsManifoldMinSmoothnessOfNatWithTopENat {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 3) M] : IsManifold I (minSmoothness 𝕜 2) M

instance instIsManifoldMinSmoothnessOfNatWithTopENat_1 {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (minSmoothness 𝕜 2) M] : IsManifold I (minSmoothness 𝕜 1) M

Pullback of vector fields in manifolds

def VectorField.mpullbackWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') (V : (x : M') → TangentSpace I' x) (s : Set M) (x : M) : TangentSpace I x

The pullback of a vector field under a map between manifolds, within a set s. If the derivative of the map within s is not invertible, then pullback is given the junk value zero.

Equations

• VectorField.mpullbackWithin I I' f V s x = (mfderivWithin I I' f s x).inverse (V (f x))

def VectorField.mpullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] (I' : ModelWithCorners 𝕜 E' H') {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] (f : M → M') (V : (x : M') → TangentSpace I' x) (x : M) : TangentSpace I x

The pullback of a vector field under a map between manifolds. If the derivative of the map is not invertible, then pullback is given the junk value zero.

Equations

• VectorField.mpullback I I' f V x = (mfderiv I I' f x).inverse (V (f x))

theorem VectorField.mpullbackWithin_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M} {V : (x : M') → TangentSpace I' x} : mpullbackWithin I I' f V s x = (mfderivWithin I I' f s x).inverse (V (f x))

theorem VectorField.mpullbackWithin_smul_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M} {V : (x : M') → TangentSpace I' x} {c : 𝕜} : mpullbackWithin I I' f (c • V) s x = c • mpullbackWithin I I' f V s x

theorem VectorField.mpullbackWithin_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {V : (x : M') → TangentSpace I' x} {c : 𝕜} : mpullbackWithin I I' f (c • V) s = c • mpullbackWithin I I' f V s

theorem VectorField.mpullbackWithin_add_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M} {V V₁ : (x : M') → TangentSpace I' x} : mpullbackWithin I I' f (V + V₁) s x = mpullbackWithin I I' f V s x + mpullbackWithin I I' f V₁ s x

theorem VectorField.mpullbackWithin_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {V V₁ : (x : M') → TangentSpace I' x} : mpullbackWithin I I' f (V + V₁) s = mpullbackWithin I I' f V s + mpullbackWithin I I' f V₁ s

theorem VectorField.mpullbackWithin_neg_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M} {V : (x : M') → TangentSpace I' x} : mpullbackWithin I I' f (-V) s x = -mpullbackWithin I I' f V s x

theorem VectorField.mpullbackWithin_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {V : (x : M') → TangentSpace I' x} : mpullbackWithin I I' f (-V) s = -mpullbackWithin I I' f V s

theorem VectorField.mpullbackWithin_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {s : Set M} {x : M} {V : (x : M) → TangentSpace I x} (h : UniqueMDiffWithinAt I s x) : mpullbackWithin I I id V s x = V x

theorem VectorField.mpullback_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} {V : (x : M') → TangentSpace I' x} : mpullback I I' f V x = (mfderiv I I' f x).inverse (V (f x))

theorem VectorField.mpullback_smul_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} {V : (x : M') → TangentSpace I' x} {c : 𝕜} : mpullback I I' f (c • V) x = c • mpullback I I' f V x

theorem VectorField.mpullback_smul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M') → TangentSpace I' x} {c : 𝕜} : mpullback I I' f (c • V) = c • mpullback I I' f V

theorem VectorField.mpullback_add_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} {V V₁ : (x : M') → TangentSpace I' x} : mpullback I I' f (V + V₁) x = mpullback I I' f V x + mpullback I I' f V₁ x

theorem VectorField.mpullback_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V V₁ : (x : M') → TangentSpace I' x} : mpullback I I' f (V + V₁) = mpullback I I' f V + mpullback I I' f V₁

theorem VectorField.mpullback_neg_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x : M} {V : (x : M') → TangentSpace I' x} : mpullback I I' f (-V) x = -mpullback I I' f V x

theorem VectorField.mpullback_neg {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M') → TangentSpace I' x} : mpullback I I' f (-V) = -mpullback I I' f V

@[simp]

theorem VectorField.mpullbackWithin_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M') → TangentSpace I' x} : mpullbackWithin I I' f V Set.univ = mpullback I I' f V

theorem VectorField.mpullbackWithin_eq_pullbackWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {f : E → E'} {V : E' → E'} {s : Set E} : mpullbackWithin (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V s = pullbackWithin 𝕜 f V s

theorem VectorField.mpullback_eq_pullback {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {f : E → E'} {V : E' → E'} : mpullback (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') f V = pullback 𝕜 f V

@[simp]

theorem VectorField.mpullback_id {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {V : (x : M) → TangentSpace I x} : mpullback I I id V = V

Regularity of pullback of vector fields

In this paragraph, we assume that the model space is complete, to ensure that the set of invertible linear maps is open and that inversion is a smooth map there. Otherwise, the pullback of vector fields could behave wildly, even at points where the derivative of the map is invertible.

theorem MDifferentiableWithinAt.mpullbackWithin_vectorField_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t (f x₀)) (hf : ContMDiffWithinAt I I' n f s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible) (hx₀ : x₀ ∈ s) (hs : UniqueMDiffOn I s) (hmn : 2 ≤ n) : MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) (s ∩ f ⁻¹' t) x₀

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable. Version within a set at a point.

theorem MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t y₀) (hf : ContMDiffWithinAt I I' n f s x₀) (hf' : (mfderivWithin I I' f s x₀).IsInvertible) (hx₀ : x₀ ∈ s) (hs : UniqueMDiffOn I s) (hmn : 2 ≤ n) (h : y₀ = f x₀) : MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) (s ∩ f ⁻¹' t) x₀

theorem MDifferentiableOn.mpullbackWithin_vectorField_inter {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {s : Set M} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableOn I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t) (hf : ContMDiffOn I I' n f s) (hf' : ∀ x ∈ s ∩ f ⁻¹' t, (mfderivWithin I I' f s x).IsInvertible) (hs : UniqueMDiffOn I s) (hmn : 2 ≤ n) : MDifferentiableOn I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullbackWithin I I' f V s y }) (s ∩ f ⁻¹' t)

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable. Version on a set.

theorem MDifferentiableWithinAt.mpullback_vectorField_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x₀ : M} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t (f x₀)) (hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : 2 ≤ n) : MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t) x₀

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable. Version within a set at a point, but with full pullback.

theorem MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x₀ : M} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t y₀) (hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : 2 ≤ n) (hy₀ : y₀ = f x₀) : MDifferentiableWithinAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t) x₀

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable. Version within a set at a point, but with full pullback.

theorem MDifferentiableOn.mpullback_vectorField_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableOn I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) t) (hf : ContMDiff I I' n f) (hf' : ∀ x ∈ f ⁻¹' t, (mfderiv I I' f x).IsInvertible) (hmn : 2 ≤ n) : MDifferentiableOn I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) (f ⁻¹' t)

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable. Version on a set, but with full pullback

theorem MDifferentiableAt.mpullback_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {x₀ : M} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiableAt I' I'.tangent (fun (y : M') => { proj := y, snd := V y }) (f x₀)) (hf : ContMDiffAt I I' n f x₀) (hf' : (mfderiv I I' f x₀).IsInvertible) (hmn : 2 ≤ n) : MDifferentiableAt I I.tangent (fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }) x₀

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable. Version at a point.

theorem MDifferentiable.mpullback_vectorField {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {H : Type u_2} [TopologicalSpace H] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4} [TopologicalSpace M] [ChartedSpace H M] {H' : Type u_5} [TopologicalSpace H'] {E' : Type u_6} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7} [TopologicalSpace M'] [ChartedSpace H' M'] {f : M → M'} {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} [IsManifold I 2 M] [IsManifold I' 2 M'] [CompleteSpace E] (hV : MDifferentiable I' I'.tangent fun (y : M') => { proj := y, snd := V y }) (hf : ContMDiff I I' n f) (hf' : ∀ (x : M), (mfderiv I I' f x).IsInvertible) (hmn : 2 ≤ n) : MDifferentiable I I.tangent fun (y : M) => { proj := y, snd := VectorField.mpullback I I' f V y }

The pullback of a differentiable vector field by a C^n function with 2 ≤ n is differentiable.