English
For a morphism f: B→LE1E2, differentiability at a point x0 is equivalent to the differentiability of the base projection and of the fiber-coordinate map at x0, in coordinates.
Русский
Для отображения f: B→LE1E2 дифференцируемость в точке равносильна дифференцируемости базовой проекции и координат по волокну в точке x0, в координатах.
LaTeX
$$$\\text{mdiffAt}(f,x_0) \\iff \\text{mdiffAt}(f|_{base},x_0) \\land \\text{mdiffAt}(coordinates, x_0)$$$
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 `ContMDiffWithinAt`. We also give a version for `ContMDiffAt`, 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 `ContMDiffWithinAt.clm_bundle_apply`
-/
theorem clm_apply_of_inCoordinates
(hϕ :
ContMDiffWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) n (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s
m₀)
(hv : ContMDiffWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) n (fun m ↦ (v m : TotalSpace F₁ E₁)) s m₀)
(hb₂ : ContMDiffWithinAt IM IB₂ n b₂ s m₀) :
ContMDiffWithinAt IM (IB₂.prod 𝓘(𝕜, F₂)) n (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) s m₀ :=
by
rw [← contMDiffWithinAt_insert_self] at hϕ hv hb₂ ⊢
rw [contMDiffWithinAt_totalSpace] at hv ⊢
refine ⟨hb₂, ?_⟩
apply (ContMDiffWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_of_mem ?_ (mem_insert m₀ s)
have A : ∀ᶠ m in 𝓝[insert m₀ s] m₀, b₁ m ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet :=
by
apply hv.1.continuousWithinAt
apply (trivializationAt F₁ E₁ (b₁ m₀)).open_baseSet.mem_nhds
exact FiberBundle.mem_baseSet_trivializationAt' (b₁ m₀)
have A' : ∀ᶠ m in 𝓝[insert m₀ s] m₀, b₂ m ∈ (trivializationAt F₂ E₂ (b₂ m₀)).baseSet :=
by
apply hb₂.continuousWithinAt
apply (trivializationAt F₂ E₂ (b₂ m₀)).open_baseSet.mem_nhds
exact FiberBundle.mem_baseSet_trivializationAt' (b₂ m₀)
filter_upwards [A, A'] with m hm h'm
rw [inCoordinates_eq hm h'm]
simp only [coe_comp', ContinuousLinearEquiv.coe_coe, Trivialization.continuousLinearEquivAt_apply,
Trivialization.continuousLinearEquivAt_symm_apply, Function.comp_apply]
congr
rw [Trivialization.symm_apply_apply_mk (trivializationAt F₁ E₁ (b₁ m₀)) hm (v m)]
