Diffeomorphisms #

DDiffeomorph.instEquivLike = { coe := fun (Φ : X ᵈ≃ Y) => ⇑Φ.toEquiv, inv := fun (Φ : X ᵈ≃ Y) => ⇑Φ.symm, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source

theorem DDiffeomorph.continuous {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

Continuous ⇑h

source

theorem DDiffeomorph.continuous' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) :

Continuous ⇑h

source

theorem DDiffeomorph.dsmooth {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

DSmooth ⇑h

source

theorem DDiffeomorph.isInduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

IsInduction ⇑h

source

theorem DDiffeomorph.isOpenInduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

IsOpenInduction ⇑h

source

theorem DDiffeomorph.isSubduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

IsSubduction ⇑h

source

@[simp]

theorem DDiffeomorph.coe_toEquiv {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

⇑h.toEquiv = ⇑h

source

@[simp]

theorem DDiffeomorph.toEquiv_inj {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {h h' : X ᵈ≃ Y} :

h.toEquiv = h'.toEquiv ↔ h = h'

source

theorem DDiffeomorph.coeFn_injective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] :

Function.Injective DFunLike.coe

source

theorem DDiffeomorph.bijective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

Function.Bijective ⇑h

source

theorem DDiffeomorph.injective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

Function.Injective ⇑h

source

theorem DDiffeomorph.surjective {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

Function.Surjective ⇑h

source

theorem DDiffeomorph.ext {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {h h' : X ᵈ≃ Y} (heq : ∀ (x : X), h x = h' x) :

h = h'

source

theorem DDiffeomorph.ext_iff {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {h h' : X ᵈ≃ Y} :

h = h' ↔ ∀ (x : X), h x = h' x

source

def DDiffeomorph.refl (X : Type u_4) [DiffeologicalSpace X] :

X ᵈ≃ X

Identity map as a diffeomorphism.

Equations

DDiffeomorph.refl X = { toEquiv := Equiv.refl X, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.refl_toEquiv {X : Type u_1} [DiffeologicalSpace X] :

(DDiffeomorph.refl X).toEquiv = Equiv.refl X

source

@[simp]

theorem DDiffeomorph.coe_refl {X : Type u_1} [DiffeologicalSpace X] :

⇑(DDiffeomorph.refl X) = id

source

def DDiffeomorph.trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h₁ : X ᵈ≃ Y) (h₂ : Y ᵈ≃ Z) :

X ᵈ≃ Z

Composition of diffeomorphisms.

Equations

h₁.trans h₂ = { toEquiv := h₁.trans h₂.toEquiv, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.trans_refl {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

h.trans (DDiffeomorph.refl Y) = h

source

@[simp]

theorem DDiffeomorph.refl_trans {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

(DDiffeomorph.refl X).trans h = h

source

@[simp]

theorem DDiffeomorph.coe_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h₁ : X ᵈ≃ Y) (h₂ : Y ᵈ≃ Z) :

⇑(h₁.trans h₂) = ⇑h₂ ∘ ⇑h₁

source

def DDiffeomorph.symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

Y ᵈ≃ X

Inverse of a diffeomorphism.

Equations

h.symm = { toEquiv := h.symm, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.apply_symm_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (y : Y) :

h (h.symm y) = y

source

@[simp]

theorem DDiffeomorph.symm_apply_apply {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (x : X) :

h.symm (h x) = x

source

@[simp]

theorem DDiffeomorph.symm_refl {X : Type u_1} [DiffeologicalSpace X] :

(DDiffeomorph.refl X).symm = DDiffeomorph.refl X

source

@[simp]

theorem DDiffeomorph.self_trans_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

h.trans h.symm = DDiffeomorph.refl X

source

@[simp]

theorem DDiffeomorph.symm_trans_self {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

h.symm.trans h = DDiffeomorph.refl Y

source

@[simp]

theorem DDiffeomorph.symm_trans' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h₁ : X ᵈ≃ Y) (h₂ : Y ᵈ≃ Z) :

(h₁.trans h₂).symm = h₂.symm.trans h₁.symm

source

@[simp]

theorem DDiffeomorph.symm_toEquiv {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

h.symm.toEquiv = h.symm

source

@[simp]

theorem DDiffeomorph.toEquiv_coe_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

⇑h.symm = ⇑h.symm

source

theorem DDiffeomorph.image_eq_preimage {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set X) :

⇑h '' s = ⇑h.symm ⁻¹' s

source

theorem DDiffeomorph.symm_image_eq_preimage {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set Y) :

⇑h.symm '' s = ⇑h ⁻¹' s

source

@[simp]

theorem DDiffeomorph.range_comp {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {α : Type u_4} (h : X ᵈ≃ Y) (f : α → X) :

Set.range (⇑h ∘ f) = ⇑h.symm ⁻¹' Set.range f

source

@[simp]

theorem DDiffeomorph.image_symm_image {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set Y) :

⇑h '' (⇑h.symm '' s) = s

source

@[simp]

theorem DDiffeomorph.symm_image_image {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) (s : Set X) :

⇑h.symm '' (⇑h '' s) = s

source

noncomputable def DDiffeomorph.ofIsInduction {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] {f : X → Y} (hf : IsInduction f) :

X ᵈ≃ ↑(Set.range f)

An induction is a diffeomorphism onto its image.

Equations

DDiffeomorph.ofIsInduction hf = { toEquiv := Equiv.ofInjective f ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

def DDiffeomorph.toHomeomorph {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

X ≃ₜ Y

A diffeomorphism is a homeomorphism with respect to the D-topologies.

Equations

h.toHomeomorph = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.toHomeomorph_toEquiv {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

h.toHomeomorph.toEquiv = h.toEquiv

source

@[simp]

theorem DDiffeomorph.symm_toHomeomorph {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

h.symm.toHomeomorph = h.toHomeomorph.symm

source

@[simp]

theorem DDiffeomorph.coe_toHomeomorph {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

⇑h.toHomeomorph = ⇑h

source

@[simp]

theorem DDiffeomorph.coe_toHomeomorph_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (h : X ᵈ≃ Y) :

⇑h.toHomeomorph.symm = ⇑h.symm

source

def DDiffeomorph.toHomeomorph' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) :

X ≃ₜ Y

A diffeomorphism between spaces that are equipped with the D-topologies is also a homeoomorphism.

Equations

h.toHomeomorph' = { toEquiv := h.toEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.toHomeomorph_toEquiv' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) :

h.toHomeomorph'.toEquiv = h.toEquiv

source

@[simp]

theorem DDiffeomorph.symm_toHomeomorph' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) :

h.symm.toHomeomorph' = h.toHomeomorph'.symm

source

@[simp]

theorem DDiffeomorph.coe_toHomeomorph' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) :

⇑h.toHomeomorph' = ⇑h

source

@[simp]

theorem DDiffeomorph.coe_toHomeomorph_symm' {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Y] [DTopCompatible X] [DTopCompatible Y] (h : X ᵈ≃ Y) :

⇑h.toHomeomorph'.symm = ⇑h.symm

source

@[simp]

theorem DDiffeomorph.dsmooth_comp_ddiffeomorph_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h : X ᵈ≃ Y) {f : Y → Z} :

DSmooth (f ∘ ⇑h) ↔ DSmooth f

source

@[simp]

theorem DDiffeomorph.dsmooth_ddiffeomorph_comp_iff {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (h : X ᵈ≃ Y) {f : Z → X} :

DSmooth (⇑h ∘ f) ↔ DSmooth f

source

theorem IsInduction.dsmooth_comp_iff_dsmooth_restrict {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] {f : X → Y} (hf : IsInduction f) {g : Y → Z} :

DSmooth (g ∘ f) ↔ DSmooth ((Set.range f).restrict g)

For any induction f, g ∘ f is smooth iff g is smooth on Set.range f. TODO: move to a more fitting location

source

instance DDiffeomorph.instContinuousMapClass {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] :

DSmoothMapClass (X ᵈ≃ Y) X Y

source

@[reducible, inline]

abbrev DDiffeomorph.toDSmoothMap {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (d : X ᵈ≃ Y) :

DSmoothMap X Y

Equations

d.toDSmoothMap = ↑d

Instances For

source

@[simp]

theorem DDiffeomorph.toDSmoothMap_refl {X : Type u_1} [DiffeologicalSpace X] :

↑(DDiffeomorph.refl X) = DSmoothMap.id X

source

@[simp]

theorem DDiffeomorph.toDSmoothMap_trans {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (f : X ᵈ≃ Y) (g : Y ᵈ≃ Z) :

↑(f.trans g) = (↑g).comp ↑f

source

@[simp]

theorem DDiffeomorph.symm_comp_toDSmoothMap {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X ᵈ≃ Y) :

(↑f.symm).comp ↑f = DSmoothMap.id X

Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self.

source

@[simp]

theorem DDiffeomorph.toDSmoothMap_comp_symm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (f : X ᵈ≃ Y) :

(↑f).comp ↑f.symm = DSmoothMap.id Y

Right inverse to a continuous map from a homeomorphism, mirroring Equiv.self_comp_symm.

source

noncomputable def DDiffeomorph.univBall {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] (x : E) {r : ℝ} (hr : r > 0) :

E ᵈ≃ ↑(Metric.ball x r)

Inner product spaces are diffeomorphic to open balls in them.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem DDiffeomorph.coe_univBall_zero {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [DiffeologicalSpace E] [ContDiffCompatible E] (x : E) {r : ℝ} (hr : r > 0) :

↑((univBall x hr) 0) = x

source

def DDiffeomorph.Set.univ (X : Type u_4) [DiffeologicalSpace X] :

↑_root_.Set.univ ᵈ≃ X

Set.univ X is diffeomorphic to X.

Equations

DDiffeomorph.Set.univ X = { toEquiv := Equiv.Set.univ X, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.Set.univ_invFun_coe (X : Type u_4) [DiffeologicalSpace X] (a : X) :

↑((univ X).invFun a) = a

source

@[simp]

theorem DDiffeomorph.Set.univ_toFun (X : Type u_4) [DiffeologicalSpace X] :

⇑(univ X) = Subtype.val

source

def DDiffeomorph.Set.nested {X : Type u_1} [DiffeologicalSpace X] {u : Set X} (v : Set ↑u) :

↑v ᵈ≃ ↑(Subtype.val '' v)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def DDiffeomorph.restrict {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (d : X ᵈ≃ Y) (u : Set X) :

↑u ᵈ≃ ↑(⇑d.symm ⁻¹' u)

Equations

d.restrict u = { toFun := Set.MapsTo.restrict (⇑d) u (⇑d.symm ⁻¹' u) ⋯, invFun := u.restrictPreimage ⇑d.symm, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

def DDiffeomorph.restrictPreimage {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] (d : X ᵈ≃ Y) (u : Set Y) :

↑(⇑d ⁻¹' u) ᵈ≃ ↑u

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def DDiffeomorph.quotient_bot (X : Type u_4) [DiffeologicalSpace X] :

Quotient ⊥ ᵈ≃ X

The quotient of X by the identity relation is diffeomorphic to X.

Equations

DDiffeomorph.quotient_bot X = { toFun := Quotient.lift id ⋯, invFun := Quotient.mk', left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

@[simp]

theorem DDiffeomorph.quotient_bot_invFun (X : Type u_4) [DiffeologicalSpace X] :

(quotient_bot X).invFun = Quotient.mk'

source

@[simp]

theorem DDiffeomorph.quotient_bot_toFun (X : Type u_4) [DiffeologicalSpace X] :

⇑(quotient_bot X) = Quotient.lift id ⋯

source

def DDiffeomorph.prodComm {X : Type u_1} {Y : Type u_2} [DiffeologicalSpace X] [DiffeologicalSpace Y] :

X × Y ᵈ≃ Y × X

Equations

DDiffeomorph.prodComm = { toFun := Prod.swap, invFun := Prod.swap, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

def DDiffeomorph.curry {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] :

DSmoothMap (X × Y) Z ᵈ≃ DSmoothMap X (DSmoothMap Y Z)

The currying diffeomorphism DSmoothMap (X × Y) Z ᵈ≃ DSmoothMap X (DSmoothMap Y Z).

Equations

DDiffeomorph.curry = { toFun := DSmoothMap.curry, invFun := DSmoothMap.uncurry, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }

Instances For

source

def DDiffeomorph.comp_left {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (d : Y ᵈ≃ Z) :

DSmoothMap X Y ᵈ≃ DSmoothMap X Z

Postcomposition with d : Y ᵈ≃ Z as a diffeomorphism DSmoothMap X Y ᵈ≃ DSmoothMap X Z.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def DDiffeomorph.comp_right {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DiffeologicalSpace X] [DiffeologicalSpace Y] [DiffeologicalSpace Z] (d : X ᵈ≃ Y) :

DSmoothMap Y Z ᵈ≃ DSmoothMap X Z

Precomposition with d : X ᵈ≃ Y as a diffeomorphism DSmoothMap Y Z ᵈ≃ DSmoothMap X Z.

Equations

d.comp_right = { toFun := fun (f : DSmoothMap Y Z) => f.comp ↑d, invFun := fun (f : DSmoothMap X Z) => f.comp ↑d.symm, left_inv := ⋯, right_inv := ⋯, dsmooth_toFun := ⋯, dsmooth_invFun := ⋯ }