English
The symm application at base point b to L is the same as composing with e2.symmL and L composed with e1.continuousLinearMapAt.
Русский
Симм-применение в точке b к L равно композиции с e2.symmL и L, композиция с e1.continuousLinearMapAt.
LaTeX
$$$ (continuousLinearMap σ e_1 e_2).symm b L = (e_2.symmL 𝕜_2 b).comp (L.comp (e_1.continuousLinearMapAt 𝕜_1 b)) $$$
Lean4
theorem continuousLinearMapCoordChange_apply (b : B) (hb : b ∈ e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
(L : F₁ →SL[σ] F₂) :
continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂' b L =
(continuousLinearMap σ e₁' e₂' ⟨b, (continuousLinearMap σ e₁ e₂).symm b L⟩).2 :=
by
ext v
simp_rw [continuousLinearMapCoordChange, ContinuousLinearEquiv.coe_coe, ContinuousLinearEquiv.arrowCongrSL_apply,
continuousLinearMap_apply, continuousLinearMap_symm_apply' σ e₁ e₂ hb.1, comp_apply, ContinuousLinearEquiv.coe_coe,
ContinuousLinearEquiv.symm_symm, Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply]
rw [e₂.coordChangeL_apply e₂', e₁'.coordChangeL_apply e₁, e₁.coe_linearMapAt_of_mem hb.1.1,
e₂'.coe_linearMapAt_of_mem hb.2.2]
exacts [⟨hb.2.1, hb.1.1⟩, ⟨hb.1.2, hb.2.2⟩]
