The identity theorem for Riemann surfaces

A holomorphic map f : X → Y between Riemann surfaces which is constant near one point of a connected X is constant: this is the identity theorem for Riemann surfaces. The set of points near which f is constant is open for any map, and it is closed because the chart representative of f near a point is analytic on a disc, so that the identity theorem for analytic functions, AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq, spreads constancy near one point of the disc to the whole disc. On a connected X the set is therefore empty or everything, and in the second case f is locally constant, hence constant.

The contrapositive form TauCeti.RiemannSurface.not_eventuallyConst_of_ne turns the hypothesis that f takes two distinct values into the pointwise nonconstancy ∀ x, ¬ EventuallyConst f (𝓝 x) under which the local fibre count, the open mapping theorem and the degree are stated.

Main declarations

• TauCeti.RiemannSurface.eventually_not_eventuallyConst: near a point at which a holomorphic map is not constant, it is not constant near any point.
• TauCeti.RiemannSurface.apply_eq_of_eventuallyConst: the identity theorem.
• TauCeti.RiemannSurface.not_eventuallyConst_of_ne: a holomorphic map on a connected Riemann surface taking two distinct values is constant near no point.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §1, Theorem 1.11.

theorem TauCeti.RiemannSurface.eventually_not_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {f : X → Y} {x : X} (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) (hne : ¬Filter.EventuallyConst f (nhds x)) : ∀ᶠ (x' : X) in nhds x, ¬Filter.EventuallyConst f (nhds x')

A map holomorphic near x which is not constant near x is not constant near any point close to x: its chart representative is analytic on a disc about the coordinate of x, and constancy of the representative near one point of the disc would spread to the whole disc.

theorem TauCeti.RiemannSurface.apply_eq_of_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {f : X → Y} [PreconnectedSpace X] (hf : MDiff f) {x : X} (hx : Filter.EventuallyConst f (nhds x)) (x' : X) : f x' = f x

The identity theorem for Riemann surfaces. A holomorphic map on a connected Riemann surface which is constant near one point is constant.

theorem TauCeti.RiemannSurface.not_eventuallyConst_of_ne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {f : X → Y} [PreconnectedSpace X] (hf : MDiff f) {x₁ x₂ : X} (h : f x₁ ≠ f x₂) (x : X) : ¬Filter.EventuallyConst f (nhds x)

A holomorphic map on a connected Riemann surface which takes two distinct values is constant near no point.