A local diffeomorphism at a point is a partial diffeomorphism near it

Mathlib defines IsLocalDiffeomorphAt I J n f x as the existence of a partial diffeomorphism Φ with x ∈ Φ.source on whose source f agrees with Φ, but does not expose the definition to importing modules, so a proof cannot destructure it. IsLocalDiffeomorphAt.exists_partialDiffeomorph recovers the witness from Mathlib's IsLocalDiffeomorphAt.localInverse: the inverse of an arbitrary local inverse of f at x. The converse is Mathlib's PartialDiffeomorph.isLocalDiffeomorphAt.

theorem IsLocalDiffeomorphAt.exists_partialDiffeomorph {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H₁ : Type u_4} [TopologicalSpace H₁] {H₂ : Type u_5} [TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H₁ M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M} (hf : IsLocalDiffeomorphAt I J n f x) : ∃ (Φ : PartialDiffeomorph I J M N n), x ∈ Φ.source ∧ Set.EqOn f (↑Φ.toPartialEquiv) Φ.source

A local diffeomorphism f at x agrees with a partial diffeomorphism Φ on the source of Φ, a neighbourhood of x: the definition of IsLocalDiffeomorphAt, which Mathlib does not expose; the witness is the inverse of hf.localInverse.

theorem IsLocalDiffeomorphAt.of_eqOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H₁ : Type u_4} [TopologicalSpace H₁] {H₂ : Type u_5} [TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H₁ M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M} (Φ : PartialDiffeomorph I J M N n) (hx : x ∈ Φ.source) (h : Set.EqOn f (↑Φ.toPartialEquiv) Φ.source) : IsLocalDiffeomorphAt I J n f x

The converse: f is a local diffeomorphism at x when it agrees on the source of a partial diffeomorphism Φ, a neighbourhood of x, with Φ. Mathlib's PartialDiffeomorph.isLocalDiffeomorphAt is the case f = Φ; here f replaces Φ as the forward map of Φ, which changes nothing on Φ.source.

def Diffeomorph.toPartialDiffeomorphUniv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H₁ : Type u_4} [TopologicalSpace H₁] {H₂ : Type u_5} [TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H₁ M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H₂ N] {n : WithTop ℕ∞} (g : Diffeomorph I J M N n) : PartialDiffeomorph I J M N n

A diffeomorphism as a partial diffeomorphism with source and target everything: Mathlib's Diffeomorph.toPartialDiffeomorph, exposed, so that in an importing module its source and target reduce to univ and its maps to those of the diffeomorphism (Mathlib exposes neither and has no lemmas about it).

Equations

• g.toPartialDiffeomorphUniv = { toPartialEquiv := g.toHomeomorph.toPartialEquiv, open_source := ⋯, open_target := ⋯, contMDiffOn_toFun := ⋯, contMDiffOn_invFun := ⋯ }

noncomputable def IsLocalDiffeomorph.toDiffeomorphOfBijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H₁ : Type u_4} [TopologicalSpace H₁] {H₂ : Type u_5} [TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H₁ M] {N : Type u_7} [TopologicalSpace N] [ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} (hf : IsLocalDiffeomorph I J n f) (hf' : Function.Bijective f) : Diffeomorph I J M N n

A bijective local diffeomorphism as a diffeomorphism, with f as its forward map: Mathlib's IsLocalDiffeomorph.diffeomorphOfBijective, exposed, so that an importing module sees that the forward map is f (Mathlib exposes neither the definition nor this fact). The inverse is a right inverse g of f, which agrees with the inverse of each local inverse of f.

Equations

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