Injective holomorphic maps as partial homeomorphisms

An injective holomorphic map on an open subset of ℂ is a biholomorphism onto its image. This file packages that fact as an OpenPartialHomeomorph ℂ ℂ, so conformal-mapping results can carry their source, target, inverse, and topological equivalence in one existing Mathlib object.

The forward map of DifferentiableOn.toOpenPartialHomeomorph is the original function, its source is the given open set, its target is the image, and its inverse is Function.invFunOn. The inverse is holomorphic by DifferentiableOn.invFunOn. Both directions are conformal: injectivity on an open neighbourhood forces the complex derivative to be nonzero, so Mathlib's DifferentiableAt.conformalAt applies.

This is the packaging prerequisite for the conformal companion to the Riemann mapping theorem. It advances the ConformalMapping/README.md generality-bar requirement to derive packaged equivalence and ConformalAt API from a holomorphic bijection.

Main declarations

• DifferentiableOn.toOpenPartialHomeomorph packages an injective holomorphic map.
• DifferentiableOn.toHomeomorphOfBijOn packages a holomorphic bijection between open sets as a homeomorphism of their subtypes.
• DifferentiableOn.conformalAt_of_isOpen_of_injOn proves its pointwise conformality.
• DifferentiableOn.conformalAt_toOpenPartialHomeomorph_symm proves conformality of the inverse.

Coordination with upstream Mathlib

This L0--L3 infrastructure overlaps the Riemann-mapping development in mathlib4#33505. It is a temporary shim: replace it with public human-curated Mathlib API, and refactor its consumers, if that development exports the same packaging.

noncomputable def DifferentiableOn.toOpenPartialHomeomorph {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : OpenPartialHomeomorph ℂ ℂ

Package an injective holomorphic map on an open set as an open partial homeomorphism onto its image.

On the image, Function.invFunOn f U selects the unique preimage in U; no injectivity of f outside U is required.

Equations

• hf.toOpenPartialHomeomorph hU hinj = OpenPartialHomeomorph.ofContinuousOpenRestrict (Set.InjOn.toPartialEquiv f U hinj) ⋯ ⋯ hU

@[simp]

theorem DifferentiableOn.toOpenPartialHomeomorph_source {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : (hf.toOpenPartialHomeomorph hU hinj).source = U

The source of the partial homeomorphism associated to an injective holomorphic map is its given domain.

@[simp]

theorem DifferentiableOn.toOpenPartialHomeomorph_target {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : (hf.toOpenPartialHomeomorph hU hinj).target = f '' U

The target of the partial homeomorphism associated to an injective holomorphic map is its image.

@[simp]

theorem DifferentiableOn.toOpenPartialHomeomorph_apply {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) (z : ℂ) : ↑(hf.toOpenPartialHomeomorph hU hinj) z = f z

The partial homeomorphism associated to an injective holomorphic map applies as the original map.

@[simp]

theorem DifferentiableOn.toOpenPartialHomeomorph_coe {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : ↑(hf.toOpenPartialHomeomorph hU hinj) = f

The underlying function of the partial homeomorphism associated to an injective holomorphic map is the original map.

@[simp]

theorem DifferentiableOn.toOpenPartialHomeomorph_symm_apply {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) (w : ℂ) : ↑(hf.toOpenPartialHomeomorph hU hinj).symm w = Function.invFunOn f U w

The inverse of the partial homeomorphism associated to an injective holomorphic map is Function.invFunOn for the specified domain.

@[simp]

theorem DifferentiableOn.toOpenPartialHomeomorph_coe_symm {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : ↑(hf.toOpenPartialHomeomorph hU hinj).symm = Function.invFunOn f U

The underlying inverse function of the partial homeomorphism associated to an injective holomorphic map is Function.invFunOn for the specified domain.

noncomputable def DifferentiableOn.toHomeomorphOfBijOn {U : Set ℂ} {f : ℂ → ℂ} {V : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hbij : Set.BijOn f U V) : ↑U ≃ₜ ↑V

Package a holomorphic bijection from an open set U onto a set V as a homeomorphism between the corresponding subtypes.

This is the subtype equivalence carried by DifferentiableOn.toOpenPartialHomeomorph, with its target identified using the supplied BijOn hypothesis.

Equations

• hf.toHomeomorphOfBijOn hU hbij = (hf.toOpenPartialHomeomorph hU ⋯).homeomorphOfImageSubsetSource ⋯ ⋯

@[simp]

theorem DifferentiableOn.toHomeomorphOfBijOn_apply {U : Set ℂ} {f : ℂ → ℂ} {V : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hbij : Set.BijOn f U V) (z : ↑U) : ↑((hf.toHomeomorphOfBijOn hU hbij) z) = f ↑z

The homeomorphism induced by a holomorphic bijection applies as the original map.

@[simp]

theorem DifferentiableOn.toHomeomorphOfBijOn_symm_apply {U : Set ℂ} {f : ℂ → ℂ} {V : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hbij : Set.BijOn f U V) (w : ↑V) : ↑((hf.toHomeomorphOfBijOn hU hbij).symm w) = Function.invFunOn f U ↑w

The inverse homeomorphism induced by a holomorphic bijection applies as Function.invFunOn.

theorem DifferentiableOn.differentiableOn_toOpenPartialHomeomorph_symm {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) : DifferentiableOn ℂ (↑(hf.toOpenPartialHomeomorph hU hinj).symm) (f '' U)

The inverse of the open partial homeomorphism associated to an injective holomorphic map is holomorphic on its target.

theorem DifferentiableOn.conformalAt_of_isOpen_of_injOn {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) {z : ℂ} (hz : z ∈ U) : ConformalAt f z

An injective holomorphic map on an open set is conformal at every point of that set.

theorem DifferentiableOn.conformalAt_toOpenPartialHomeomorph {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) {z : ℂ} (hz : z ∈ U) : ConformalAt (↑(hf.toOpenPartialHomeomorph hU hinj)) z

The open partial homeomorphism associated to an injective holomorphic map is conformal on its source.

theorem DifferentiableOn.conformalAt_toOpenPartialHomeomorph_symm {U : Set ℂ} {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) {w : ℂ} (hw : w ∈ f '' U) : ConformalAt (↑(hf.toOpenPartialHomeomorph hU hinj).symm) w

The inverse of the open partial homeomorphism associated to an injective holomorphic map is conformal on its target.