The degree of a holomorphic map between compact Riemann surfaces

Let f : X → Y be a holomorphic map between Riemann surfaces which is constant near no point of X. Its fibre sum at y : Y is the number of preimages of y counted with local multiplicities, TauCeti.RiemannSurface.fiberMultiplicitySum f y = ∑ᶠ x ∈ f ⁻¹' {y}, localMultiplicity f x. When X is compact every fibre is finite, and the fibre sum is a locally constant function of y: the local fibre count exists_nhds_localMultiplicity_fiber_sum gives, at each of the finitely many points of a fibre, a neighbourhood on which nearby fibres carry exactly the multiplicity of that point, while compactness of the complement of these neighbourhoods keeps nearby fibres from having any further points. Over a connected Y the fibre sum is therefore the same at every point, and this common value is the degree TauCeti.RiemannSurface.degree f. The degree dominates every local multiplicity and is multiplicative under composition; when X is nonempty (so that some fibre sum is nonzero) it is positive and forces f to be surjective. Nonconstancy of the composite of two such maps comes from the open mapping theorem for Riemann surfaces, TauCeti.RiemannSurface.not_eventuallyConst_comp in TauCeti.Analysis.Complex.RiemannSurface.OpenMapping.

Nonconstancy is spelled pointwise, as ∀ x, ¬ EventuallyConst f (𝓝 x), exactly as in the local fibre count: this is the hypothesis the arguments use. The degree is defined for every map f : X → Y as the supremum of its fibre sums, so that no point of Y needs to be chosen; for a map with constant fibre sums this is that constant, and for other maps the value is junk.

The bundled carrier TauCeti.RiemannSurface.FiniteHolomorphicMap X Y collects a holomorphic map which takes two distinct values and has finite fibres. On a connected X the identity theorem (TauCeti.RiemannSurface.not_eventuallyConst_of_ne in TauCeti.Analysis.Complex.RiemannSurface.IdentityTheorem) turns the two distinct values into pointwise nonconstancy, so the results above apply to a finite holomorphic map with no side hypotheses, and between compact connected Riemann surfaces every nonconstant holomorphic map is a finite holomorphic map.

Main declarations

• TauCeti.RiemannSurface.finite_preimage_singleton: fibre finiteness over a compact source.
• TauCeti.RiemannSurface.fiberMultiplicitySum: the fibre sum of local multiplicities, and TauCeti.RiemannSurface.eventually_fiberMultiplicitySum_eq, its local constancy.
• TauCeti.RiemannSurface.degree: the degree, with TauCeti.RiemannSurface.fiberMultiplicitySum_eq_degree saying that every fibre sum over a connected target equals it, TauCeti.RiemannSurface.degree_pos_of_forall_not_eventuallyConst, TauCeti.RiemannSurface.surjective_of_forall_not_eventuallyConst and TauCeti.RiemannSurface.degree_comp_of_forall_not_eventuallyConst, for maps carrying the pointwise nonconstancy hypothesis.
• TauCeti.RiemannSurface.FiniteHolomorphicMap: the bundled finite holomorphic maps, with TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMDifferentiable and TauCeti.RiemannSurface.FiniteHolomorphicMap.comp, and the degree API on them with no side hypotheses: TauCeti.RiemannSurface.localMultiplicity_pos, TauCeti.RiemannSurface.degree_eq_fiber_sum, TauCeti.RiemannSurface.degree_pos, TauCeti.RiemannSurface.localMultiplicity_comp, TauCeti.RiemannSurface.degree_comp and TauCeti.RiemannSurface.biholomorphOfDegreeEqOne, the biholomorphism constructed from a degree-one map.

References

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

The fibre sum

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

The number of preimages of y under f, counted with local multiplicities: the sum of TauCeti.RiemannSurface.localMultiplicity f x over the fibre f ⁻¹' {y}. Over a finite fibre it is a finite sum (TauCeti.RiemannSurface.fiberMultiplicitySum_eq_sum); by the convention for finsum, it is 0 when infinitely many points of the fibre have nonzero local multiplicity.

For a holomorphic f on a compact Riemann surface which is constant near no point, this is a locally constant function of y (TauCeti.RiemannSurface.eventually_fiberMultiplicitySum_eq), and over a connected target it is the degree of f (TauCeti.RiemannSurface.fiberMultiplicitySum_eq_degree).

Equations

• TauCeti.RiemannSurface.fiberMultiplicitySum f y = ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {y}), TauCeti.RiemannSurface.localMultiplicity f x

theorem TauCeti.RiemannSurface.fiberMultiplicitySum_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) (y : Y) : fiberMultiplicitySum f y = ∑ᶠ (x : X) (_ : x ∈ f ⁻¹' {y}), localMultiplicity f x

theorem TauCeti.RiemannSurface.fiberMultiplicitySum_eq_sum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {y : Y} (hy : (f ⁻¹' {y}).Finite) : fiberMultiplicitySum f y = ∑ x ∈ hy.toFinset, localMultiplicity f x

Over a finite fibre, the fibre sum is a finite sum.

theorem TauCeti.RiemannSurface.localMultiplicity_le_fiberMultiplicitySum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {x : X} {y : Y} (hy : (f ⁻¹' {y}).Finite) (hx : f x = y) : localMultiplicity f x ≤ fiberMultiplicitySum f y

Each local multiplicity at a point of a finite fibre is at most the fibre sum.

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

The degree of a map f : X → Y between Riemann surfaces: the supremum of its fibre sums TauCeti.RiemannSurface.fiberMultiplicitySum f y. For f holomorphic and constant near no point of a compact X, with Y connected, every fibre sum equals the degree (TauCeti.RiemannSurface.fiberMultiplicitySum_eq_degree): the degree is the number of preimages of any point, counted with local multiplicities. The supremum only avoids choosing a point of Y; for maps whose fibre sums are not constant the value is junk.

Equations

• TauCeti.RiemannSurface.degree f = ⨆ (y : Y), TauCeti.RiemannSurface.fiberMultiplicitySum f y

theorem TauCeti.RiemannSurface.degree_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (f : X → Y) : degree f = ⨆ (y : Y), fiberMultiplicitySum f y

Finite holomorphic maps

structure TauCeti.RiemannSurface.FiniteHolomorphicMap (X : Type u_4) (Y : Type u_5) [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] : Type (max u_4 u_5)

A finite holomorphic map between Riemann surfaces: a holomorphic map which takes two distinct values and has finite fibres. On a connected source it is constant near no point by the identity theorem (TauCeti.RiemannSurface.FiniteHolomorphicMap.not_eventuallyConst), so the degree theory of this file applies to it with no side hypotheses; between compact connected Riemann surfaces every nonconstant holomorphic map is finite (TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMDifferentiable).

• toFun : X → Y

  The underlying map.

• holomorphic : MDiff ↑self

  The map is holomorphic.

• nonconstant : ∃ (x : X) (x' : X), ↑self x ≠ ↑self x'

  The map takes two distinct values.

• finite_fiber (y : Y) : (↑self ⁻¹' {y}).Finite

  Every fibre of the map is finite.

@[instance_reducible]

instance TauCeti.RiemannSurface.FiniteHolomorphicMap.instCoeFunForall {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] : CoeFun (FiniteHolomorphicMap X Y) fun (x : FiniteHolomorphicMap X Y) => X → Y

Equations

• TauCeti.RiemannSurface.FiniteHolomorphicMap.instCoeFunForall = { coe := TauCeti.RiemannSurface.FiniteHolomorphicMap.toFun }

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.ext {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f g : FiniteHolomorphicMap X Y} (h : ∀ (x : X), ↑f x = ↑g x) : f = g

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.ext_iff {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f g : FiniteHolomorphicMap X Y} : f = g ↔ ∀ (x : X), ↑f x = ↑g x

Fibre finiteness

theorem TauCeti.RiemannSurface.finite_preimage_singleton {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T1Space Y] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) (y : Y) : (f ⁻¹' {y}).Finite

Finiteness of fibres. A holomorphic map from a compact Riemann surface which is constant near no point has finite fibres: each fibre is compact, and each of its points has a neighbourhood containing no other point of the fibre.

Local constancy of the fibre sum

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

Local constancy of the fibre sum. For a holomorphic map from a compact Riemann surface which is constant near no point, the fibre sum of local multiplicities is the same at every point near y as at y.

theorem TauCeti.RiemannSurface.isLocallyConstant_fiberMultiplicitySum {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [T2Space Y] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) : IsLocallyConstant (fiberMultiplicitySum f)

For a holomorphic map from a compact Riemann surface which is constant near no point, the fibre sum of local multiplicities is a locally constant function on the target.

The degree

theorem TauCeti.RiemannSurface.fiberMultiplicitySum_eq_degree {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) (y : Y) : fiberMultiplicitySum f y = degree f

Fibre independence of the degree. For a holomorphic map from a compact Riemann surface to a connected Riemann surface which is constant near no point, the number of preimages of any point counted with local multiplicities is the degree.

theorem TauCeti.RiemannSurface.localMultiplicity_le_degree_of_forall_not_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) (x : X) : localMultiplicity f x ≤ degree f

Every local multiplicity of a holomorphic map from a compact Riemann surface to a connected Riemann surface which is constant near no point is at most the degree.

theorem TauCeti.RiemannSurface.degree_pos_of_forall_not_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) [Nonempty X] : 0 < degree f

Positivity of the degree. A holomorphic map from a nonempty compact Riemann surface to a connected Riemann surface which is constant near no point has positive degree.

theorem TauCeti.RiemannSurface.surjective_of_forall_not_eventuallyConst {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) [Nonempty X] : Function.Surjective f

Surjectivity. A holomorphic map from a nonempty compact Riemann surface to a connected Riemann surface which is constant near no point is surjective: its positive degree is the fibre sum over every point, so no fibre is empty.

Composition

theorem TauCeti.RiemannSurface.degree_comp_of_forall_not_eventuallyConst {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {f : X → Y} {g : Y → Z} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [TopologicalSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] [CompactSpace X] [T2Space X] [CompactSpace Y] [T2Space Y] [PreconnectedSpace Y] [T2Space Z] [PreconnectedSpace Z] (hf : MDiff f) (hne : ∀ (x : X), ¬Filter.EventuallyConst f (nhds x)) (hg : MDiff g) (hneg : ∀ (y : Y), ¬Filter.EventuallyConst g (nhds y)) : degree (g ∘ f) = degree g * degree f

Multiplicativity of the degree. For holomorphic maps f : X → Y and g : Y → Z of compact Riemann surfaces with connected targets, both constant near no point, the degree of g ∘ f is the product of the degrees: the fibre of g ∘ f over z is the disjoint union of the fibres of f over the points of the fibre of g over z, and the local multiplicities multiply.

The degree of a finite holomorphic map

The results above, restated on TauCeti.RiemannSurface.FiniteHolomorphicMap with no side hypotheses: on a connected source the identity theorem supplies the pointwise nonconstancy. The statements about degree and localMultiplicity keep the names of the theorems they restate and live in the namespace of that head symbol; the theorems whose head symbol is generic (Function.Surjective, Filter.EventuallyConst, the composite) live in the carrier's namespace.

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.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 : FiniteHolomorphicMap X Y) [PreconnectedSpace X] (x : X) : ¬Filter.EventuallyConst (↑f) (nhds x)

A finite holomorphic map from a connected Riemann surface is constant near no point: this is the identity theorem.

theorem TauCeti.RiemannSurface.localMultiplicity_pos {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 : FiniteHolomorphicMap X Y) [PreconnectedSpace X] (x : X) : 0 < localMultiplicity (↑f) x

The local multiplicity of a finite holomorphic map from a connected Riemann surface is positive at every point.

def TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMDifferentiable {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [PreconnectedSpace X] [T1Space Y] {f : X → Y} (hf : MDiff f) (hne : ∃ (x : X) (x' : X), f x ≠ f x') : FiniteHolomorphicMap X Y

A holomorphic map from a compact connected Riemann surface which takes two distinct values is a finite holomorphic map: its fibres are finite by TauCeti.RiemannSurface.finite_preimage_singleton.

Equations

• TauCeti.RiemannSurface.FiniteHolomorphicMap.ofMDifferentiable hf hne = { toFun := f, holomorphic := hf, nonconstant := hne, finite_fiber := ⋯ }

@[simp]

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.coe_ofMDifferentiable {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [PreconnectedSpace X] [T1Space Y] {f : X → Y} (hf : MDiff f) (hne : ∃ (x : X) (x' : X), f x ≠ f x') : ↑(ofMDifferentiable hf hne) = f

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.surjective {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 : FiniteHolomorphicMap X Y) [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] : Function.Surjective ↑f

A finite holomorphic map from a compact connected Riemann surface to a connected Riemann surface is surjective.

theorem TauCeti.RiemannSurface.degree_eq_fiber_sum {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 : FiniteHolomorphicMap X Y) [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] (y : Y) : degree ↑f = ∑ x ∈ ⋯.toFinset, localMultiplicity (↑f) x

Fibre independence of the degree, for a finite holomorphic map from a compact connected Riemann surface to a connected Riemann surface: the degree is the sum of the local multiplicities over any fibre.

theorem TauCeti.RiemannSurface.localMultiplicity_le_degree {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 : FiniteHolomorphicMap X Y) [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] (x : X) : localMultiplicity (↑f) x ≤ degree ↑f

Every local multiplicity of a finite holomorphic map from a compact connected Riemann surface to a connected Riemann surface is at most its degree.

theorem TauCeti.RiemannSurface.degree_pos {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 : FiniteHolomorphicMap X Y) [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] : 0 < degree ↑f

Positivity of the degree of a finite holomorphic map from a compact connected Riemann surface to a connected Riemann surface.

def TauCeti.RiemannSurface.FiniteHolomorphicMap.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] [TopologicalSpace Z] [ChartedSpace ℂ Z] [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : FiniteHolomorphicMap X Z

The composite of finite holomorphic maps, for a compact connected source and a connected middle surface: the composite takes two distinct values because the first map is surjective, and its fibres are finite unions of finite fibres.

Equations

• g.comp f = { toFun := ↑g ∘ ↑f, holomorphic := ⋯, nonconstant := ⋯, finite_fiber := ⋯ }

@[simp]

theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.coe_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] [TopologicalSpace Z] [ChartedSpace ℂ Z] [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : ↑(g.comp f) = ↑g ∘ ↑f

theorem TauCeti.RiemannSurface.localMultiplicity_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] [TopologicalSpace Z] [ChartedSpace ℂ Z] [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) (x : X) : localMultiplicity (↑(g.comp f)) x = localMultiplicity (↑g) (↑f x) * localMultiplicity (↑f) x

Multiplicativity of the local multiplicity for finite holomorphic maps: the local multiplicity of g.comp f at x is the product of that of g at f x and that of f at x. The statement for maps, with holomorphy near the two points as hypotheses, is TauCeti.RiemannSurface.localMultiplicity_comp_of_eventually_mdifferentiableAt.

theorem TauCeti.RiemannSurface.degree_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] [TopologicalSpace Z] [ChartedSpace ℂ Z] [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] [CompactSpace Y] [T2Space Z] [PreconnectedSpace Z] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : degree ↑(g.comp f) = degree ↑g * degree ↑f

Multiplicativity of the degree for finite holomorphic maps f : X → Y and g : Y → Z with X and Y compact and connected and Z connected.

noncomputable def TauCeti.RiemannSurface.biholomorphOfDegreeEqOne {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) (hf : degree ↑f = 1) : Diffeomorph (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) X Y ↑⊤

A degree-one map is a biholomorphism: construct a biholomorphism from a finite holomorphic map of degree one between compact connected Riemann surfaces.

Equations

• TauCeti.RiemannSurface.biholomorphOfDegreeEqOne f hf = { toEquiv := (IsHomeomorph.homeomorph ↑f ⋯).toEquiv, contMDiff_toFun := ⋯, contMDiff_invFun := ⋯ }

@[simp]

theorem TauCeti.RiemannSurface.biholomorphOfDegreeEqOne_toFun {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] [CompactSpace X] [T2Space X] [PreconnectedSpace X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) (hf : degree ↑f = 1) : ⇑(biholomorphOfDegreeEqOne f hf) = ↑f