English
For bundles over a base manifold B with a linear map on fibers varying continuously along B, the local charts for the induced morphism of vector bundles align with coordinates, i.e., the chart at a base point is the base chart together with the fiber coordinates given by inCoordinates.
Русский
Для расслоений над базой и линейного отображения на волокнах, зависящего непрерывно от точки основания, локальные карты соответствуют координатам, где карта будет состоять из базового чартa и координат по волокну через inCoordinates.
LaTeX
$$$\\text{hom_chart}(y_0,y) = (chartAtHB, inCoordinates(·))$$$
Lean4
@[simp]
theorem mem_contMDiffFiberwiseLinear_iff {n : WithTop ℕ∞} (e : OpenPartialHomeomorph (B × F) (B × F)) :
e ∈ contMDiffFiberwiseLinear B F IB n ↔
∃ (φ : B → F ≃L[𝕜] F) (U : Set B) (hU : IsOpen U) (hφ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => φ x : B → F →L[𝕜] F) U) (h2φ :
ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun x => (φ x).symm : B → F →L[𝕜] F) U),
e.EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hU hφ.continuousOn h2φ.continuousOn) :=
mem_aux
