6.42. MappingDegree.MeromorphicDivisor🔗

Jacobians.MappingDegree.MeromorphicDivisor — source

orderFun

The integer-valued order function of a meromorphic function on a complex manifold: (mmeromorphicOrderAt I f x).untop₀. Positive at zeros, negative at poles, 0 at regular non-zero points. Under the hypothesis hf0 (no germ is identically zero), the value is also 0 at points where mmeromorphicOrderAt I f x = ⊤, but those points do not exist by hf0.

def orderFun (I : ModelWithCorners ℂ ℂ ℂ) (f : X → ℂ) (x : X) : ℤ

divisor

The order divisor of a meromorphic function f on a complex manifold, valued in ℤ (positive at zeros, negative at poles, 0 elsewhere). The locallyFinsuppWithin Set.univ packaging encodes the local-finiteness statement that, for a non-identically-zero meromorphic function, the set {x | mmeromorphicOrderAt I f x ≠ 0} is locally finite (in particular has no accumulation point in any chart).

The hypothesis hf0 : ∀ x, mmeromorphicOrderAt I f x ≠ ⊤ says that no germ of f is identically zero; it is the standard hypothesis under which the order divisor is a well-defined locally-finite object.

Construction: pull f back to each canonical chart, invoke mathlib's MeromorphicOn.divisor (whose local-finiteness comes from MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top), and transport the local-finite-support neighborhood through the chart map. Chart-independence is handled by mmeromorphicOrderAt_eq_of_isManifold.

def divisor
    (I : ModelWithCorners ℂ ℂ ℂ)
    (f : X → ℂ)
    (hf : MMeromorphicOn I f Set.univ)
    (hf0 : ∀ x, mmeromorphicOrderAt I f x ≠ ⊤) :
    Function.locallyFinsuppWithin (Set.univ : Set X) ℤ where