Restricting the scalars of diffeomorphisms #
Let 𝕜' be a normed algebra over 𝕜, and let the model spaces be normed spaces over both fields,
compatibly. A C^n diffeomorphism for boundaryless models over 𝕜' is, with the same underlying
equivalence, a C^n diffeomorphism for their scalar restrictions over 𝕜, since a C^n map over
𝕜' is C^n over 𝕜 (ContMDiff.restrictScalars). This file bundles that diffeomorphism and
records its compatibility with the identity, inverses, and composition.
The main example is a biholomorphism between complex manifolds modelled on 𝓘(ℂ, E) and
𝓘(ℂ, E'), which is a diffeomorphism between the underlying real manifolds modelled on
𝓘(ℝ, E) and 𝓘(ℝ, E').
Main definitions #
Diffeomorph.restrictScalars: a diffeomorphism over𝕜'regarded as a diffeomorphism over𝕜.
Main results #
Diffeomorph.coe_restrictScalars: it has the same underlying map.Diffeomorph.restrictScalars_refl,Diffeomorph.restrictScalars_symm,Diffeomorph.restrictScalars_trans: restriction of scalars commutes with the identity, inverses, and composition.
def
Diffeomorph.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_6}
{H' : Type u_7}
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
[I.Boundaryless]
[I'.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I I' M N n)
:
Diffeomorph (ModelWithCorners.restrictScalars 𝕜 I) (ModelWithCorners.restrictScalars 𝕜 I') M N n
A C^n diffeomorphism for boundaryless models over 𝕜' is a C^n diffeomorphism for
their scalar restrictions to 𝕜, with the same underlying equivalence. For instance, a
biholomorphism between complex manifolds is a diffeomorphism of the underlying real manifolds.
Instances For
@[simp]
theorem
Diffeomorph.restrictScalars_toEquiv
(𝕜 : 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_6}
{H' : Type u_7}
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
[I.Boundaryless]
[I'.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I I' M N n)
:
Restricting the scalars of a diffeomorphism does not change its underlying equivalence.
@[simp]
theorem
Diffeomorph.coe_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_6}
{H' : Type u_7}
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
[I.Boundaryless]
[I'.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I I' M N n)
:
Restricting the scalars of a diffeomorphism does not change its underlying map.
@[simp]
theorem
Diffeomorph.restrictScalars_toHomeomorph
(𝕜 : 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_6}
{H' : Type u_7}
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
[I.Boundaryless]
[I'.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I I' M N n)
:
Restricting the scalars of a diffeomorphism does not change its underlying homeomorphism.
theorem
Diffeomorph.restrictScalars_injective
(𝕜 : 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_6}
{H' : Type u_7}
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
[I.Boundaryless]
[I'.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
:
Restricting the scalars of diffeomorphisms is injective.
@[simp]
theorem
Diffeomorph.restrictScalars_refl
(𝕜 : Type u_1)
{𝕜' : Type u_2}
[NontriviallyNormedField 𝕜]
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[NormedSpace 𝕜' E]
[IsScalarTower 𝕜 𝕜' E]
{H : Type u_6}
[TopologicalSpace H]
{I : ModelWithCorners 𝕜' E H}
[I.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{n : WithTop ℕ∞}
:
restrictScalars 𝕜 (Diffeomorph.refl I M n) = Diffeomorph.refl (ModelWithCorners.restrictScalars 𝕜 I) M n
Restricting the scalars of the identity diffeomorphism gives the identity diffeomorphism.
@[simp]
theorem
Diffeomorph.restrictScalars_symm
(𝕜 : 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_6}
{H' : Type u_7}
[TopologicalSpace H]
[TopologicalSpace H']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
[I.Boundaryless]
[I'.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I I' M N n)
:
Restricting scalars commutes with taking the inverse diffeomorphism.
@[simp]
theorem
Diffeomorph.restrictScalars_trans
(𝕜 : 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']
{F : Type u_5}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{H : Type u_6}
{H' : Type u_7}
{H'' : Type u_8}
[TopologicalSpace H]
[TopologicalSpace H']
[TopologicalSpace H'']
{I : ModelWithCorners 𝕜' E H}
{I' : ModelWithCorners 𝕜' E' H'}
{J : ModelWithCorners 𝕜' F H''}
[I.Boundaryless]
[I'.Boundaryless]
[J.Boundaryless]
{M : Type u_9}
[TopologicalSpace M]
[ChartedSpace H M]
{N : Type u_10}
[TopologicalSpace N]
[ChartedSpace H' N]
{P : Type u_11}
[TopologicalSpace P]
[ChartedSpace H'' P]
{n : WithTop ℕ∞}
(Φ : Diffeomorph I I' M N n)
(Ψ : Diffeomorph I' J N P n)
:
Restricting scalars commutes with the composition of diffeomorphisms.