# mathlib3documentation

geometry.manifold.diffeomorph

# Diffeomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.to_homeomorph`: reinterpret a diffeomorphism as a homeomorphism.
• `continuous_linear_equiv.to_diffeomorph`: reinterpret a continuous equivalence as a diffeomorphism.
• `model_with_corners.trans_diffeomorph`: compose a given `model_with_corners` 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.to_trans_diffeomorph`: 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

@[nolint]
structure diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_9) [ M] (M' : Type u_10) [ M'] (n : ℕ∞) :
Type (max u_10 u_9)

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

Instances for `diffeomorph`
@[protected, instance]
def diffeomorph.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} :
has_coe_to_fun I' M M' n) (λ (_x : I' M M' n), M M')
Equations
@[protected, instance]
def diffeomorph.cont_mdiff_map.has_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} :
has_coe I' M M' n) I' M M' n)
Equations
@[protected, continuity]
theorem diffeomorph.continuous {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) :
@[protected]
theorem diffeomorph.cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) :
I' n h
@[protected]
theorem diffeomorph.cont_mdiff_at {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) {x : M} :
I' n h x
@[protected]
theorem diffeomorph.cont_mdiff_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) {s : set M} {x : M} :
n h s x
@[protected]
theorem diffeomorph.cont_diff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {n : ℕ∞} (h : E E' n) :
n h
@[protected]
theorem diffeomorph.smooth {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] (h : I' M M' ) :
I' h
@[protected]
theorem diffeomorph.mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) (hn : 1 n) :
I' h
@[protected]
theorem diffeomorph.mdifferentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) (s : set M) (hn : 1 n) :
h s
@[simp]
theorem diffeomorph.coe_to_equiv {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) :
@[simp, norm_cast]
theorem diffeomorph.coe_coe {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) :
theorem diffeomorph.to_equiv_injective {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} :
@[simp]
theorem diffeomorph.to_equiv_inj {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} {h h' : I' M M' n} :
h.to_equiv = h'.to_equiv h = h'
theorem diffeomorph.coe_fn_injective {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} :
function.injective (λ (h : I' M M' n) (x : M), h x)

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

@[ext]
theorem diffeomorph.ext {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} {h h' : I' M M' n} (Heq : (x : M), h x = h' x) :
h = h'
@[protected, instance]
def diffeomorph.continuous_map_class {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] :
Equations
@[protected]
def diffeomorph.refl {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_5} (I : H) (M : Type u_9) [ M] (n : ℕ∞) :
I M M n

Identity map as a diffeomorphism.

Equations
@[simp]
theorem diffeomorph.refl_to_equiv {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_5} (I : H) (M : Type u_9) [ M] (n : ℕ∞) :
M n).to_equiv =
@[simp]
theorem diffeomorph.coe_refl {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_5} (I : H) (M : Type u_9) [ M] (n : ℕ∞) :
M n) = id
@[protected]
def diffeomorph.trans {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n : ℕ∞} (h₁ : I' M M' n) (h₂ : J M' N n) :
J M N n

Composition of two diffeomorphisms.

Equations
@[simp]
theorem diffeomorph.trans_refl {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) :
h.trans M' n) = h
@[simp]
theorem diffeomorph.refl_trans {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (h : I' M M' n) :
M n).trans h = h
@[simp]
theorem diffeomorph.coe_trans {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n : ℕ∞} (h₁ : I' M M' n) (h₂ : J M' N n) :
(h₁.trans h₂) = h₂ h₁
@[protected]
def diffeomorph.symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
I N M n

Inverse of a diffeomorphism.

Equations
@[simp]
theorem diffeomorph.apply_symm_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (x : N) :
h ((h.symm) x) = x
@[simp]
theorem diffeomorph.symm_apply_apply {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (x : M) :
(h.symm) (h x) = x
@[simp]
theorem diffeomorph.symm_refl {𝕜 : Type u_1} {E : Type u_2} [ E] {H : Type u_5} {I : H} {M : Type u_9} [ M] {n : ℕ∞} :
M n).symm = n
@[simp]
theorem diffeomorph.self_trans_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
h.trans h.symm = n
@[simp]
theorem diffeomorph.symm_trans_self {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
h.symm.trans h = n
@[simp]
theorem diffeomorph.symm_trans' {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n : ℕ∞} (h₁ : I' M M' n) (h₂ : J M' N n) :
(h₁.trans h₂).symm = h₂.symm.trans h₁.symm
@[simp]
theorem diffeomorph.symm_to_equiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
@[simp]
theorem diffeomorph.to_equiv_coe_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
theorem diffeomorph.image_eq_preimage {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : 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} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (s : set N) :
(h.symm) '' s = h ⁻¹' s
@[simp]
theorem diffeomorph.range_comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} {α : Sort u_3} (h : J M N n) (f : α M) :
@[simp]
theorem diffeomorph.image_symm_image {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : 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} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (s : set M) :
(h.symm) '' (h '' s) = s
def diffeomorph.to_homeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
M ≃ₜ N

A diffeomorphism is a homeomorphism.

Equations
@[simp]
theorem diffeomorph.to_homeomorph_to_equiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
@[simp]
theorem diffeomorph.symm_to_homeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
@[simp]
theorem diffeomorph.coe_to_homeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
@[simp]
theorem diffeomorph.coe_to_homeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) :
@[simp]
theorem diffeomorph.cont_mdiff_within_at_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : N M'} {s : set M} {x : M} (hm : m n) :
m (f h) s x m f ((h.symm) ⁻¹' s) (h x)
@[simp]
theorem diffeomorph.cont_mdiff_on_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : N M'} {s : set M} (hm : m n) :
I' m (f h) s I' m f ((h.symm) ⁻¹' s)
@[simp]
theorem diffeomorph.cont_mdiff_at_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : N M'} {x : M} (hm : m n) :
I' m (f h) x I' m f (h x)
@[simp]
theorem diffeomorph.cont_mdiff_comp_diffeomorph_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : N M'} (hm : m n) :
I' m (f h) I' m f
@[simp]
theorem diffeomorph.cont_mdiff_within_at_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : M' M} (hm : m n) {s : set M'} {x : M'} :
m (h f) s x m f s x
@[simp]
theorem diffeomorph.cont_mdiff_at_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : M' M} (hm : m n) {x : M'} :
J m (h f) x I m f x
@[simp]
theorem diffeomorph.cont_mdiff_on_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : M' M} (hm : m n) {s : set M'} :
J m (h f) s I m f s
@[simp]
theorem diffeomorph.cont_mdiff_diffeomorph_comp_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {I : H} {I' : H'} {J : G} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {n m : ℕ∞} (h : J M N n) {f : M' M} (hm : m n) :
J m (h f) I m f
theorem diffeomorph.to_local_homeomorph_mdifferentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (hn : 1 n) :
def diffeomorph.prod_congr {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {G' : Type u_8} {I : H} {I' : H'} {J : G} {J' : G'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {N' : Type u_12} [ N'] {n : ℕ∞} (h₁ : I' M M' n) (h₂ : J' N N' n) :
diffeomorph (I.prod J) (I'.prod J') (M × N) (M' × N') n

Product of two diffeomorphisms.

Equations
@[simp]
theorem diffeomorph.prod_congr_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {G' : Type u_8} {I : H} {I' : H'} {J : G} {J' : G'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {N' : Type u_12} [ N'] {n : ℕ∞} (h₁ : I' M M' n) (h₂ : J' N N' n) :
(h₁.prod_congr h₂).symm = h₁.symm.prod_congr h₂.symm
@[simp]
theorem diffeomorph.coe_prod_congr {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} {G' : Type u_8} {I : H} {I' : H'} {J : G} {J' : G'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {N : Type u_11} [ N] {N' : Type u_12} [ N'] {n : ℕ∞} (h₁ : I' M M' n) (h₂ : J' N N' n) :
(h₁.prod_congr h₂) = h₂
def diffeomorph.prod_comm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} (I : H) (J : G) (M : Type u_9) [ M] (N : Type u_11) [ N] (n : ℕ∞) :
diffeomorph (I.prod J) (J.prod I) (M × N) (N × M) n

`M × N` is diffeomorphic to `N × M`.

Equations
@[simp]
theorem diffeomorph.prod_comm_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} (I : H) (J : G) (M : Type u_9) [ M] (N : Type u_11) [ N] (n : ℕ∞) :
M N n).symm = M n
@[simp]
theorem diffeomorph.coe_prod_comm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} (I : H) (J : G) (M : Type u_9) [ M] (N : Type u_11) [ N] (n : ℕ∞) :
M N n) = prod.swap
def diffeomorph.prod_assoc {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {G' : Type u_8} (I : H) (J : G) (J' : G') (M : Type u_9) [ M] (N : Type u_11) [ N] (N' : Type u_12) [ 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
theorem diffeomorph.unique_mdiff_on_image_aux {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (hn : 1 n) {s : set M} (hs : s) :
(h '' s)
@[simp]
theorem diffeomorph.unique_mdiff_on_image {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (hn : 1 n) {s : set M} :
(h '' s)
@[simp]
theorem diffeomorph.unique_mdiff_on_preimage {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {G : Type u_7} {I : H} {J : G} {M : Type u_9} [ M] {N : Type u_11} [ N] {n : ℕ∞} (h : J M N n) (hn : 1 n) {s : set N} :
(h ⁻¹' s)
@[simp]
theorem diffeomorph.unique_diff_on_image {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {n : ℕ∞} (h : E F n) (hn : 1 n) {s : set E} :
(h '' s)
@[simp]
theorem diffeomorph.unique_diff_on_preimage {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {n : ℕ∞} (h : E F n) (hn : 1 n) {s : set F} :
(h ⁻¹' s)
def continuous_linear_equiv.to_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] (e : E ≃L[𝕜] E') :
E E'

A continuous linear equivalence between normed spaces is a diffeomorphism.

Equations
@[simp]
theorem continuous_linear_equiv.coe_to_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] (e : E ≃L[𝕜] E') :
@[simp]
theorem continuous_linear_equiv.symm_to_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] (e : E ≃L[𝕜] E') :
@[simp]
theorem continuous_linear_equiv.coe_to_diffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] (e : E ≃L[𝕜] E') :
def model_with_corners.trans_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) (e : E E' ) :
H

Apply a diffeomorphism (e.g., a continuous linear equivalence) to the model vector space.

Equations
Instances for `model_with_corners.trans_diffeomorph`
@[simp]
theorem model_with_corners.coe_trans_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) (e : E E' ) :
@[simp]
theorem model_with_corners.coe_trans_diffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) (e : E E' ) :
theorem model_with_corners.trans_diffeomorph_range {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) (e : E E' ) :
=
theorem model_with_corners.coe_ext_chart_at_trans_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) {M : Type u_9} [ M] (e : E E' ) (x : M) :
x) = e x)
theorem model_with_corners.coe_ext_chart_at_trans_diffeomorph_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) {M : Type u_9} [ M] (e : E E' ) (x : M) :
theorem model_with_corners.ext_chart_at_trans_diffeomorph_target {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {H : Type u_5} (I : H) {M : Type u_9} [ M] (e : E E' ) (x : M) :
@[protected, instance]
def diffeomorph.smooth_manifold_with_corners_trans_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} {I : H} {M : Type u_9} [ M] (e : E F )  :
def diffeomorph.to_trans_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_4} [ F] {H : Type u_5} (I : H) (M : Type u_9) [ M] (e : E F ) :

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

Equations
@[simp]
theorem diffeomorph.cont_mdiff_within_at_trans_diffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M' M} {x : M'} {s : set M'} :
n f s x n f s x
@[simp]
theorem diffeomorph.cont_mdiff_at_trans_diffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M' M} {x : M'} :
(I.trans_diffeomorph e) n f x I n f x
@[simp]
theorem diffeomorph.cont_mdiff_on_trans_diffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M' M} {s : set M'} :
(I.trans_diffeomorph e) n f s I n f s
@[simp]
theorem diffeomorph.cont_mdiff_trans_diffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M' M} :
(I.trans_diffeomorph e) n f I n f
@[simp]
theorem diffeomorph.smooth_trans_diffeomorph_right {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] (e : E F ) {f : M' M} :
@[simp]
theorem diffeomorph.cont_mdiff_within_at_trans_diffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M M'} {x : M} {s : set M} :
n f s x n f s x
@[simp]
theorem diffeomorph.cont_mdiff_at_trans_diffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M M'} {x : M} :
I' n f x I' n f x
@[simp]
theorem diffeomorph.cont_mdiff_on_trans_diffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M M'} {s : set M} :
I' n f s I' n f s
@[simp]
theorem diffeomorph.cont_mdiff_trans_diffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] {n : ℕ∞} (e : E F ) {f : M M'} :
I' n f I' n f
@[simp]
theorem diffeomorph.smooth_trans_diffeomorph_left {𝕜 : Type u_1} {E : Type u_2} [ E] {E' : Type u_3} [ E'] {F : Type u_4} [ F] {H : Type u_5} {H' : Type u_6} {I : H} {I' : H'} {M : Type u_9} [ M] {M' : Type u_10} [ M'] (e : E F ) {f : M M'} :
smooth (I.trans_diffeomorph e) I' f I' f