Documentation

TauCeti.Analysis.Complex.RiemannSurface.Branch.Values

Coverings away from branch values #

For a finite holomorphic map of Riemann surfaces with connected target, 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. Local multiplicities multiply along composites, so the branch values of g ∘ f are the images under g of the branch values of f together with the branch values of g.

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 #

References #

The covering construction uses Mathlib's IsClosedMap.isCoveringMapOn_of_isLocalHomeomorphOn.

source
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.

Instances For
    source
    @[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.

    source
    @[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] (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.

    source
    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] (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.

    source
    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] [CompactSpace X] (f : FiniteHolomorphicMap X Y) :
    f.branchValues.Finite

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

    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] [CompactSpace X] (f : FiniteHolomorphicMap X Y) :
    IsClosed f.branchValues

    The branch values form a closed set.

    source
    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] [CompactSpace X] (f : FiniteHolomorphicMap X Y) :
    IsOpen f.branchValuesᶜ

    The complement of the branch values is open.

    source
    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] [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.

    source
    theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.isCoveringMap_restrictPreimage_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] [CompactSpace X] [T2Space X] [T2Space Y] (f : FiniteHolomorphicMap X Y) {S : Set Y} (hS : f.branchValues ⊆ S) :
    IsCoveringMap (Sᶜ.restrictPreimage ↑f)

    Deleting a set containing every branch value, and its preimage, gives an ordinary covering map.

    source
    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] [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.

    source
    theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.ncard_fiber_restrictPreimage_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] [CompactSpace X] [T2Space X] [T2Space Y] [PreconnectedSpace Y] (f : FiniteHolomorphicMap X Y) {S : Set Y} (hS : f.branchValues ⊆ S) (y : ↑Sᶜ) :
    (Sᶜ.restrictPreimage ↑f ⁻¹' {y}).ncard = degree ↑f

    Every fibre of the covering obtained by deleting a set containing every branch value has cardinality equal to the analytic degree of the original map.

    source
    theorem TauCeti.RiemannSurface.FiniteHolomorphicMap.branchValues_comp {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 Y] [PreconnectedSpace Y] {Z : Type u_3} [TopologicalSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Z] (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) :
    (g.comp f).branchValues = ↑g '' f.branchValues ∪ g.branchValues

    Branch values of a composite: for finite holomorphic maps f : X → Y and g : Y → Z, with X compact and Y connected, the branch values of g ∘ f are the images under g of the branch values of f together with the branch values of g.