English
Rewrite the coordinate-change map in coordinates using trivializations; the inCoordinates construction equals the composition of continuous linear maps provided by the trivializations and fiber bundle changes.
Русский
Переопределение перехода координат через координаты: inCoordinates равен композиции непрерывно-линейных отображений, задаваемых тривиализациями и сменами координат волокон.
LaTeX
$$$$ inCoordinates F E F' E' x_0 x y_0 y ϕ = (trivializationAt F' E' y_0).continuousLinearEquivAt 𝕜_2 y hy .comp ϕ .comp (trivializationAt F E x_0).continuousLinearEquivAt 𝕜_1 x hx $$$$
Lean4
/-- When `ϕ` is a continuous (semi)linear map between the fibers `E x` and `E' y` of two vector
bundles `E` and `E'`, `ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ` is a coordinate
change of this continuous linear map w.r.t. the chart around `x₀` and the chart around `y₀`.
It is defined by composing `ϕ` with appropriate coordinate changes given by the vector bundles
`E` and `E'`.
We use the operations `Trivialization.continuousLinearMapAt` and `Trivialization.symmL` in the
definition, instead of `Trivialization.continuousLinearEquivAt`, so that
`ContinuousLinearMap.inCoordinates` is defined everywhere (but see
`ContinuousLinearMap.inCoordinates_eq`).
This is the (second component of the) underlying function of a trivialization of the hom-bundle
(see `hom_trivializationAt_apply`). However, note that `ContinuousLinearMap.inCoordinates` is
defined even when `x` and `y` live in different base sets.
Therefore, it is also convenient when working with the hom-bundle between pulled back bundles.
-/
def inCoordinates (x₀ x : B) (y₀ y : B') (ϕ : E x →SL[σ] E' y) : F →SL[σ] F' :=
((trivializationAt F' E' y₀).continuousLinearMapAt 𝕜₂ y).comp <| ϕ.comp <| (trivializationAt F E x₀).symmL 𝕜₁ x
