English
There is an explicit equality expressing inCoordinates in terms of continuous linear equivalences associated with trivializations around x0 and y0.
Русский
Существует явное равенство, выражающее inCoordinates через эквивалентности линейных отображений вокруг точек x0, y0.
LaTeX
$$$$ inCoordinates F E F' E' x_0 x y_0 y ϕ = ((trivializationAt F' E' y_0).continuousLinearEquivAt 𝕜_2 y hy : E' y \\to_L[𝕜_2] F').comp (ϕ.comp (((trivializationAt F E x_0).continuousLinearEquivAt 𝕜_1 x hx)^{-1}.toContinuousLinearMap)) $$$$
Lean4
/-- Rewrite `ContinuousLinearMap.inCoordinates` using continuous linear equivalences. -/
theorem inCoordinates_eq {x₀ x : B} {y₀ y : B'} {ϕ : E x →SL[σ] E' y} (hx : x ∈ (trivializationAt F E x₀).baseSet)
(hy : y ∈ (trivializationAt F' E' y₀).baseSet) :
inCoordinates F E F' E' x₀ x y₀ y ϕ =
((trivializationAt F' E' y₀).continuousLinearEquivAt 𝕜₂ y hy : E' y →L[𝕜₂] F').comp
(ϕ.comp <| (((trivializationAt F E x₀).continuousLinearEquivAt 𝕜₁ x hx).symm : F →L[𝕜₁] E x)) :=
by
ext
simp_rw [inCoordinates, ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe,
Trivialization.coe_continuousLinearEquivAt_eq, Trivialization.symm_continuousLinearEquivAt_eq]
