English
Writing a linear map between tangent spaces in coordinates amounts to pre- and post-composing with derivatives of extended charts.
Русский
Запись линейного отображения между касательными пространствами в координатах равносильна предварительному и последующему композициям с производными от расширенных чартов.
LaTeX
$$$inTangentCoordinates I I' f g ϕ x_0 x = (mfderiv I' (extChartAt I' (g x_0)) (g x)) \\circ_L ϕ x \\circ_L (mfderivWithin I (extChartAt I (f x_0)).symm (range I) (extChartAt I (f x_0) (f x))).$$$
Lean4
/-- To write a linear map between tangent spaces in coordinates amounts to precomposing and
postcomposing it with derivatives of extended charts.
Concrete version of `inTangentCoordinates_eq`. -/
theorem inTangentCoordinates_eq_mfderiv_comp {N : Type*} {f : N → M} {g : N → M'}
{ϕ : Π x : N, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)} {x₀ : N} {x : N}
(hx : f x ∈ (chartAt H (f x₀)).source) (hy : g x ∈ (chartAt H' (g x₀)).source) :
inTangentCoordinates I I' f g ϕ x₀ x =
(mfderiv I' 𝓘(𝕜, E') (extChartAt I' (g x₀)) (g x)) ∘L
(ϕ x) ∘L (mfderivWithin 𝓘(𝕜, E) I (extChartAt I (f x₀)).symm (range I) (extChartAt I (f x₀) (f x))) :=
by
rw [inTangentCoordinates_eq _ _ _ hx hy, tangentBundleCore_coordChange]
congr
· have : MDifferentiableAt I' 𝓘(𝕜, E') (extChartAt I' (g x₀)) (g x) := mdifferentiableAt_extChartAt hy
simp_all [mfderiv]
· simp only [mfderivWithin, writtenInExtChartAt, modelWithCornersSelf_coe, range_id, inter_univ]
rw [if_pos]
· simp [Function.comp_def, OpenPartialHomeomorph.left_inv (chartAt H (f x₀)) hx]
· apply mdifferentiableWithinAt_extChartAt_symm
apply (extChartAt I (f x₀)).map_source
simpa using hx
