English
Let V be a differentiable vector field along a target manifold M', and f: M → M' be a C^n map with n ≥ 2. If V is differentiable along the image of f on a set s, the derivative of f is invertible on s, and the domain s is compatible with a unique differential structure, then the pullback vector field defined by V ∘ f is differentiable of class C^m on the subset s ∩ f⁻¹(t).
Русский
Пусть V — дифференцируемое векторное поле на мантоводстве M', и f: M → M' — C^n отображение с n ≥ 2. Если V дифференцируемо вдоль образа f на множестве s, производная f обратима на s, и задана совместимая дифференцируемая структура, то пуллбэк-веторное поле V ∘ f дифференцируемо класса C^m на подмножестве s ∩ f⁻¹(t).
LaTeX
$$$\text{Let } V: M' \to TM' \text{ be } C^m \text{ along } M',\; f: M \to M' \text{ be } C^n,\; n \ge 2. \text{ If } V \text{ is differentiable along } f \text{ on } s,\; Df|_s \text{ is invertible} \\ \text{then the pullback vector field } V^{\*} \text{ on } M, \\ V^{\*}(x) = (V(f(x)) )^{\#} \text{ is } C^m \text{ on } s \cap f^{-1}(t).$$$
Lean4
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point. -/
protected theorem _root_.MDifferentiableWithinAt.mpullbackWithin_vectorField_inter
(hV : MDifferentiableWithinAt I' I'.tangent (fun (y : M') ↦ (V y : TangentBundle I' M')) 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) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t)
x₀ :=
by
/- We want to apply the theorem `MDifferentiableWithinAt.clm_apply_of_inCoordinates`,
stating that applying linear maps to vector fields gives a smooth result when the linear map and
the vector field are smooth. This theorem is general, we will apply it to
`b₁ = f`, `b₂ = id`, `v = V ∘ f`, `ϕ = fun x ↦ (mfderivWithin I I' f s x).inverse` -/
let b₁ := f
let b₂ : M → M := id
let v : Π (x : M), TangentSpace I' (f x) := V ∘ f
let ϕ : Π (x : M), TangentSpace I' (f x) →L[𝕜] TangentSpace I x := fun x ↦ (mfderivWithin I I' f s x).inverse
have hv : MDifferentiableWithinAt I I'.tangent (fun x ↦ (v x : TangentBundle I' M')) (s ∩ f ⁻¹' t) x₀ :=
by
apply hV.comp x₀ ((hf.mdifferentiableWithinAt (one_le_two.trans hmn)).mono inter_subset_left)
exact MapsTo.mono_left (mapsTo_preimage _ _) inter_subset_right
suffices hϕ :
MDifferentiableWithinAt I 𝓘(𝕜, E' →L[𝕜] E)
(fun (x : M) ↦
ContinuousLinearMap.inCoordinates E' (TangentSpace I' (M := M')) E (TangentSpace I (M := M)) (b₁ x₀) (b₁ x)
(b₂ x₀) (b₂ x) (ϕ x))
s x₀
from MDifferentiableWithinAt.clm_apply_of_inCoordinates (hϕ.mono inter_subset_left) hv mdifferentiableWithinAt_id
have :
MDifferentiableWithinAt I 𝓘(𝕜, E →L[𝕜] E')
(fun (x : M) ↦
ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M')) x₀ x (f x₀) (f x)
(mfderivWithin I I' f s x))
s x₀ :=
((hf.of_le hmn).mfderivWithin_const le_rfl hx₀ hs).mdifferentiableWithinAt le_rfl
have :
MDifferentiableWithinAt I 𝓘(𝕜, E' →L[𝕜] E)
(ContinuousLinearMap.inverse ∘
(fun (x : M) ↦
ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E' (TangentSpace I' (M := M')) x₀ x (f x₀) (f x)
(mfderivWithin I I' f s x)))
s x₀ :=
by
apply MDifferentiableAt.comp_mdifferentiableWithinAt _ _ this
apply ContMDiffAt.mdifferentiableAt _ le_rfl
apply ContDiffAt.contMDiffAt
apply IsInvertible.contDiffAt_map_inverse
rw [inCoordinates_eq (FiberBundle.mem_baseSet_trivializationAt' x₀)
(FiberBundle.mem_baseSet_trivializationAt' (f x₀))]
exact
isInvertible_equiv.comp
(hf'.comp isInvertible_equiv)
-- the inverse in coordinates coincides with the in-coordinate version of the inverse,
-- therefore the previous point gives the conclusion
apply this.congr_of_eventuallyEq_of_mem _ hx₀
have A : (trivializationAt E (TangentSpace I) x₀).baseSet ∈ 𝓝[s] x₀ :=
by
apply nhdsWithin_le_nhds
apply (trivializationAt _ _ _).open_baseSet.mem_nhds
exact FiberBundle.mem_baseSet_trivializationAt' _
have B : f ⁻¹' (trivializationAt E' (TangentSpace I') (f x₀)).baseSet ∈ 𝓝[s] x₀ :=
by
apply hf.continuousWithinAt.preimage_mem_nhdsWithin
apply (trivializationAt _ _ _).open_baseSet.mem_nhds
exact FiberBundle.mem_baseSet_trivializationAt' _
filter_upwards [A, B] with x hx h'x
simp only [Function.comp_apply]
rw [inCoordinates_eq hx h'x, inCoordinates_eq h'x (by exact hx)]
simp only [inverse_equiv_comp, inverse_comp_equiv, ContinuousLinearEquiv.symm_symm, ϕ]
rfl
