English
For a morphism f: B→LE1E2, differentiability at a point is equivalent to differentiability of the base component and the coordinate component, in the sense of ContMDiffAt.
Русский
Для отображения f: B→LE1E2 дифференцируемость в точке равносильна дифференцируемости базовой и координатной части в смысле ContMDiffAt.
LaTeX
$$$\\text{contMDiffAt}(f) \\iff \\text{contMDiffAt}(f.\\text{proj}) \\land \\text{contMDiffAt}(\\text{inCoordinates}(f))$$$
Lean4
/-- Consider a `C^n` map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another base map `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending smoothly
on `m`, one can apply `ϕ m` to `g m`, and the resulting map is `C^n`.
Note that the smoothness of `ϕ` cannot be always be stated as smoothness of a map into a manifold,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` are smooth manifolds only when `b₁` and `b₂` are
globally smooth, but we want to apply this lemma with only local information. Therefore, we
formulate it using smoothness of `ϕ` read in coordinates.
Version for `ContMDiffAt`. We also give a version for `ContMDiffWithinAt`, but no version for
`ContMDiffOn` or `ContMDiff` as our assumption, written in coordinates, only makes sense around
a point.
For a version with `B₁ = B₂` and `b₁ = b₂`, in which smoothness can be expressed without
`inCoordinates`, see `ContMDiffAt.clm_bundle_apply`
-/
theorem clm_apply_of_inCoordinates
(hϕ : ContMDiffAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hv : ContMDiffAt IM (IB₁.prod 𝓘(𝕜, F₁)) n (fun m ↦ (v m : TotalSpace F₁ E₁)) m₀)
(hb₂ : ContMDiffAt IM IB₂ n b₂ m₀) :
ContMDiffAt IM (IB₂.prod 𝓘(𝕜, F₂)) n (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) m₀ :=
by
rw [← contMDiffWithinAt_univ] at hϕ hv hb₂ ⊢
exact ContMDiffWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂
