# mathlibdocumentation

geometry.manifold.diffeomorph

# Diffeomorphisms

This file implements diffeomorphisms.

## Definitions

• times_diffeomorph I I' M M' n: n-times continuously differentiable diffeomorphism between M and M' with respect to I and I'
• diffeomorph I I' M M' : smooth diffeomorphism between M and M' with respect to I and I'

## Notations

• M ≃ₘ^n⟮I, I'⟯ M' := times_diffeomorph I J M N n
• M ≃ₘ⟮I, I'⟯ M' := times_diffeomorph I J M N ⊤

## 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.

@[nolint]
structure times_diffeomorph {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (n : with_top ) :
Type (max u_8 u_9)

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

def diffeomorph {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] :
Type (max u_8 u_9)

A diffeomorph is just a smooth times_diffeomorph.

Equations
@[instance]
def times_diffeomorph.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (n : with_top ) :

Equations
@[instance]
def times_diffeomorph.times_cont_mdiff_map.has_coe {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (n : with_top ) :
has_coe (M ≃ₘ^ nI,I'M') C^nI, M; I', M'

Equations
theorem times_diffeomorph.continuous {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (n : with_top ) (h : M ≃ₘ^ nI,I'M') :

theorem times_diffeomorph.times_cont_mdiff {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (n : with_top ) (h : M ≃ₘ^ nI,I'M') :
I' n h

theorem times_diffeomorph.smooth {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (h : M ≃ₘ^ I,I'M') :
I' h

theorem times_diffeomorph.coe_eq_to_equiv {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {H : Type u_5} {H' : Type u_6} (I : H) (I' : H') (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (n : with_top ) (h : M ≃ₘ^ nI,I'M') (x : M) :
h x = (h.to_equiv) x

def times_diffeomorph.refl {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {H : Type u_5} (I : H) (M : Type u_8) [ M] (n : with_top ) :

Identity map as a diffeomorphism.

Equations
def times_diffeomorph.trans {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {E' : Type u_3} [normed_group E'] [ E'] {F : Type u_4} [normed_group F] [ F] {H : Type u_5} {H' : Type u_6} {G : Type u_7} (I : H) (I' : H') (J : G) (M : Type u_8) [ M] (M' : Type u_9) [ M'] [ M'] (N : Type u_10) [ N] (n : with_top ) (h₁ : M ≃ₘ^ nI,I'M') (h₂ : M' ≃ₘ^ nI',JN) :

Composition of two diffeomorphisms.

Equations
def times_diffeomorph.symm {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] {F : Type u_4} [normed_group F] [ F] {H : Type u_5} {G : Type u_7} (I : H) (J : G) (M : Type u_8) [ M] (N : Type u_10) [ N] (n : with_top ) (h : M ≃ₘ^ nI,JN) :

Inverse of a diffeomorphism.

Equations