English
If a family of linear maps ϕ_m depends differentiably on m, and v is differentiable along with a differentiable base map, then the map m ↦ ϕ_m(v_m) is differentiable in the corresponding coordinate sense.
Русский
Если семейство линейных отображений ϕ_m зависит дифференцируемо от m, и v дифференцируема вместе с базовой картой, то отображение m ↦ ϕ_m(v_m) дифференцируемо в соответствующей координатной записи.
LaTeX
$$$(\\forall m,\\; ϕ_m: E_1(b_1 m) \\to E_2(b_2 m))$, $v_m \\in E_1(b_1 m)$, $ϕ_m$ дифференцируемо по m и $v$ дифференцимо; тогда $m \\mapsto ϕ_m(v_m)$ дифференцируемо.$$
Lean4
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a basemap `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
differentiably on `m`, one can apply `ϕ m` to `g m`, and the resulting map is differentiable.
Note that the differentiability of `ϕ` cannot be always be stated as differentiability of a map
into a manifold, as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only make sense when `b₁`
and `b₂` are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of `ϕ` read in coordinates.
Version for `MDifferentiableWithinAt`. We also give a version for `MDifferentiableAt`, but no
version for `MDifferentiableOn` or `MDifferentiable` as our assumption, written in coordinates,
only makes sense around a point.
-/
theorem clm_apply_of_inCoordinates
(hϕ :
MDifferentiableWithinAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂)
(fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀)
(hv : MDifferentiableWithinAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m ↦ (v m : TotalSpace F₁ E₁)) s m₀)
(hb₂ : MDifferentiableWithinAt IM IB₂ b₂ s m₀) :
MDifferentiableWithinAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) s m₀ :=
by
rw [mdifferentiableWithinAt_totalSpace] at hv ⊢
refine ⟨hb₂, ?_⟩
apply (MDifferentiableWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_insert
have A : ∀ᶠ m in 𝓝[insert m₀ s] m₀, b₁ m ∈ (trivializationAt F₁ E₁ (b₁ m₀)).baseSet :=
by
apply hv.1.insert.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₂.insert.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)]
