Diffeomorphisms #
This file implements diffeomorphisms.
Definitions #
Diffeomorph I I' M M' n
:n
-times continuously differentiable diffeomorphism betweenM
andM'
with respect to I and I'; we do not introduce a separate definition for the casen = ∞
; we use notation instead.Diffeomorph.toHomeomorph
: reinterpret a diffeomorphism as a homeomorphism.ContinuousLinearEquiv.toDiffeomorph
: reinterpret a continuous equivalence as a diffeomorphism.ModelWithCorners.transDiffeomorph
: compose a givenModelWithCorners
with a diffeomorphism between the old and the new target spaces. Useful, e.g, to turn any finite dimensional manifold into a manifold modelled on a Euclidean space.Diffeomorph.toTransDiffeomorph
: the identity diffeomorphism betweenM
with modelI
andM
with modelI.trans_diffeomorph e
.
Notations #
M ≃ₘ^n⟮I, I'⟯ M'
:=Diffeomorph I J M N n
M ≃ₘ⟮I, I'⟯ M'
:=Diffeomorph I J M N ⊤
E ≃ₘ^n[𝕜] E'
:=E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
E ≃ₘ[𝕜] E'
:=E ≃ₘ⟮𝓘(𝕜, E), 𝓘(𝕜, E')⟯ E'
Implementation notes #
This notion of diffeomorphism is needed although there is already a notion of structomorphism
because structomorphisms do not allow the model spaces H
and H'
of the two manifolds to be
different, i.e. for a structomorphism one has to impose H = H'
which is often not the case in
practice.
Keywords #
diffeomorphism, manifold
- toFun : M → M'
- invFun : M' → M
- left_inv : Function.LeftInverse s.invFun s.toFun
- right_inv : Function.RightInverse s.invFun s.toFun
- contMDiff_toFun : ContMDiff I I' n ↑s.toEquiv
- contMDiff_invFun : ContMDiff I' I n ↑s.symm
n
-times continuously differentiable diffeomorphism between M
and M'
with respect to I and I'
Instances For
Interpret a diffeomorphism as a ContMDiffMap
.
Instances For
Coercion to function λ h : M ≃ₘ^n⟮I, I'⟯ M', (h : M → M')
is injective.
Identity map as a diffeomorphism.
Instances For
Composition of two diffeomorphisms.
Instances For
Inverse of a diffeomorphism.
Instances For
A diffeomorphism is a homeomorphism.
Instances For
Product of two diffeomorphisms.
Instances For
M × N
is diffeomorphic to N × M
.
Instances For
(M × N) × N'
is diffeomorphic to M × (N × N')
.
Instances For
A continuous linear equivalence between normed spaces is a diffeomorphism.
Instances For
Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.
Instances For
The identity diffeomorphism between a manifold with model I
and the same manifold
with model I.trans_diffeomorph e
.