Documentation

TauCeti.Geometry.Manifold.ModelWithCorners.RestrictScalars.Basic

Restricting scalars in boundaryless models #

A boundaryless model can be regarded over a smaller scalar field without changing its coordinate maps or the carrier of its charts. This operation commutes with products, so the product comparison requires no new atlas.

The construction uses Mathlib's ModelWithCorners.ofTargetUniv; no scalar structure is replaced on the model vector space.

For the underlying real model of a complex manifold, see Huybrechts, Complex Geometry, Chapter 1, and Kobayashi--Nomizu, Foundations of Differential Geometry, Volume I, Chapter I.

source
def ModelWithCorners.restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] :
ModelWithCorners 𝕜 E H

Regard a boundaryless model over another scalar field, preserving both coordinate maps and the caller's normed-space structure.

Instances For
    source
    @[simp]
    theorem ModelWithCorners.restrictScalars_toPartialEquiv (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] :
    (restrictScalars 𝕜 I).toPartialEquiv = I.toPartialEquiv

    Restriction of scalars preserves the entire coordinate partial equivalence.

    source
    @[simp]
    theorem ModelWithCorners.coe_restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] :
    ↑(restrictScalars 𝕜 I) = ↑I
    source
    @[simp]
    theorem ModelWithCorners.coe_restrictScalars_symm (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] :
    ↑(restrictScalars 𝕜 I).symm = ↑I.symm
    source
    instance ModelWithCorners.instBoundarylessRestrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] :
    (restrictScalars 𝕜 I).Boundaryless

    Restricting scalars does not introduce a boundary.

    source
    @[simp]
    theorem modelWithCornersSelf_restrictScalars (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] :
    ModelWithCorners.restrictScalars 𝕜 (modelWithCornersSelf 𝕜' E) = modelWithCornersSelf 𝕜 E

    The trivial model restricts to the trivial model for the caller's scalar action.

    source
    @[simp]
    theorem ModelWithCorners.restrictScalars_prod (𝕜 : Type u_1) {𝕜' : Type u_2} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜'] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E] {H : Type u_4} [TopologicalSpace H] (I : ModelWithCorners 𝕜' E H) [I.Boundaryless] {F : Type u_5} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F] {H' : Type u_6} [TopologicalSpace H'] (J : ModelWithCorners 𝕜' F H') [J.Boundaryless] :
    restrictScalars 𝕜 (I.prod J) = (restrictScalars 𝕜 I).prod (restrictScalars 𝕜 J)

    Restricting scalars commutes with the ordinary product model.