Coverings away from branch values

For a finite holomorphic map of connected Riemann surfaces, the branch values are the images of the points of local multiplicity greater than one. With compact source this is a finite closed set, and the map is a covering over its complement. Every fibre of this covering has cardinality equal to the analytic degree of the map. Conversely, a branch value cannot admit an evenly covered neighbourhood: a local homeomorphism has local multiplicity one.

These results supply the unbranched covering obtained by removing neighbourhoods of branch values, used in the topological proof of the Riemann--Hurwitz formula. The restriction is Mathlib's Set.restrictPreimage, so the ordinary covering-map API applies without a new carrier or notion of covering.

The covering and its sheet count use local multiplicity, finite fibres, and the analytic fibre-sum degree. Euler characteristic and topological genus are needed for the subsequent Riemann--Hurwitz application, rather than for these covering results.

Main declarations

• FiniteHolomorphicMap.branchValues: the set of branch values.
• FiniteHolomorphicMap.isLocalHomeomorphOn_iff: local homeomorphy is equivalent to local multiplicity one at every point of the specified source set.
• FiniteHolomorphicMap.isCoveringMapOn_iff: a map with compact source is a covering on precisely the subsets disjoint from its branch values.
• FiniteHolomorphicMap.isCoveringMap_restrictPreimage_branchValues_compl: the covering obtained by deleting the branch values and their preimages.
• FiniteHolomorphicMap.card_fiber_eq_degree_iff: a fibre has as many points as the degree exactly when its value is not a branch value.
• FiniteHolomorphicMap.ncard_fiber_restrictPreimage_branchValues_compl: every fibre of the restricted covering has cardinality equal to the analytic degree.

References

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

The covering construction uses Mathlib's IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn.

def TauCeti.RiemannSurface.FiniteHolomorphicMap.branchValues {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : FiniteHolomorphicMap X Y) : Set Y

The branch values of a finite holomorphic map: the images of the points with local multiplicity greater than one.

Equations

• f.branchValues = ↑f '' {x : X | 1 < TauCeti.RiemannSurface.localMultiplicity (↑f) x}

@[simp]

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.mem_branchValues_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : FiniteHolomorphicMap X Y) (y : Y) : y ∈ f.branchValues ↔ ∃ (x : X), ↑f x = y ∧ 1 < localMultiplicity (↑f) x

A value is a branch value exactly when some point above it is ramified.

@[simp]

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.notMem_branchValues_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] (f : FiniteHolomorphicMap X Y) (y : Y) : y ∉ f.branchValues ↔ ∀ (x : X), ↑f x = y → localMultiplicity (↑f) x = 1

Away from branch values, every point of the fibre has local multiplicity one.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.isLocalHomeomorphOn_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] (f : FiniteHolomorphicMap X Y) (s : Set X) : IsLocalHomeomorphOn (↑f) s ↔ ∀ x ∈ s, localMultiplicity (↑f) x = 1

A finite holomorphic map is locally homeomorphic on a set exactly when its local multiplicities on that set are one. No compactness assumption is needed.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.finite_branchValues {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] (f : FiniteHolomorphicMap X Y) : f.branchValues.Finite

There are finitely many branch values for a finite holomorphic map with compact source.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.isClosed_branchValues {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T1Space Y] (f : FiniteHolomorphicMap X Y) : IsClosed f.branchValues

The branch values form a closed set.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.isOpen_branchValues_compl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T1Space Y] (f : FiniteHolomorphicMap X Y) : IsOpen f.branchValuesᶜ

The complement of the branch values is open.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.isCoveringMapOn_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] (f : FiniteHolomorphicMap X Y) (s : Set Y) : IsCoveringMapOn (↑f) s ↔ s ⊆ f.branchValuesᶜ

A finite holomorphic map with compact source is a covering over exactly those subsets of the target that contain no branch values. In particular it is not a covering at a branch value.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.isCoveringMap_restrictPreimage_branchValues_compl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] (f : FiniteHolomorphicMap X Y) : IsCoveringMap (f.branchValuesᶜ.restrictPreimage ↑f)

Deleting the branch values and their preimages gives an ordinary covering map.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.card_fiber_eq_degree_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) (y : Y) : ⋯.toFinset.card = degree ↑f ↔ y ∉ f.branchValues

A fibre has cardinality equal to the degree exactly when it contains no ramification points. Thus the covering away from branch values has as many sheets as the analytic degree.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.ncard_fiber_restrictPreimage_branchValues_compl {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) (y : ↑f.branchValuesᶜ) : (f.branchValuesᶜ.restrictPreimage ↑f ⁻¹' {y}).ncard = degree ↑f

Every fibre of the covering obtained by deleting branch values has cardinality equal to the analytic degree of the original map.