Restricting the scalars of a boundaryless manifold

Let 𝕜' be a normed algebra over 𝕜 and let E be a normed space over both fields, compatibly. A map which is C^n over 𝕜' is C^n over 𝕜, so the C^n groupoid of a boundaryless model I is contained in that of I.restrictScalars 𝕜. Consequently a C^n manifold modelled on I is, with the same charts, a C^n manifold modelled on I.restrictScalars 𝕜, and every chart of its maximal atlas over 𝕜' is a chart of its maximal atlas over 𝕜. The self-modelled specializations use 𝓘(𝕜', E) and 𝓘(𝕜, E).

The groupoid comparison is obtained from Mathlib's ContDiffOn.restrict_scalars.

The main example is a complex manifold modelled on 𝓘(ℂ, E), which is a real manifold modelled on 𝓘(ℝ, E); its holomorphic charts are real C^n charts. This is how real-analytic notions, such as the real Hessian at a critical point, are applied to complex manifolds.

Main results

• ModelWithCorners.contDiffGroupoid_le_restrictScalars, ModelWithCorners.isManifold_restrictScalars, and ModelWithCorners.maximalAtlas_subset_restrictScalars apply to boundaryless models.
• TauCeti.contDiffGroupoid_le_restrictScalars: the C^n groupoid over 𝕜' is contained in the C^n groupoid over 𝕜.
• IsManifold.restrictScalars: a C^n manifold over 𝕜' is a C^n manifold over 𝕜.
• IsManifold.maximalAtlas_subset_restrictScalars: the maximal atlas over 𝕜' is contained in the maximal atlas over 𝕜.
• TauCeti.ComplexManifold.isManifold_restrictScalars_real: scoped instance equipping a C^n manifold over a boundaryless complex model I with IsManifold (I.restrictScalars ℝ) n X.

theorem ModelWithCorners.contDiffGroupoid_le_restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} {H : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] {n : WithTop ℕ∞} : contDiffGroupoid n I ≤ contDiffGroupoid n (restrictScalars 𝕜 I)

Restricting scalars enlarges the smooth structure groupoid, without changing the coordinate maps of a boundaryless model.

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

The same atlas makes a boundaryless manifold a manifold over the smaller field.

theorem ModelWithCorners.maximalAtlas_subset_restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} {H : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] {n : WithTop ℕ∞} {M : Type u_5} [TopologicalSpace M] [ChartedSpace H M] : IsManifold.maximalAtlas I n M ⊆ IsManifold.maximalAtlas (restrictScalars 𝕜 I) n M

Every maximal chart over the larger field remains a maximal chart after restricting the scalars of a boundaryless model.

theorem TauCeti.contDiffGroupoid_le_restrictScalars {𝕜 : Type u_1} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {n : WithTop ℕ∞} : contDiffGroupoid n (modelWithCornersSelf 𝕜' E) ≤ contDiffGroupoid n (modelWithCornersSelf 𝕜 E)

The C^n groupoid of the trivial model over 𝕜' is contained in the C^n groupoid of the trivial model over the smaller field 𝕜.

theorem IsManifold.restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {n : WithTop ℕ∞} (h : IsManifold (modelWithCornersSelf 𝕜' E) n M) : IsManifold (modelWithCornersSelf 𝕜 E) n M

A C^n manifold modelled on 𝓘(𝕜', E) is a C^n manifold modelled on 𝓘(𝕜, E) with the same charts. For instance, a complex manifold is a real manifold.

theorem IsManifold.maximalAtlas_subset_restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {M : Type u_4} [TopologicalSpace M] [ChartedSpace E M] {n : WithTop ℕ∞} : maximalAtlas (modelWithCornersSelf 𝕜' E) n M ⊆ maximalAtlas (modelWithCornersSelf 𝕜 E) n M

Every chart of the C^n maximal atlas over 𝕜' is a chart of the C^n maximal atlas over the smaller field 𝕜. For instance, a holomorphic chart of a complex manifold is a real C^n chart.

theorem TauCeti.ComplexManifold.isManifold_restrictScalars_real {n : WithTop ℕ∞} {E : Type u_5} {H : Type u_6} {X : Type u_7} [NormedAddCommGroup E] [NormedSpace ℂ E] [TopologicalSpace H] {I : ModelWithCorners ℂ E H} [I.Boundaryless] [TopologicalSpace X] [ChartedSpace H X] [h : IsManifold I n X] : IsManifold (ModelWithCorners.restrictScalars ℝ I) n X

A C^n manifold modelled on a boundaryless complex model I is, with the same charts, a real C^n manifold modelled on I.restrictScalars ℝ. Available after open scoped TauCeti.ComplexManifold.