Injective local diffeomorphisms on open sets

A local diffeomorphism that is injective on an open set identifies that set smoothly with its image. The inverse is smooth because it agrees near each image point with a local smooth inverse.

Main results:

• IsLocalDiffeomorphOn.contMDiffOn_invFunOn: the inverse on an injective open set is smooth.
• IsLocalDiffeomorphOn.partialDiffeomorphOfInjOn: the partial diffeomorphism onto the image, with simp lemmas for its source, target, forward function and inverse.

The construction extends Mathlib's IsLocalDiffeomorph.diffeomorphOfBijective, using Set.InjOn.toPartialEquiv for the inverse and its inverse laws. Nonemptiness of the domain is required to define the inverse function outside the image, even when the open set is empty.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Proposition 4.6.

theorem IsLocalDiffeomorphOn.contMDiffOn_invFunOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} [Nonempty M] (hf : IsLocalDiffeomorphOn I J n f s) (hs : IsOpen s) (hinj : Set.InjOn f s) : ContMDiffOn J I n (Function.invFunOn f s) (f '' s)

The inverse of a local diffeomorphism injective on an open set is C^n on its image. The values chosen outside the image impose no regularity requirement.

noncomputable def IsLocalDiffeomorphOn.partialDiffeomorphOfInjOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} [Nonempty M] (hf : IsLocalDiffeomorphOn I J n f s) (hs : IsOpen s) (hinj : Set.InjOn f s) : PartialDiffeomorph I J M N n

A local diffeomorphism injective on an open set, packaged as a partial diffeomorphism with that source and its actual image as target. No global injectivity is needed.

@[simp]

theorem IsLocalDiffeomorphOn.partialDiffeomorphOfInjOn_source {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} [Nonempty M] (hf : IsLocalDiffeomorphOn I J n f s) (hs : IsOpen s) (hinj : Set.InjOn f s) : (hf.partialDiffeomorphOfInjOn hs hinj).source = s

The assembled partial diffeomorphism has exactly the prescribed open source.

@[simp]

theorem IsLocalDiffeomorphOn.partialDiffeomorphOfInjOn_target {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} [Nonempty M] (hf : IsLocalDiffeomorphOn I J n f s) (hs : IsOpen s) (hinj : Set.InjOn f s) : (hf.partialDiffeomorphOfInjOn hs hinj).target = f '' s

The target of the assembled partial diffeomorphism is the image of its source.

@[simp]

theorem IsLocalDiffeomorphOn.coe_partialDiffeomorphOfInjOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} [Nonempty M] (hf : IsLocalDiffeomorphOn I J n f s) (hs : IsOpen s) (hinj : Set.InjOn f s) : ↑(hf.partialDiffeomorphOfInjOn hs hinj).toPartialEquiv = f

The assembled partial diffeomorphism retains the original forward function everywhere.

@[simp]

theorem IsLocalDiffeomorphOn.partialDiffeomorphOfInjOn_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : Type u_4} {G : Type u_5} [TopologicalSpace H] [TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G} {M : Type u_6} {N : Type u_7} [TopologicalSpace M] [ChartedSpace H M] [TopologicalSpace N] [ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {s : Set M} [Nonempty M] (hf : IsLocalDiffeomorphOn I J n f s) (hs : IsOpen s) (hinj : Set.InjOn f s) (y : N) : ↑(hf.partialDiffeomorphOfInjOn hs hinj).symm y = Function.invFunOn f s y

The inverse function of the assembled partial diffeomorphism is the inverse on its source.