English
The pullback commutes with the Lie bracket of vector fields: pullback(f)([V, W]) = [pullback(f)V, pullback(f)W].
Русский
Тогда пересылка по f commuting-скобка Ли: подстановочная скобка(S) = скобка-подстановок.
LaTeX
$$$\mathrm{mpullback}(I, I', f) (\mathrm{mlieBracket}(I', V, W)) = \mathrm{mlieBracket}(I, \mathrm{mpullback}(I, I', f, V), \mathrm{mpullback}(I, I', f, W))$$$
Lean4
theorem mpullbackWithin_mlieBracketWithin_of_isSymmSndFDerivWithinAt {f : M → M'} {V W : Π (x : M'), TangentSpace I' x}
{x₀ : M} {s : Set M} {t : Set M'}
(hV : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (V x : TangentBundle I' M')) t (f x₀))
(hW : MDifferentiableWithinAt I' I'.tangent (fun x ↦ (W x : TangentBundle I' M')) t (f x₀)) (hu : UniqueMDiffOn I s)
(hf : ContMDiffWithinAt I I' 2 f s x₀) (hx₀ : x₀ ∈ s) (hst : f ⁻¹' t ∈ 𝓝[s] x₀)
(hsymm :
IsSymmSndFDerivWithinAt 𝕜 ((extChartAt I' (f x₀)) ∘ f ∘ (extChartAt I x₀).symm)
((extChartAt I x₀).symm ⁻¹' s ∩ range I) (extChartAt I x₀ x₀)) :
mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀ =
mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀ :=
by
have A : (extChartAt I x₀).symm (extChartAt I x₀ x₀) = x₀ := by simp
by_cases hfi : (mfderivWithin I I' f s x₀).IsInvertible; swap
· simp only [mlieBracketWithin_apply, mpullbackWithin_apply, ContinuousLinearMap.inverse_of_not_isInvertible hfi,
ContinuousLinearMap.zero_apply]
rw [lieBracketWithin_eq_zero_of_eq_zero]
· simp [-extChartAt]
· simp only [mpullbackWithin_apply]
rw [A, ContinuousLinearMap.inverse_of_not_isInvertible hfi]
simp [-extChartAt]
· simp only [mpullbackWithin_apply]
rw [A, ContinuousLinearMap.inverse_of_not_isInvertible hfi]
simp [-extChartAt]
-- Now, interesting case where the derivative of `f` is invertible
have : CompleteSpace E' := by
rcases hfi with ⟨M, -⟩
let M' : E ≃L[𝕜] E' := M
exact
(completeSpace_congr (e := M'.toEquiv) M'.isUniformEmbedding).1
(by assumption)
-- choose a small open set `v` around `x₀` where `f` is `C^2`
obtain ⟨u, u_open, x₀u, ut, maps_u, u_smooth⟩ :
∃ u,
IsOpen u ∧
x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u) :=
by
obtain ⟨u, u_open, x₀u, hu⟩ : ∃ u, IsOpen u ∧ x₀ ∈ u ∧ ContMDiffOn I I' 2 f (insert x₀ s ∩ u) :=
hf.contMDiffOn' le_rfl (by simp)
have : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀ :=
hf.continuousWithinAt.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (f x₀))
rcases mem_nhdsWithin.1 (Filter.inter_mem hst this) with ⟨w, w_open, x₀w, hw⟩
refine ⟨u ∩ w, u_open.inter w_open, by simp [x₀u, x₀w], ?_, ?_, ?_⟩
· apply Subset.trans _ (hw.trans inter_subset_left)
exact fun y hy ↦ ⟨hy.2.2, hy.1⟩
· apply Subset.trans _ (hw.trans inter_subset_right)
exact fun y hy ↦ ⟨hy.2.2, hy.1⟩
· apply hu.mono
exact fun y hy ↦ ⟨subset_insert _ _ hy.1, hy.2.1⟩
have u_mem : u ∈ 𝓝 x₀ := u_open.mem_nhds x₀u
set s' := s ∩ u with hs'
have s'_eq : s' =ᶠ[𝓝 x₀] s := by
filter_upwards [u_mem] with y hy
change (y ∈ s ∩ u) = (y ∈ s)
simp [hy]
set t' := t ∩ (extChartAt I' (f x₀)).source with ht'
calc
mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
_ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s' x₀ := by
simp only [mpullbackWithin, hs', mfderivWithin_inter u_mem]
_ = mpullbackWithin I I' f (mlieBracketWithin I' V W t') s' x₀ := by
simp only [mpullbackWithin, ht', mlieBracketWithin_inter (extChartAt_source_mem_nhds (f x₀))]
_ = mlieBracketWithin I (mpullbackWithin I I' f V s') (mpullbackWithin I I' f W s') s' x₀ :=
by
apply
mpullbackWithin_mlieBracketWithin_aux (t := t') (hV.mono inter_subset_left) (hW.mono inter_subset_left)
(hu.inter u_open) u_smooth ⟨hx₀, x₀u⟩ inter_subset_right (fun y hy ↦ ⟨ut hy, maps_u hy⟩)
apply hsymm.congr_set
have : (extChartAt I x₀).symm ⁻¹' u ∈ 𝓝 (extChartAt I x₀ x₀) :=
by
apply (continuousAt_extChartAt_symm x₀).preimage_mem_nhds
apply u_open.mem_nhds (by simpa using x₀u)
filter_upwards [this] with y hy
change (y ∈ (extChartAt I x₀).symm ⁻¹' s ∩ range I) = (y ∈ (extChartAt I x₀).symm ⁻¹' (s ∩ u) ∩ range I)
simp [-extChartAt, hy]
_ = mlieBracketWithin I (mpullbackWithin I I' f V s') (mpullbackWithin I I' f W s') s x₀ := by
simp only [hs', mlieBracketWithin_inter u_mem]
_ = mlieBracketWithin I (mpullbackWithin I I' f V s) (mpullbackWithin I I' f W s) s x₀ :=
by
apply Filter.EventuallyEq.mlieBracketWithin_vectorField_eq_of_mem _ _ hx₀
· apply nhdsWithin_le_nhds
filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq] with y hy using by
simp [mpullbackWithin, hy]
· apply nhdsWithin_le_nhds
filter_upwards [mfderivWithin_eventually_congr_set (I := I) (I' := I') (f := f) s'_eq] with y hy using by
simp [mpullbackWithin, hy]
