English
The symmL of the trivialization At at b0 equals the tangentBundleCore.coordChange between charts; i.e., trivializationAt.symmL equals coordChange.
Русский
Обратное тривиализации симмL равно coordChange между чартаками; то есть симмL тривиализации равен coordChange.
LaTeX
$$$\mathrm{trivializationAt}\,E\,(\mathrm{TangentSpace}\,I)\;b_0).\mathrm{symmL} \; \mathbb{K} \; b = (\mathrm{tangentBundleCore}\;I\;M).coordChange (\operatorname{achart} H b_0) (\operatorname{achart} H b) b$$$
Lean4
/-- The inverse trivialization of the tangent space can be expressed in terms of the tangent bundle
core. To write it as the manifold derivative of `(extChartAt I b₀).symm`, see
`TangentBundle.symmL_trivializationAt`.
Use with care as it abuses the defeq `TangentSpace I b = E`. -/
theorem symmL_trivializationAt_eq_core {b₀ b : M} (hb : b ∈ (chartAt H b₀).source) :
(trivializationAt E (TangentSpace I) b₀).symmL 𝕜 b =
(tangentBundleCore I M).coordChange (achart H b₀) (achart H b) b :=
by simp [hb]
