English
If V is a differentiable vector field on M' and f: M→M' is C^n with n≥2 and the derivative of f is invertible, then the pullback vector field is C^m at a point x0.
Русский
Если V — дифференцируемое векторное поле на M', и f: M→M' — C^n с n≥2 и производная f обратима, тогда пуллбэк-векторное поле гладко класса C^m в точке x0.
LaTeX
$$$\text{If } V\in C^m(M'), \ f\in C^n(M,M'), \ mfderiv f \text{ invertible } n\ge 2, \text{ then } mpullback(V,f) \in C^m \text{ at } x_0.$$$
Lean4
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
`m + 1 ≤ n` is `C^m`.
Version within a set at a point. -/
protected theorem _root_.ContMDiffWithinAt.mpullbackWithin_vectorField_inter
(hV : ContMDiffWithinAt I' I'.tangent m (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 : m + 1 ≤ n) :
ContMDiffWithinAt I I.tangent m (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t)
x₀ :=
by
/- We want to apply the theorem `ContMDiffWithinAt.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 : ContMDiffWithinAt I I'.tangent m (fun x ↦ (v x : TangentBundle I' M')) (s ∩ f ⁻¹' t) x₀ :=
by
apply hV.comp x₀ ((hf.of_le (le_trans (le_self_add) hmn)).mono inter_subset_left)
exact MapsTo.mono_left (mapsTo_preimage _ _) inter_subset_right
suffices hϕ :
ContMDiffWithinAt I 𝓘(𝕜, E' →L[𝕜] E) m
(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 ContMDiffWithinAt.clm_apply_of_inCoordinates (hϕ.mono inter_subset_left) hv contMDiffWithinAt_id
have :
ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
(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.mfderivWithin_const hmn hx₀ hs
have :
ContMDiffWithinAt I 𝓘(𝕜, E' →L[𝕜] E) m
(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 ContMDiffAt.comp_contMDiffWithinAt _ _ this
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
