English
The chartAt for the tangent bundle in model space matches the product chart at the base space.
Русский
ChartAt касательного пространства в модельном пространстве совпадает с произведением чарта базового пространства.
LaTeX
$$$\text{tangentBundle_model_space_chartAt}$$$
Lean4
/-- In the tangent bundle to the model space, the charts are just the canonical identification
between a product type and a sigma type, a.k.a. `TotalSpace.toProd`. -/
@[simp, mfld_simps]
theorem tangentBundle_model_space_chartAt (p : TangentBundle I H) :
(chartAt (ModelProd H E) p).toPartialEquiv = (TotalSpace.toProd H E).toPartialEquiv :=
by
ext x : 1
· ext; · rfl
exact (tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2
· ext; · rfl
apply heq_of_eq
exact (tangentBundleCore I H).coordChange_self (achart _ x.1) x.1 (mem_achart_source H x.1) x.2
simp_rw [TangentBundle.chartAt, FiberBundleCore.localTriv, FiberBundleCore.localTrivAsPartialEquiv,
VectorBundleCore.toFiberBundleCore_baseSet, tangentBundleCore_baseSet]
simp only [mfld_simps]
