The ramification divisor of a finite holomorphic map

Let f : X → Y be a finite holomorphic map of Riemann surfaces with X connected. Its local multiplicity e_x = localMultiplicity f x is at least 1 everywhere, and x is a ramification point when e_x > 1. Near every point of X the map has multiplicity 1 at all other points (TauCeti.RiemannSurface.eventually_localMultiplicity_eq_one), so the ramification points form a codiscrete complement; when X is moreover compact there are only finitely many of them. The ramification divisor is the effective divisor

R_f = ∑ₓ (e_x - 1) [x]

on X, and the ramification degree is its degree ∑ₓ (e_x - 1), the correction term in the Riemann–Hurwitz formula 2 g_X - 2 = deg f · (2 g_Y - 2) + deg R_f.

Over each point y of a connected target, the fibre has deg f - ∑_{x ∈ f⁻¹(y)} (e_x - 1) points; equivalently, the pushforward of R_f to Y has coefficient deg f - #f⁻¹(y) at y. This is the count of missing sheets over the branch points that enters the Euler-characteristic form of Riemann–Hurwitz. The ramification divisor of a composite satisfies the chain rule R_{g ∘ f} = R_f + f^* R_g, so ramification degrees satisfy deg R_{g ∘ f} = deg R_f + deg f · deg R_g.

Main declarations

• TauCeti.RiemannSurface.FiniteHolomorphicMap.eventually_codiscrete_localMultiplicity_eq_one and TauCeti.RiemannSurface.FiniteHolomorphicMap.finite_setOf_one_lt_localMultiplicity: the ramification points of a finite holomorphic map are isolated, and finite on a compact source.
• TauCeti.RiemannSurface.ramificationDivisor: the ramification divisor, with its coefficients TauCeti.RiemannSurface.coeff_ramificationDivisor and its support TauCeti.RiemannSurface.support_ramificationDivisor.
• TauCeti.RiemannSurface.ramificationDegree: the ramification degree, and TauCeti.RiemannSurface.degree_ramificationDivisor: it is the degree of the ramification divisor.
• TauCeti.RiemannSurface.card_fiber_add_sum_localMultiplicity_sub_one and TauCeti.RiemannSurface.coeff_pushforward_ramificationDivisor: the fibre count.
• TauCeti.RiemannSurface.ramificationDivisor_comp and TauCeti.RiemannSurface.ramificationDegree_comp: the chain rule for composites.

References

• Otto Forster, Lectures on Riemann Surfaces, Graduate Texts in Mathematics 81, Springer, 1981, §17 (the total branching order and the Riemann–Hurwitz formula).
• Rick Miranda, Algebraic Curves and Riemann Surfaces, Graduate Studies in Mathematics 5, American Mathematical Society, 1995, Chapter II §4 (ramification and branch points, Hurwitz's formula).

noncomputable def TauCeti.RiemannSurface.ramificationDegree {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) : ℕ

The ramification degree of a map f : X → Y of Riemann surfaces: the sum of localMultiplicity f x - 1 over all points x. For a finite holomorphic map from a compact connected Riemann surface the sum is finite and is the degree of the ramification divisor (TauCeti.RiemannSurface.degree_ramificationDivisor); by the convention for finsum, it is 0 when infinitely many points have local multiplicity at least 2.

Equations

• TauCeti.RiemannSurface.ramificationDegree f = ∑ᶠ (x : X), (TauCeti.RiemannSurface.localMultiplicity f x - 1)

theorem TauCeti.RiemannSurface.ramificationDegree_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) : ramificationDegree f = ∑ᶠ (x : X), (localMultiplicity f x - 1)

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.eventually_codiscrete_localMultiplicity_eq_one {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) : ∀ᶠ (x : X) in Filter.codiscrete X, localMultiplicity (↑f) x = 1

The ramification points of a finite holomorphic map from a connected Riemann surface are isolated: the local multiplicity is 1 away from a closed discrete set.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.finite_setOf_one_lt_localMultiplicity {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) : {x : X | 1 < localMultiplicity (↑f) x}.Finite

A finite holomorphic map from a compact connected Riemann surface has only finitely many ramification points.

noncomputable def TauCeti.RiemannSurface.ramificationDivisor {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) : AlgebraicGeometry.WeilDivisor X

The ramification divisor ∑ₓ (e_x - 1) [x] of a finite holomorphic map from a compact connected Riemann surface, where e_x is the local multiplicity at x. Its support is the finite set of ramification points (TauCeti.RiemannSurface.support_ramificationDivisor).

Equations

• TauCeti.RiemannSurface.ramificationDivisor f = Finsupp.ofSupportFinite (fun (x : X) => ↑(TauCeti.RiemannSurface.localMultiplicity (↑f) x) - 1) ⋯

@[simp]

theorem TauCeti.RiemannSurface.coeff_ramificationDivisor {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) (x : X) : (ramificationDivisor f).coeff x = ↑(localMultiplicity (↑f) x) - 1

The coefficient of the ramification divisor at x is the local multiplicity minus one.

theorem TauCeti.RiemannSurface.isEffective_ramificationDivisor {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) : (ramificationDivisor f).IsEffective

The ramification divisor is effective.

@[simp]

theorem TauCeti.RiemannSurface.support_ramificationDivisor {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) : ↑(ramificationDivisor f).support = {x : X | 1 < localMultiplicity (↑f) x}

The support of the ramification divisor is the set of ramification points.

theorem TauCeti.RiemannSurface.ramificationDivisor_eq_zero_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] (f : FiniteHolomorphicMap X Y) : ramificationDivisor f = 0 ↔ ∀ (x : X), localMultiplicity (↑f) x = 1

A finite holomorphic map is unramified, that is, has local multiplicity 1 everywhere, exactly when its ramification divisor vanishes.

@[simp]

theorem TauCeti.RiemannSurface.degree_ramificationDivisor {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) : AlgebraicGeometry.WeilDivisor.degree (ramificationDivisor f) = ↑(ramificationDegree ↑f)

The ramification degree of a finite holomorphic map from a compact connected Riemann surface is the degree of its ramification divisor.

theorem TauCeti.RiemannSurface.card_fiber_add_sum_localMultiplicity_sub_one {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 + ∑ x ∈ ⋯.toFinset, (localMultiplicity (↑f) x - 1) = degree ↑f

The fibre count. Over every point y of a connected target, the number of points of the fibre plus the sum of e_x - 1 over the fibre is the degree of a finite holomorphic map from a compact connected Riemann surface.

theorem TauCeti.RiemannSurface.coeff_pushforward_ramificationDivisor {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) : ((AlgebraicGeometry.WeilDivisor.pushforward ↑f) (ramificationDivisor f)).coeff y = ↑(degree ↑f) - ↑⋯.toFinset.card

The pushforward of the ramification divisor has coefficient deg f - #f⁻¹(y) at y: it counts the sheets of f that come together over y.

theorem TauCeti.RiemannSurface.ramificationDivisor_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] [T2Space X] [T2Space Y] [PreconnectedSpace Y] [CompactSpace Y] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : ramificationDivisor (g.comp f) = ramificationDivisor f + (divisorPullback f) (ramificationDivisor g)

The chain rule for ramification divisors. The ramification divisor of a composite of finite holomorphic maps between compact connected Riemann surfaces is R_{g ∘ f} = R_f + f^* R_g: at x this is e_g e_f - 1 = (e_f - 1) + e_f (e_g - 1).

theorem TauCeti.RiemannSurface.ramificationDegree_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [PreconnectedSpace X] [CompactSpace X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] [T2Space X] [T2Space Y] [PreconnectedSpace Y] [CompactSpace Y] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : ramificationDegree ↑(g.comp f) = ramificationDegree ↑f + degree ↑f * ramificationDegree ↑g

The ramification degree of a composite of finite holomorphic maps between compact connected Riemann surfaces is deg R_f + deg f · deg R_g.