English
The tangent map of chart symmetrically relates to the inverse chart in the tangent bundle, via the product identification.
Русский
Граф касательной симметрично связывает обратную карту касательного расхождения через произведение, используя идентификацию.
LaTeX
$$$\\text{tangentMap } I I (chartAt\\ H p.1).symm = (chartAt (ModelProd H E) p).symm \\circ \\mathrm{TotalSpace.toProd}_{H,E}.$$$
Lean4
/-- The derivative of the inverse of the chart at a base point is the inverse of the chart of the
tangent bundle, composed with the identification between the tangent bundle of the model space and
the product space. -/
theorem tangentMap_chart_symm {p : TangentBundle I M} {q : TangentBundle I H} (h : q.1 ∈ (chartAt H p.1).target) :
tangentMap I I (chartAt H p.1).symm q = (chartAt (ModelProd H E) p).symm (TotalSpace.toProd H E q) :=
by
dsimp only [tangentMap]
rw [MDifferentiableAt.mfderiv (mdifferentiableAt_atlas_symm (chart_mem_atlas _ _) h)]
simp only [TangentBundle.chartAt, tangentBundleCore, mfld_simps, (· ∘ ·)]
-- `simp` fails to apply `PartialEquiv.prod_symm` with `ModelProd`
congr
exact ((chartAt H (TotalSpace.proj p)).right_inv h).symm
