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
n
-times continuously differentiable diffeomorphism between M
and M'
with respect to I
and I'
.
- toFun : M → M'
- invFun : M' → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- contMDiff_toFun : ContMDiff I I' n ⇑self.toEquiv
- contMDiff_invFun : ContMDiff I' I n ⇑self.symm
Instances For
n
-times continuously differentiable diffeomorphism between M
and M'
with respect to I
and I'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Infinitely differentiable diffeomorphism between M
and M'
with respect to I
and I'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
n
-times continuously differentiable diffeomorphism between E
and E'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Infinitely differentiable diffeomorphism between E
and E'
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Diffeomorph.instEquivLike = { coe := fun (Φ : Diffeomorph I I' M M' n) => ⇑Φ.toEquiv, inv := fun (Φ : Diffeomorph I I' M M' n) => ⇑Φ.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
Interpret a diffeomorphism as a ContMDiffMap
.
Equations
- ↑Φ = ⟨⇑Φ, ⋯⟩
Instances For
Equations
- Diffeomorph.instCoeContMDiffMap = { coe := Diffeomorph.toContMDiffMap }
Coercion to function fun h : M ≃ₘ^n⟮I, I'⟯ M' ↦ (h : M → M')
is injective.
Equations
- ⋯ = ⋯
Identity map as a diffeomorphism.
Equations
- Diffeomorph.refl I M n = { toEquiv := Equiv.refl M, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
Composition of two diffeomorphisms.
Equations
- h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
Inverse of a diffeomorphism.
Equations
- h.symm = { toEquiv := h.symm, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
A diffeomorphism is a homeomorphism.
Equations
- h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Product of two diffeomorphisms.
Equations
- h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
M × N
is diffeomorphic to N × M
.
Equations
- Diffeomorph.prodComm I J M N n = { toEquiv := Equiv.prodComm M N, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
(M × N) × N'
is diffeomorphic to M × (N × N')
.
Equations
- Diffeomorph.prodAssoc I J J' M N N' n = { toEquiv := Equiv.prodAssoc M N N', contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
A continuous linear equivalence between normed spaces is a diffeomorphism.
Equations
- e.toDiffeomorph = { toEquiv := e.toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }
Instances For
Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.
Equations
- I.transDiffeomorph e = { toPartialEquiv := I.trans e.toPartialEquiv, source_eq := ⋯, uniqueDiffOn' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Equations
- ⋯ = ⋯
The identity diffeomorphism between a manifold with model I
and the same manifold
with model I.trans_diffeomorph e
.
Equations
- Diffeomorph.toTransDiffeomorph I M e = { toEquiv := Equiv.refl M, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }