English
The inCoordinates mapping at the tangent bundle core model space is the identity, i.e., it acts as the identity on coordinates.
Русский
Карта inCoordinates в ядре касательного bundle на модельном пространстве действует как тождественная на координатах.
LaTeX
$$$inCoordinates E (TangentSpace I) E' (TangentSpace I') x_0 x y_0 y ϕ = ϕ$ for all x_0, x, y_0, y, ϕ$$
Lean4
/-- When `ϕ x` is a continuous linear map that changes vectors in charts around `f x` to vectors
in charts around `g x`, `inTangentCoordinates I I' f g ϕ x₀ x` is a coordinate change of
this continuous linear map that makes sense from charts around `f x₀` to charts around `g x₀`
by composing it with appropriate coordinate changes.
Note that the type of `ϕ` is more accurately
`Π x : N, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)`.
We are unfolding `TangentSpace` in this type so that Lean recognizes that the type of `ϕ` doesn't
actually depend on `f` or `g`.
This is the underlying function of the trivializations of the hom of (pullbacks of) tangent spaces.
-/
def inTangentCoordinates (f : N → M) (g : N → M') (ϕ : N → E →L[𝕜] E') : N → N → E →L[𝕜] E' := fun x₀ x =>
inCoordinates E (TangentSpace I) E' (TangentSpace I') (f x₀) (f x) (g x₀) (g x) (ϕ x)
