English
The tangent map at a chart equals the inverse identification between the tangent bundle and the product space, via the chart on the model product.
Русский
Линейное отображение касательной в точке-chart равняется обратно найденной идентификации между касательным расхождением и произведением, осуществляемой через карту-чарт на модельном произведении.
LaTeX
$$$\\text{tangentMap } I I (chartAt\\ H\\ p) = (TotalSpace.toProd\\ H\\ E)^{-1} \\circ (chartAt\\ (ModelProd\\ H\\ E)\\ p) \\;\\; \\text{ on appropriate domain.}$$$
Lean4
/-- The derivative of the chart at a base point is 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 {p q : TangentBundle I M} (h : q.1 ∈ (chartAt H p.1).source) :
tangentMap I I (chartAt H p.1) q =
(TotalSpace.toProd _ _).symm ((chartAt (ModelProd H E) p : TangentBundle I M → ModelProd H E) q) :=
by
dsimp [tangentMap]
rw [MDifferentiableAt.mfderiv]
· rfl
· exact mdifferentiableAt_atlas (chart_mem_atlas _ _) h
