The open mapping theorem for Riemann surfaces

A holomorphic map f : X → Y between Riemann surfaces which is constant near no point of X is an open map: this is the open mapping theorem for Riemann surfaces. It follows from the local fibre count TauCeti.RiemannSurface.exists_nhds_localMultiplicity_fiber_sum, which produces, for every neighbourhood U of a point x, a neighbourhood V of f x all of whose points have a preimage in U. As a consequence, if f is holomorphic and nonconstant near x and g is nonconstant near f x, then g ∘ f is nonconstant near x, which is how nonconstancy of a composite of holomorphic maps is established.

Nonconstancy is spelled pointwise, as ¬ EventuallyConst f (𝓝 x), exactly as in the local fibre count; on a connected X this is equivalent to f being nonconstant by the identity theorem, which is not part of this file.

Main declarations

• TauCeti.RiemannSurface.nhds_le_map_nhds_of_not_eventuallyConst: the open mapping theorem at a point.
• TauCeti.RiemannSurface.isOpenMap_of_forall_not_eventuallyConst: the open mapping theorem.
• TauCeti.RiemannSurface.not_eventuallyConst_comp: a composite of maps nonconstant near a point is nonconstant near it.

References

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

theorem TauCeti.RiemannSurface.nhds_le_map_nhds_of_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)) : nhds (f x) ≤ Filter.map f (nhds x)

The open mapping theorem, at a point. A map holomorphic and nonconstant near x sends every neighbourhood of x onto a neighbourhood of f x.

theorem TauCeti.RiemannSurface.isOpenMap_of_forall_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} (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) : IsOpenMap f

The open mapping theorem. A holomorphic map between Riemann surfaces which is constant near no point is an open map.

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

If f is holomorphic and nonconstant near x and g is not constant near f x, then g ∘ f is not constant near x: by the open mapping theorem, constancy of g ∘ f near x would force constancy of g on the neighbourhood f '' U of f x.