The open-mapping degree

The local mapping theorem: near a point z₀ at which f - f z₀ vanishes to order n, every value w close enough to f z₀ is attained exactly n times, counted with multiplicity. This is the third target of layer L0 (the local-mapping engine) of the conformal-mapping roadmap.

This strengthens the open mapping theorem quantitatively. That theorem says the image of an open set is open — every nearby value is attained at least once. The degree says how many times: exactly n, so f is locally an n-to-one branched cover, behaving like z ↦ z ^ n up to a change of coordinates. Nothing here is derived from Mathlib's Complex.AnalyticOnNhd.is_constant_or_isOpenMap; the relationship is one of strength, not dependency.

The proof is a Rouché comparison. On a circle small enough that z₀ is the only solution of f z = f z₀ inside, ‖f - f z₀‖ attains a positive minimum δ; for ‖w - f z₀‖ < δ the difference (f - f z₀) - (f - w) = w - f z₀ is smaller than ‖f - f z₀‖ there, so Rouché equates the zero counts of f - w and f - f z₀ inside. The latter count collapses to the single order at z₀, because z₀ is its only zero in the disc.

Adding the hypothesis that f' is zero-free on the punctured disc upgrades the count with multiplicity to the sharper classical statement: for w ≠ f z₀ the n solutions are distinct and each is a simple zero of f - w.

That refinement yields the local injectivity criterion: an analytic function is injective on some neighbourhood of z₀ exactly when deriv f z₀ ≠ 0. The forward direction is proved here — a critical point makes the degree at least 2, so a nearby value is attained twice — and needs no non-constancy hypothesis, since a function constant near z₀ is not injective there either. The converse is Mathlib's inverse function theorem (HasStrictDerivAt.eventually_left_inverse), consumed rather than reproved.

Main results

• TauCeti.localDegree — the count form, with the radius supplied by the caller.
• TauCeti.localDegree_card — the distinct-and-simple form.
• TauCeti.exists_localDegree — the textbook form: if z₀ is an isolated solution of f z = f z₀, suitable radii exist.
• TauCeti.not_injOn_of_deriv_eq_zero — a critical point destroys injectivity on every neighbourhood of z₀.
• TauCeti.exists_injOn_nhds_iff_deriv_ne_zero — the local injectivity criterion.
• TauCeti.deriv_ne_zero_of_injOn — the derivative of a holomorphic injection of an open set vanishes nowhere on it.

Coordination with upstream Mathlib

Per the Coordination with upstream Mathlib section of ConformalMapping/README.md, L0 material overlaps mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort. This file is therefore a temporary shim: once corresponding Mathlib lemmas land, these statements should be backed by them — or deleted and their consumers refactored — rather than maintained as independent re-proofs. What Tau Ceti adds at L0 is named, discoverable API, not first proof.

References

• L. Ahlfors, Complex Analysis, Ch. 4 §3.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IV §7.

theorem TauCeti.localDegree {f : ℂ → ℂ} {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f (Metric.closedBall z₀ r)) (hisol : ∀ z ∈ Metric.closedBall z₀ r, z ≠ z₀ → f z ≠ f z₀) : ∃ δ > 0, ∀ (w : ℂ), ‖w - f z₀‖ < δ → ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball z₀ r), analyticOrderNatAt (fun (ζ : ℂ) => f ζ - w) z = analyticOrderNatAt (fun (ζ : ℂ) => f ζ - f z₀) z₀

The open-mapping degree, count form. If f is holomorphic on the closed disc C(z₀, r) and z₀ is the only solution there of f z = f z₀, then every w close enough to f z₀ is attained in the open disc exactly as often as f z₀ is — that is, analyticOrderNatAt of f - f z₀ at z₀ times, counted with multiplicity.

theorem TauCeti.localDegree_card {f : ℂ → ℂ} {z₀ : ℂ} {r : ℝ} (hr : 0 < r) (hf : AnalyticOnNhd ℂ f (Metric.closedBall z₀ r)) (hisol : ∀ z ∈ Metric.closedBall z₀ r, z ≠ z₀ → f z ≠ f z₀) (hderiv : ∀ z ∈ Metric.ball z₀ r, z ≠ z₀ → deriv f z ≠ 0) : ∃ δ > 0, ∀ (w : ℂ), w ≠ f z₀ → ‖w - f z₀‖ < δ → {z : ℂ | z ∈ Metric.ball z₀ r ∧ f z = w}.Finite ∧ {z : ℂ | z ∈ Metric.ball z₀ r ∧ f z = w}.ncard = analyticOrderNatAt (fun (ζ : ℂ) => f ζ - f z₀) z₀ ∧ ∀ z ∈ Metric.ball z₀ r, f z = w → analyticOrderNatAt (fun (ζ : ℂ) => f ζ - w) z = 1

The open-mapping degree, distinct-and-simple form. Under the additional hypothesis that f' is zero-free on the punctured disc, every w ≠ f z₀ close enough to f z₀ has exactly n distinct preimages in the open disc, each of them a simple zero of f - w.

theorem TauCeti.exists_localDegree {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (hisol : ∀ᶠ (z : ℂ) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ f z₀) : ∃ r > 0, AnalyticOnNhd ℂ f (Metric.closedBall z₀ r) ∧ ∃ δ > 0, ∀ (w : ℂ), ‖w - f z₀‖ < δ → ∑ᶠ (z : ℂ) (_ : z ∈ Metric.ball z₀ r), analyticOrderNatAt (fun (ζ : ℂ) => f ζ - w) z = analyticOrderNatAt (fun (ζ : ℂ) => f ζ - f z₀) z₀

The open-mapping degree, textbook form. If f is analytic at z₀ and z₀ is an isolated solution of f z = f z₀ — equivalently, f is not constant near z₀ — then there are radii r and δ for which localDegree applies.

theorem TauCeti.not_injOn_of_deriv_eq_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (hd₀ : deriv f z₀ = 0) {V : Set ℂ} (hV : V ∈ nhds z₀) : ¬Set.InjOn f V

Local injectivity fails at a critical point. An analytic function whose derivative vanishes at z₀ is not injective on any neighbourhood of z₀.

No non-constancy hypothesis is needed: if f is constant near z₀ the conclusion is immediate, and otherwise f - f z₀ vanishes at z₀ to finite order n, which deriv f z₀ = 0 forces to be at least 2, so localDegree_card produces two distinct preimages of a nearby value.

theorem TauCeti.exists_injOn_nhds_iff_deriv_ne_zero {f : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) : (∃ V ∈ nhds z₀, Set.InjOn f V) ↔ deriv f z₀ ≠ 0

The local injectivity criterion. An analytic function is injective on some neighbourhood of z₀ exactly when its derivative there is nonzero.

The forward direction is not_injOn_of_deriv_eq_zero; the reverse is Mathlib's inverse function theorem, consumed rather than reproved.

theorem TauCeti.deriv_ne_zero_of_injOn {f : ℂ → ℂ} {U : Set ℂ} (hf : DifferentiableOn ℂ f U) (hU : IsOpen U) (hinj : Set.InjOn f U) {z : ℂ} (hz : z ∈ U) : deriv f z ≠ 0

The derivative of a holomorphic injection of an open set vanishes nowhere on it. The pointwise form of TauCeti.exists_injOn_nhds_iff_deriv_ne_zero: injectivity on the open set is injectivity on a neighbourhood of each of its points.