# Diffeomorphisms #

This file implements diffeomorphisms.

## Definitions #

• Diffeomorph I I' M M' n: n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'; we do not introduce a separate definition for the case n = ∞; 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 given ModelWithCorners 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 between M with model I and M with model I.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

structure Diffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] (I : ) (I' : ModelWithCorners 𝕜 E' H') (M : Type u_9) [] [] (M' : Type u_10) [] [ChartedSpace H' M'] (n : ℕ∞) extends :
Type (max u_10 u_9)

n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'.

Instances For
theorem Diffeomorph.contMDiff_toFun {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (self : Diffeomorph I I' M M' n) :
ContMDiff I I' n self.toEquiv
theorem Diffeomorph.contMDiff_invFun {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (self : Diffeomorph I I' M M' n) :
ContMDiff I' I n self.symm

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
theorem Diffeomorph.toEquiv_injective {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} :
Function.Injective Diffeomorph.toEquiv
instance Diffeomorph.instEquivLike {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} :
EquivLike (Diffeomorph I I' M M' n) M M'
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' := }
def Diffeomorph.toContMDiffMap {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (Φ : Diffeomorph I I' M M' n) :
ContMDiffMap I I' M M' n

Interpret a diffeomorphism as a ContMDiffMap.

Equations
• Φ = Φ,
Instances For
instance Diffeomorph.instCoeContMDiffMap {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} :
Coe (Diffeomorph I I' M M' n) (ContMDiffMap I I' M M' n)
Equations
• Diffeomorph.instCoeContMDiffMap = { coe := Diffeomorph.toContMDiffMap }
theorem Diffeomorph.continuous {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
theorem Diffeomorph.contMDiff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
ContMDiff I I' n h
theorem Diffeomorph.contMDiffAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) {x : M} :
ContMDiffAt I I' n (h) x
theorem Diffeomorph.contMDiffWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) {s : Set M} {x : M} :
ContMDiffWithinAt I I' n (h) s x
theorem Diffeomorph.contDiff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {n : ℕ∞} (h : Diffeomorph () () E E' n) :
ContDiff 𝕜 n h
theorem Diffeomorph.smooth {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] (h : Diffeomorph I I' M M' ) :
Smooth I I' h
theorem Diffeomorph.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) (hn : 1 n) :
MDifferentiable I I' h
theorem Diffeomorph.mdifferentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) (s : Set M) (hn : 1 n) :
MDifferentiableOn I I' (h) s
@[simp]
theorem Diffeomorph.coe_toEquiv {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
h.toEquiv = h
@[simp]
theorem Diffeomorph.coe_coe {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
h = h
@[simp]
theorem Diffeomorph.toEquiv_inj {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} {h : Diffeomorph I I' M M' n} {h' : Diffeomorph I I' M M' n} :
h.toEquiv = h'.toEquiv h = h'
theorem Diffeomorph.coeFn_injective {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} :
Function.Injective DFunLike.coe

Coercion to function fun h : M ≃ₘ^n⟮I, I'⟯ M' ↦ (h : M → M') is injective.

theorem Diffeomorph.ext {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} {h : Diffeomorph I I' M M' n} {h' : Diffeomorph I I' M M' n} (Heq : ∀ (x : M), h x = h' x) :
h = h'
instance Diffeomorph.instContinuousMapClassTopENat {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] :
Equations
• =
def Diffeomorph.refl {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_5} [] (I : ) (M : Type u_9) [] [] (n : ℕ∞) :
Diffeomorph I I M M n

Identity map as a diffeomorphism.

Equations
• = { toEquiv := , contMDiff_toFun := , contMDiff_invFun := }
Instances For
@[simp]
theorem Diffeomorph.refl_toEquiv {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_5} [] (I : ) (M : Type u_9) [] [] (n : ℕ∞) :
().toEquiv =
@[simp]
theorem Diffeomorph.coe_refl {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_5} [] (I : ) (M : Type u_9) [] [] (n : ℕ∞) :
() = id
def Diffeomorph.trans {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
Diffeomorph I J M N n

Composition of two diffeomorphisms.

Equations
• h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, contMDiff_toFun := , contMDiff_invFun := }
Instances For
@[simp]
theorem Diffeomorph.trans_refl {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
h.trans (Diffeomorph.refl I' M' n) = h
@[simp]
theorem Diffeomorph.refl_trans {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (h : Diffeomorph I I' M M' n) :
().trans h = h
@[simp]
theorem Diffeomorph.coe_trans {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
(h₁.trans h₂) = h₂ h₁
def Diffeomorph.symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
Diffeomorph J I N M n

Inverse of a diffeomorphism.

Equations
• h.symm = { toEquiv := h.symm, contMDiff_toFun := , contMDiff_invFun := }
Instances For
@[simp]
theorem Diffeomorph.apply_symm_apply {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (x : N) :
h (h.symm x) = x
@[simp]
theorem Diffeomorph.symm_apply_apply {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (x : M) :
h.symm (h x) = x
@[simp]
theorem Diffeomorph.symm_refl {𝕜 : Type u_1} {E : Type u_2} [] {H : Type u_5} [] {I : } {M : Type u_9} [] [] {n : ℕ∞} :
().symm =
@[simp]
theorem Diffeomorph.self_trans_symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.trans h.symm =
@[simp]
theorem Diffeomorph.symm_trans_self {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.symm.trans h =
@[simp]
theorem Diffeomorph.symm_trans' {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph I' J M' N n) :
(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
@[simp]
theorem Diffeomorph.symm_toEquiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.symm.toEquiv = h.symm
@[simp]
theorem Diffeomorph.toEquiv_coe_symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.symm = h.symm
theorem Diffeomorph.image_eq_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (s : Set M) :
h '' s = h.symm ⁻¹' s
theorem Diffeomorph.symm_image_eq_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (s : Set N) :
h.symm '' s = h ⁻¹' s
@[simp]
theorem Diffeomorph.range_comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} {α : Sort u_13} (h : Diffeomorph I J M N n) (f : αM) :
Set.range (h f) = h.symm ⁻¹'
@[simp]
theorem Diffeomorph.image_symm_image {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (s : Set N) :
h '' (h.symm '' s) = s
@[simp]
theorem Diffeomorph.symm_image_image {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (s : Set M) :
h.symm '' (h '' s) = s
def Diffeomorph.toHomeomorph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
M ≃ₜ N

A diffeomorphism is a homeomorphism.

Equations
• h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem Diffeomorph.toHomeomorph_toEquiv {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.toHomeomorph.toEquiv = h.toEquiv
@[simp]
theorem Diffeomorph.symm_toHomeomorph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.symm.toHomeomorph = h.toHomeomorph.symm
@[simp]
theorem Diffeomorph.coe_toHomeomorph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.toHomeomorph = h
@[simp]
theorem Diffeomorph.coe_toHomeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) :
h.toHomeomorph.symm = h.symm
@[simp]
theorem Diffeomorph.contMDiffWithinAt_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : NM'} {s : Set M} {x : M} (hm : m n) :
ContMDiffWithinAt I I' m (f h) s x ContMDiffWithinAt J I' m f (h.symm ⁻¹' s) (h x)
@[simp]
theorem Diffeomorph.contMDiffOn_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : NM'} {s : Set M} (hm : m n) :
ContMDiffOn I I' m (f h) s ContMDiffOn J I' m f (h.symm ⁻¹' s)
@[simp]
theorem Diffeomorph.contMDiffAt_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : NM'} {x : M} (hm : m n) :
ContMDiffAt I I' m (f h) x ContMDiffAt J I' m f (h x)
@[simp]
theorem Diffeomorph.contMDiff_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : NM'} (hm : m n) :
ContMDiff I I' m (f h) ContMDiff J I' m f
@[simp]
theorem Diffeomorph.contMDiffWithinAt_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) {s : Set M'} {x : M'} :
ContMDiffWithinAt I' J m (h f) s x ContMDiffWithinAt I' I m f s x
@[simp]
theorem Diffeomorph.contMDiffAt_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) {x : M'} :
ContMDiffAt I' J m (h f) x ContMDiffAt I' I m f x
@[simp]
theorem Diffeomorph.contMDiffOn_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) {s : Set M'} :
ContMDiffOn I' J m (h f) s ContMDiffOn I' I m f s
@[simp]
theorem Diffeomorph.contMDiff_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {n : ℕ∞} {m : ℕ∞} (h : Diffeomorph I J M N n) {f : M'M} (hm : m n) :
ContMDiff I' J m (h f) ContMDiff I' I m f
theorem Diffeomorph.toPartialHomeomorph_mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (hn : 1 n) :
PartialHomeomorph.MDifferentiable I J h.toHomeomorph.toPartialHomeomorph
def Diffeomorph.prodCongr {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {G' : Type u_8} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {N' : Type u_12} [] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
Diffeomorph (I.prod J) (I'.prod J') (M × N) (M' × N') n

Product of two diffeomorphisms.

Equations
• h₁.prodCongr h₂ = { toEquiv := h₁.prodCongr h₂.toEquiv, contMDiff_toFun := , contMDiff_invFun := }
Instances For
@[simp]
theorem Diffeomorph.prodCongr_symm {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {G' : Type u_8} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {N' : Type u_12} [] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
(h₁.prodCongr h₂).symm = h₁.symm.prodCongr h₂.symm
@[simp]
theorem Diffeomorph.coe_prodCongr {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {G : Type u_7} [] {G' : Type u_8} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {J : } {J' : ModelWithCorners 𝕜 F G'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {N : Type u_11} [] [] {N' : Type u_12} [] [ChartedSpace G' N'] {n : ℕ∞} (h₁ : Diffeomorph I I' M M' n) (h₂ : Diffeomorph J J' N N' n) :
(h₁.prodCongr h₂) = Prod.map h₁ h₂
def Diffeomorph.prodComm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] (I : ) (J : ) (M : Type u_9) [] [] (N : Type u_11) [] [] (n : ℕ∞) :
Diffeomorph (I.prod J) (J.prod I) (M × N) (N × M) n

M × N is diffeomorphic to N × M.

Equations
Instances For
@[simp]
theorem Diffeomorph.prodComm_symm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] (I : ) (J : ) (M : Type u_9) [] [] (N : Type u_11) [] [] (n : ℕ∞) :
(Diffeomorph.prodComm I J M N n).symm = Diffeomorph.prodComm J I N M n
@[simp]
theorem Diffeomorph.coe_prodComm {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] (I : ) (J : ) (M : Type u_9) [] [] (N : Type u_11) [] [] (n : ℕ∞) :
(Diffeomorph.prodComm I J M N n) = Prod.swap
def Diffeomorph.prodAssoc {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {G' : Type u_8} [] (I : ) (J : ) (J' : ModelWithCorners 𝕜 F G') (M : Type u_9) [] [] (N : Type u_11) [] [] (N' : Type u_12) [] [ChartedSpace G' N'] (n : ℕ∞) :
Diffeomorph ((I.prod J).prod J') (I.prod (J.prod J')) ((M × N) × N') (M × N × N') n

(M × N) × N' is diffeomorphic to M × (N × N').

Equations
Instances For
theorem Diffeomorph.uniqueMDiffOn_image_aux {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (hn : 1 n) {s : Set M} (hs : ) :
UniqueMDiffOn J (h '' s)
@[simp]
theorem Diffeomorph.uniqueMDiffOn_image {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (hn : 1 n) {s : Set M} :
UniqueMDiffOn J (h '' s)
@[simp]
theorem Diffeomorph.uniqueMDiffOn_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {G : Type u_7} [] {I : } {J : } {M : Type u_9} [] [] {N : Type u_11} [] [] {n : ℕ∞} (h : Diffeomorph I J M N n) (hn : 1 n) {s : Set N} :
@[simp]
theorem Diffeomorph.uniqueDiffOn_image {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {n : ℕ∞} (h : Diffeomorph () () E F n) (hn : 1 n) {s : Set E} :
UniqueDiffOn 𝕜 (h '' s)
@[simp]
theorem Diffeomorph.uniqueDiffOn_preimage {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {n : ℕ∞} (h : Diffeomorph () () E F n) (hn : 1 n) {s : Set F} :
UniqueDiffOn 𝕜 (h ⁻¹' s)
def ContinuousLinearEquiv.toDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
Diffeomorph () () E E'

A continuous linear equivalence between normed spaces is a diffeomorphism.

Equations
• e.toDiffeomorph = { toEquiv := e.toEquiv, contMDiff_toFun := , contMDiff_invFun := }
Instances For
@[simp]
theorem ContinuousLinearEquiv.coe_toDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
e.toDiffeomorph = e
@[simp]
theorem ContinuousLinearEquiv.symm_toDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
e.symm.toDiffeomorph = e.toDiffeomorph.symm
@[simp]
theorem ContinuousLinearEquiv.coe_toDiffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] (e : E ≃L[𝕜] E') :
e.toDiffeomorph.symm = e.symm
def ModelWithCorners.transDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) (e : Diffeomorph () () E E' ) :

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 := , unique_diff' := , continuous_toFun := , continuous_invFun := }
Instances For
@[simp]
theorem ModelWithCorners.coe_transDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) (e : Diffeomorph () () E E' ) :
(I.transDiffeomorph e) = e I
@[simp]
theorem ModelWithCorners.coe_transDiffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) (e : Diffeomorph () () E E' ) :
(I.transDiffeomorph e).symm = I.symm e.symm
theorem ModelWithCorners.transDiffeomorph_range {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) (e : Diffeomorph () () E E' ) :
Set.range (I.transDiffeomorph e) = e ''
theorem ModelWithCorners.coe_extChartAt_transDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) {M : Type u_9} [] [] (e : Diffeomorph () () E E' ) (x : M) :
(extChartAt (I.transDiffeomorph e) x) = e ()
theorem ModelWithCorners.coe_extChartAt_transDiffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) {M : Type u_9} [] [] (e : Diffeomorph () () E E' ) (x : M) :
(extChartAt (I.transDiffeomorph e) x).symm = ().symm e.symm
theorem ModelWithCorners.extChartAt_transDiffeomorph_target {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {H : Type u_5} [] (I : ) {M : Type u_9} [] [] (e : Diffeomorph () () E E' ) (x : M) :
(extChartAt (I.transDiffeomorph e) x).target = e.symm ⁻¹' ().target
instance Diffeomorph.smoothManifoldWithCorners_transDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] {I : } {M : Type u_9} [] [] (e : Diffeomorph () () E F ) :
SmoothManifoldWithCorners (I.transDiffeomorph e) M
Equations
• =
def Diffeomorph.toTransDiffeomorph {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_4} [] {H : Type u_5} [] (I : ) (M : Type u_9) [] [] (e : Diffeomorph () () E F ) :
Diffeomorph I (I.transDiffeomorph e) M M

The identity diffeomorphism between a manifold with model I and the same manifold with model I.trans_diffeomorph e.

Equations
• = { toEquiv := , contMDiff_toFun := , contMDiff_invFun := }
Instances For
@[simp]
theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : M'M} {x : M'} {s : Set M'} :
ContMDiffWithinAt I' (I.transDiffeomorph e) n f s x ContMDiffWithinAt I' I n f s x
@[simp]
theorem Diffeomorph.contMDiffAt_transDiffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : M'M} {x : M'} :
ContMDiffAt I' (I.transDiffeomorph e) n f x ContMDiffAt I' I n f x
@[simp]
theorem Diffeomorph.contMDiffOn_transDiffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : M'M} {s : Set M'} :
ContMDiffOn I' (I.transDiffeomorph e) n f s ContMDiffOn I' I n f s
@[simp]
theorem Diffeomorph.contMDiff_transDiffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : M'M} :
ContMDiff I' (I.transDiffeomorph e) n f ContMDiff I' I n f
theorem Diffeomorph.smooth_transDiffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] (e : Diffeomorph () () E F ) {f : M'M} :
Smooth I' (I.transDiffeomorph e) f Smooth I' I f
@[simp]
theorem Diffeomorph.contMDiffWithinAt_transDiffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : MM'} {x : M} {s : Set M} :
ContMDiffWithinAt (I.transDiffeomorph e) I' n f s x ContMDiffWithinAt I I' n f s x
@[simp]
theorem Diffeomorph.contMDiffAt_transDiffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : MM'} {x : M} :
ContMDiffAt (I.transDiffeomorph e) I' n f x ContMDiffAt I I' n f x
@[simp]
theorem Diffeomorph.contMDiffOn_transDiffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : MM'} {s : Set M} :
ContMDiffOn (I.transDiffeomorph e) I' n f s ContMDiffOn I I' n f s
@[simp]
theorem Diffeomorph.contMDiff_transDiffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] {n : ℕ∞} (e : Diffeomorph () () E F ) {f : MM'} :
ContMDiff (I.transDiffeomorph e) I' n f ContMDiff I I' n f
theorem Diffeomorph.smooth_transDiffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [] {E' : Type u_3} [] [NormedSpace 𝕜 E'] {F : Type u_4} [] {H : Type u_5} [] {H' : Type u_6} [] {I : } {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [] [] {M' : Type u_10} [] [ChartedSpace H' M'] (e : Diffeomorph () () E F ) {f : MM'} :
Smooth (I.transDiffeomorph e) I' f Smooth I I' f