Extended charts after restriction of scalars #
Restricting the scalars of a boundaryless model leaves its coordinate maps unchanged. Consequently its extended charts are unchanged as partial equivalences. This comparison allows differentiability and smoothness arguments in these coordinates to use scalar restriction without replacing the charted space, including for product and recharted models.
For underlying real manifolds, see Huybrechts, Complex Geometry, Chapter 1.
theorem
ModelWithCorners.extChartAt_restrictScalars
(𝕜 : Type u_1)
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
{E : Type u_3}
{H : Type u_4}
{M : Type u_5}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜' E]
[TopologicalSpace H]
[TopologicalSpace M]
[ChartedSpace H M]
(I : ModelWithCorners 𝕜' E H)
[I.Boundaryless]
(x : M)
:
Scalar restriction leaves the extended chart unchanged, including its source, target, and inverse. No compatibility between the two scalar actions is needed for this equality.