The local fibre count of a holomorphic map between Riemann surfaces

TauCeti.localDegree counts, on a disc in the complex plane, the orders of vanishing of f - w as w ranges over the values close to f z₀; it is the analytic form of the statement that a nonconstant holomorphic function maps a small disc onto a disc around the image of its centre, counted with multiplicity. This file transports that count to a map f : X → Y between Riemann surfaces, where the count is read as a sum of TauCeti.RiemannSurface.localMultiplicity over a fibre of f restricted to a chart neighbourhood of the point. It is the counting consequence of the local normal form z ↦ z ^ m of a nonconstant holomorphic map, obtained as a count rather than as a conjugacy.

A degree read as a sum of local multiplicities over a whole fibre rests on the local statement recorded here: close to a point where the multiplicity of f is positive, every nearby fibre is finite, nonempty, and carries exactly the multiplicity of the base point, and the neighbourhood of the point on which it is counted may be taken inside any prescribed neighbourhood. Nonconstancy of f near x is therefore spelled as the hypothesis ¬ EventuallyConst f (𝓝 x), which says that localMultiplicity f x is positive, so the count is a positive integer.

Main declarations

• TauCeti.RiemannSurface.exists_nhds_localMultiplicity_fiber_sum: the local fibre count.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §10.
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Graduate Studies in Mathematics 5, American Mathematical Society, 1995, Chapter III §3.

The local fibre count

theorem TauCeti.RiemannSurface.exists_nhds_localMultiplicity_fiber_sum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] (hDiff : ∀ᶠ (y : X) in nhds x, MDiffAt f y) (hne : ¬Filter.EventuallyConst f (nhds x)) {W : Set X} (hW : W ∈ nhds x) : ∃ U ∈ nhds x, U ⊆ W ∧ ∃ V ∈ nhds (f x), f ⁻¹' {f x} ∩ U = {x} ∧ ∀ y' ∈ V, f ⁻¹' {y'} ∩ U ≠ ∅ ∧ (f ⁻¹' {y'} ∩ U).Finite ∧ ∑ᶠ (x' : X) (_ : x' ∈ f ⁻¹' {y'} ∩ U), localMultiplicity f x' = localMultiplicity f x

The local fibre count. Let f : X → Y be differentiable at every point of a neighbourhood of x and not constant near x, and let W be any neighbourhood of x. There are neighbourhoods U ⊆ W of x and V of f x such that x is the only preimage of f x inside U, and for every y' ∈ V the fibre of y' meets U, is finite there, and the sum of the local multiplicities over it is exactly localMultiplicity f x.

This is the counting consequence of the local normal form z ↦ z ^ m of a nonconstant holomorphic map, read without choosing a conjugacy: the multiplicity of f at x is the number of preimages of a nearby value, counted with multiplicities. That U can be taken inside any prescribed neighbourhood is what makes the counts at the finitely many points of a fibre combine into a count over the whole fibre.