Restricting the scalars of C^n maps between manifolds

Let 𝕜' be a normed algebra over 𝕜, and let E and E' be normed spaces over both fields, compatibly. A boundaryless model I and its scalar restriction I.restrictScalars 𝕜 have the same coordinate maps and use the same charted space. This file shows that a map which is C^n for boundaryless models over 𝕜' is C^n for their scalar restrictions over 𝕜: in charts, apply ContDiffWithinAt.restrict_scalars. The models need not be trivial, so the same API applies to products and continuous-linear changes of model.

For the underlying real manifold construction, see Huybrechts, Complex Geometry, Chapter 1.

The main example is a holomorphic map between complex manifolds modelled on 𝓘(ℂ, E) and 𝓘(ℂ, E'), which is a smooth map between the underlying real manifolds modelled on 𝓘(ℝ, E) and 𝓘(ℝ, E').

Main results

• ContMDiffWithinAt.restrictScalars, ContMDiffAt.restrictScalars, ContMDiffOn.restrictScalars, ContMDiff.restrictScalars: a C^n map over 𝕜' (within a set, at a point, on a set, globally) is C^n over 𝕜.

theorem ContMDiffWithinAt.restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E'] [IsScalarTower 𝕜 𝕜' E'] {H : Type u_5} {H' : Type u_6} [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜' E H} {I' : ModelWithCorners 𝕜' E' H'} [I.Boundaryless] [I'.Boundaryless] {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} {x : M} (h : ContMDiffWithinAt I I' n f s x) : ContMDiffWithinAt (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') n f s x

A map which is C^n within a set at a point for the models over 𝕜' is C^n within that set at that point for the models over the smaller field 𝕜.

theorem ContMDiffAt.restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E'] [IsScalarTower 𝕜 𝕜' E'] {H : Type u_5} {H' : Type u_6} [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜' E H} {I' : ModelWithCorners 𝕜' E' H'} [I.Boundaryless] [I'.Boundaryless] {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f : M → N} {x : M} (h : ContMDiffAt I I' n f x) : ContMDiffAt (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') n f x

A map which is C^n at a point for the models over 𝕜' is C^n at that point for the models over the smaller field 𝕜.

theorem ContMDiffOn.restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E'] [IsScalarTower 𝕜 𝕜' E'] {H : Type u_5} {H' : Type u_6} [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜' E H} {I' : ModelWithCorners 𝕜' E' H'} [I.Boundaryless] [I'.Boundaryless] {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} (h : ContMDiffOn I I' n f s) : ContMDiffOn (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') n f s

A map which is C^n on a set for the models over 𝕜' is C^n on that set for the models over the smaller field 𝕜.

theorem ContMDiff.restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {E' : Type u_4} [NormedAddCommGroup E'] [NormedSpace 𝕜 E'] [NormedSpace 𝕜' E'] [IsScalarTower 𝕜 𝕜' E'] {H : Type u_5} {H' : Type u_6} [TopologicalSpace H] [TopologicalSpace H'] {I : ModelWithCorners 𝕜' E H} {I' : ModelWithCorners 𝕜' E' H'} [I.Boundaryless] [I'.Boundaryless] {M : Type u_7} [TopologicalSpace M] [ChartedSpace H M] {N : Type u_8} [TopologicalSpace N] [ChartedSpace H' N] {n : WithTop ℕ∞} {f : M → N} (h : ContMDiff I I' n f) : ContMDiff (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') n f

A C^n map for boundaryless models over 𝕜' is C^n for their scalar restrictions to 𝕜. For instance, a holomorphic map between complex manifolds is smooth.