English
The inverse trivialization of the tangent bundle at a point is given by the derivative of the inverse extended chart.
Русский
Обратная тривиализация касательных у точки задана производной от обратного расширенного чарта.
LaTeX
$$$(\text{trivializationAt } E (\text{TangentSpace } I) x_0)^{-1} = \mathrm{mfderivWithin}\ 𝓘(𝕜,E) I (\operatorname{extChartAt} I x_0)^{-1} (\cdot)$$$
Lean4
/-- The inverse trivialization of the tangent bundle at a point is the manifold derivative of the
inverse of the extended chart.
Use with care as this abuses the defeq `TangentSpace 𝓘(𝕜, E) y = E` for `y : E`. -/
theorem symmL_trivializationAt {x₀ x : M} (hx : x ∈ (chartAt H x₀).source) :
(trivializationAt E (TangentSpace I) x₀).symmL 𝕜 x =
mfderivWithin 𝓘(𝕜, E) I (extChartAt I x₀).symm (range I) (extChartAt I x₀ x) :=
by
have : MDifferentiableWithinAt 𝓘(𝕜, E) I ((chartAt H x₀).symm ∘ I.symm) (range I) (I (chartAt H x₀ x)) := by
simpa using mdifferentiableWithinAt_extChartAt_symm (by simp [hx])
simp [hx, mfderivWithin, this]
