Restricting the scalars of manifold derivatives #
Let 𝕜' be a normed algebra over 𝕜, and let E and E' be normed spaces over both fields,
compatibly. A manifold charted by E carries the trivial models 𝓘(𝕜', E) and 𝓘(𝕜, E) with the
same charts. This file shows that a map between such manifolds which is differentiable for the
models over 𝕜' is differentiable for the models over 𝕜, and that its derivative over 𝕜 is the
derivative over 𝕜' with scalars restricted to 𝕜.
The tangent spaces TangentSpace 𝓘(𝕜', E) x and TangentSpace 𝓘(𝕜, E) x are both the model space
E, but they are distinct types carrying module structures over different fields. The comparison of
derivatives is therefore stated after reading both derivatives in the model spaces through the
identifications tangentSpaceCastModel, which is also how HasMFDerivWithinAt reads a derivative
in charts.
The main example is a holomorphic map between complex manifolds modelled on 𝓘(ℂ, E) and
𝓘(ℂ, E'): its real derivative is its complex derivative regarded as an ℝ-linear map.
Likewise, the tangent coordinate changes of a complex manifold, regarded as a real manifold, are
its complex tangent coordinate changes regarded as ℝ-linear maps.
The fibrewise linear equivalence identifies the native self-model tangent spaces over the two fields and intertwines their manifold and vector-valued derivatives.
Main results #
TauCeti.tangentSpaceRestrictScalarsSelfLinearEquivand its_apply/_symm_applyformulas: the comparison into the native smaller-field self-model tangent fibre.MDifferentiableAt.mfderiv_restrictScalarsSelf_applyandMDifferentiableAt.mvfderiv_restrictScalarsSelf_apply: derivative comparison through this fibre equivalence.MDifferentiableWithinAt.restrictScalars,MDifferentiableAt.restrictScalars,MDifferentiableOn.restrictScalars,MDifferentiable.restrictScalars: differentiability over𝕜'implies differentiability over𝕜.HasMFDerivWithinAt.restrictScalars,HasMFDerivAt.restrictScalars: a derivative over𝕜', with scalars restricted to𝕜, is a derivative over𝕜.HasMFDerivWithinAt.of_restrictScalars: conversely, a𝕜'-linear map whose scalar restriction is a derivative over𝕜is a derivative over𝕜'.MDifferentiableWithinAt.restrictScalars_mfderivWithin,MDifferentiableAt.mfderiv_restrictScalars: the derivative over𝕜is the derivative over𝕜'with scalars restricted to𝕜.TauCeti.injective_mfderiv_restrictScalars: an immersion for the models over𝕜'is an immersion for the models over𝕜.TauCeti.tangentCoordChange_restrictScalars: the tangent coordinate changes over𝕜are those over𝕜'with scalars restricted to𝕜; in particular they are𝕜'-linear (TauCeti.tangentCoordChange_smul), and so is the derivative of the inverse of a chart (TauCeti.mfderivWithin_extChartAt_symm_smul).
A map which is differentiable within a set at a point for the models over 𝕜' is
differentiable within that set at that point for the models over the smaller field 𝕜.
A map which is differentiable at a point for the models over 𝕜' is differentiable at that
point for the models over the smaller field 𝕜.
A map which is differentiable on a set for the models over 𝕜' is differentiable on that set
for the models over the smaller field 𝕜.
A map which is differentiable for the models over 𝕜' is differentiable for the models over
the smaller field 𝕜.
If f' is a derivative of f within a set at a point for the models over 𝕜', and g' is a
𝕜-linear map between the tangent spaces over 𝕜 which agrees with f' once both are read in the
model spaces, then g' is a derivative of f within that set at that point for the models over
𝕜.
If f' is a derivative of f at a point for the models over 𝕜', and g' is a 𝕜-linear map
between the tangent spaces over 𝕜 which agrees with f' once both are read in the model spaces,
then g' is a derivative of f at that point for the models over 𝕜.
If g' is a derivative of f within a set at a point for the models over 𝕜, and f' is a
𝕜'-linear map between the tangent spaces over 𝕜' which agrees with g' once both are read in
the model spaces, then f' is a derivative of f within that set at that point for the models
over 𝕜'. This is the converse of HasMFDerivWithinAt.restrictScalars.
If g' is a derivative of f at a point for the models over 𝕜, and f' is a 𝕜'-linear map
between the tangent spaces over 𝕜' which agrees with g' once both are read in the model spaces,
then f' is a derivative of f at that point for the models over 𝕜'. This is the converse of
HasMFDerivAt.restrictScalars.
At a point where f is differentiable within a set for the models over 𝕜', and where the set
has unique derivatives over the smaller field 𝕜, the derivative of f within the set over 𝕜 is
its derivative over 𝕜' with scalars restricted to 𝕜, both read in the model spaces.
At a point where f is differentiable for the models over 𝕜', the derivative of f over the
smaller field 𝕜 is its derivative over 𝕜' with scalars restricted to 𝕜, both read in the model
spaces. For instance, the real derivative of a holomorphic map is its complex derivative.
If the derivative of f at x over 𝕜' is injective, then so is its derivative over the
smaller field 𝕜. For instance, a holomorphic immersion between complex manifolds is a real
immersion. Where f is not differentiable over 𝕜' its derivative over 𝕜' is 0, and
injectivity of that derivative forces the tangent space to be trivial.
On the overlap of the charts at x and y, the tangent coordinate change for the model over
𝕜 is the tangent coordinate change for the model over 𝕜', with scalars restricted to 𝕜: both
are the derivative of the same chart transition. For instance, the tangent coordinate changes of
a complex manifold, regarded as a real manifold, are complex linear.
On the overlap of the charts at x and y, the tangent coordinate change for the model over
𝕜 is 𝕜'-linear. For instance, the real tangent coordinate changes of a complex manifold are
complex linear.
On the target of the chart at x, the derivative over 𝕜 of the inverse of the chart is
𝕜'-linear: it is a tangent coordinate change. For instance, on a complex manifold, regarded as
a real manifold, the real derivative of the inverse of a chart commutes with multiplication by
i.
Scalar restriction identifies a self-model tangent fibre with the native self-model fibre over the smaller field.
Instances For
Native self-model scalar restriction preserves preferred tangent coordinates.
The inverse native self-model comparison preserves preferred tangent coordinates.
The native self-model fibre comparison intertwines derivatives over the two fields.
Vector-valued derivatives agree through the native self-model fibre comparison.