mathlib documentation

geometry.manifold.diffeomorph

Diffeomorphisms

This file implements diffeomorphisms.

Definitions

Notations

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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (M : Type u_8) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (M' : Type u_9) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' 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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (M : Type u_8) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (M' : Type u_9) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' 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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (M : Type u_8) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (M' : Type u_9) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (n : with_top ) :

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

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

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

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

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

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

Identity map as a diffeomorphism.

Equations
def times_diffeomorph.trans {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {E' : Type u_3} [normed_group E'] [normed_space 𝕜 E'] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {H' : Type u_6} [topological_space H'] {G : Type u_7} [topological_space G] (I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H') (J : model_with_corners 𝕜 F G) (M : Type u_8) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (M' : Type u_9) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M'] (N : Type u_10) [topological_space N] [charted_space G N] [smooth_manifold_with_corners J 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} [nondiscrete_normed_field 𝕜] {E : Type u_2} [normed_group E] [normed_space 𝕜 E] {F : Type u_4} [normed_group F] [normed_space 𝕜 F] {H : Type u_5} [topological_space H] {G : Type u_7} [topological_space G] (I : model_with_corners 𝕜 E H) (J : model_with_corners 𝕜 F G) (M : Type u_8) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M] (N : Type u_10) [topological_space N] [charted_space G N] [smooth_manifold_with_corners J N] (n : with_top ) (h : M ≃ₘ^ nI,JN) :

Inverse of a diffeomorphism.

Equations