Documentation

TauCeti.Analysis.Complex.RiemannSurface.Meromorphic

Meromorphic functions on a Riemann surface and their orders #

Let X be a Riemann surface, that is, a complex manifold modelled on ℂ, and let f : X → E be a function valued in a complex normed space. Reading f in the chart chartAt ℂ x at x gives the function f ∘ (chartAt ℂ x).symm of one complex variable. This file defines f to be meromorphic at x (TauCeti.RiemannSurface.MeromorphicAt) when that representative is meromorphic at chartAt ℂ x x in the sense of Mathlib's MeromorphicAt, and defines the order of f at x (TauCeti.RiemannSurface.meromorphicOrderAt) as the meromorphic order of the representative there, in WithTop ℤ: positive at a zero, negative at a pole, and ⊤ when f vanishes on a punctured neighbourhood of x.

Since the transition maps between charts of the maximal atlas are holomorphic with nowhere vanishing derivative, both notions may be computed in any chart of the maximal atlas at x (TauCeti.RiemannSurface.meromorphicAt_iff_of_mem_maximalAtlas and TauCeti.RiemannSurface.meromorphicOrderAt_eq_of_mem_maximalAtlas); they are invariants of the function, not of the coordinate used to read it.

Pulling a meromorphic function back along a holomorphic map φ : X → Y gives a meromorphic function (TauCeti.RiemannSurface.MeromorphicAt.comp), and when φ is nonconstant near x the order is multiplied by the local multiplicity of φ: ord_x (F ∘ φ) = ord_{φ x} F * localMultiplicity φ x (TauCeti.RiemannSurface.meromorphicOrderAt_comp). This is the formula relating orders of a function upstairs and downstairs along a branched covering.

Main declarations #

References #

Definitions #

source
def TauCeti.RiemannSurface.MeromorphicAt {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] (f : X → E) (x : X) :
Prop

A function f : X → E on a Riemann surface is meromorphic at x if its representative f ∘ (chartAt ℂ x).symm in the preferred chart at x is meromorphic at chartAt ℂ x x. Any chart of the maximal atlas at x gives the same notion (TauCeti.RiemannSurface.meromorphicAt_iff_of_mem_maximalAtlas).

Equations
Instances For
    source
    theorem TauCeti.RiemannSurface.meromorphicAt_def {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] (f : X → E) (x : X) :
    MeromorphicAt f x ↔ _root_.MeromorphicAt (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)
    source
    noncomputable def TauCeti.RiemannSurface.meromorphicOrderAt {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] (f : X → E) (x : X) :
    WithTop ℤ

    The order of a function f : X → E on a Riemann surface at x: the meromorphic order of its representative in the preferred chart at x. It is positive at a zero, negative at a pole, and ⊤ when f vanishes on a punctured neighbourhood of x. Any chart of the maximal atlas at x gives the same value (TauCeti.RiemannSurface.meromorphicOrderAt_eq_of_mem_maximalAtlas). If f is not meromorphic at x the value is the junk value 0, as for meromorphicOrderAt.

    Equations
    Instances For
      source
      theorem TauCeti.RiemannSurface.meromorphicOrderAt_def {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] (f : X → E) (x : X) :
      meromorphicOrderAt f x = _root_.meromorphicOrderAt (f ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)
      source
      theorem TauCeti.RiemannSurface.meromorphicOrderAt_of_not_meromorphicAt {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : X → E} {x : X} (hf : ¬MeromorphicAt f x) :
      meromorphicOrderAt f x = 0

      The order of a function that is not meromorphic at x is the junk value 0.

      Values on a punctured neighbourhood #

      source
      theorem TauCeti.RiemannSurface.MeromorphicAt.congr {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : X → E} {x : X} (hf : MeromorphicAt f x) (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) :
      MeromorphicAt g x

      Being meromorphic at x only depends on the values on a punctured neighbourhood of x.

      source
      theorem TauCeti.RiemannSurface.meromorphicAt_congr {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : X → E} {x : X} (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) :
      MeromorphicAt f x ↔ MeromorphicAt g x

      Functions agreeing on a punctured neighbourhood of x are meromorphic at x together.

      source
      theorem TauCeti.RiemannSurface.meromorphicOrderAt_congr {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f g : X → E} {x : X} (h : f =ᶠ[nhdsWithin x {x}ᶜ] g) :
      meromorphicOrderAt f x = meromorphicOrderAt g x

      The order at x only depends on the values on a punctured neighbourhood of x.

      Chart independence #

      source
      theorem TauCeti.RiemannSurface.meromorphicAt_iff_of_mem_maximalAtlas {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : X → E} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (hx : x ∈ e.source) :
      MeromorphicAt f x ↔ _root_.MeromorphicAt (f ∘ ↑e.symm) (↑e x)

      Chart independence of meromorphy. A function is meromorphic at x exactly when its representative in some (equivalently, any) chart of the maximal atlas at x is meromorphic at the coordinate of x.

      source
      theorem TauCeti.RiemannSurface.meromorphicOrderAt_eq_of_mem_maximalAtlas {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : X → E} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) 1 X) (hx : x ∈ e.source) :
      meromorphicOrderAt f x = _root_.meromorphicOrderAt (f ∘ ↑e.symm) (↑e x)

      Chart independence of the order. The order of a function at x is the meromorphic order of its representative in any chart of the maximal atlas at x.

      source
      theorem TauCeti.RiemannSurface.meromorphicAt_of_eventually_mdifferentiableAt {X : Type u_1} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [NormedAddCommGroup E] [NormedSpace ℂ E] {f : X → E} {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [CompleteSpace E] (hf : ∀ᶠ (y : X) in nhds x, MDiffAt f y) :
      MeromorphicAt f x

      A function holomorphic near x is meromorphic at x.

      Pullback along a holomorphic map #

      source
      theorem TauCeti.RiemannSurface.MeromorphicAt.comp {X : Type u_1} {Y : Type u_2} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [NormedAddCommGroup E] [NormedSpace ℂ E] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {F : Y → E} {φ : X → Y} (hF : MeromorphicAt F (φ x)) (hφ : ∀ᶠ (y : X) in nhds x, MDiffAt φ y) :
      MeromorphicAt (F ∘ φ) x

      Pullback of a meromorphic function. A function meromorphic at φ x, pulled back along a map φ holomorphic near x, is meromorphic at x.

      source
      theorem TauCeti.RiemannSurface.meromorphicOrderAt_comp {X : Type u_1} {Y : Type u_2} {E : Type u_3} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [NormedAddCommGroup E] [NormedSpace ℂ E] {x : X} [IsManifold (modelWithCornersSelf ℂ ℂ) 1 X] [IsManifold (modelWithCornersSelf ℂ ℂ) 1 Y] {F : Y → E} {φ : X → Y} (hF : MeromorphicAt F (φ x)) (hφ : ∀ᶠ (y : X) in nhds x, MDiffAt φ y) (hnc : ¬Filter.EventuallyConst φ (nhds x)) :
      meromorphicOrderAt (F ∘ φ) x = meromorphicOrderAt F (φ x) * ↑(localMultiplicity φ x)

      The order formula for pullbacks. Pulling a function meromorphic at φ x back along a map φ holomorphic and nonconstant near x multiplies its order by the local multiplicity of φ at x.