23.4. ResidueTheorem.OmegaFactorization🔗

Jacobians.ResidueTheorem.OmegaFactorization — source

resAt_eq_zero_of_analyticAt

Res_c(f) = 0 for f analytic AT c (point version of resAt_eq_zero_of_differentiableOn_ball; analyticity spreads to a small ball).

theorem resAt_eq_zero_of_analyticAt {f : ℂ → ℂ} {c : ℂ} (hf : AnalyticAt ℂ f c) :
    resAt f c = 0

tendsto_chart_nhdsNE

The canonical chart maps the punctured neighbourhood filter of its centre to the punctured neighbourhood filter of the centre's image (continuity + injectivity on the source).

theorem tendsto_chart_nhdsNE {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (x : X) :
    Tendsto (chartAt (H := ℂ) x) (𝓝[≠] x) (𝓝[≠] ((chartAt (H := ℂ) x) x))

tendsto_chart_symm_nhdsNE

The inverse canonical chart maps the punctured neighbourhood filter of the centre's image to the punctured neighbourhood filter of the centre.

theorem tendsto_chart_symm_nhdsNE {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (x : X) :
    Tendsto (chartAt (H := ℂ) x).symm (𝓝[≠] ((chartAt (H := ℂ) x) x)) (𝓝[≠] x)

eventually_nhdsNE_notMem_of_finite

A finite set is eventually avoided on every punctured neighbourhood (T1 space).

theorem eventually_nhdsNE_notMem_of_finite {Y : Type*} [TopologicalSpace Y] [T1Space Y]
    {S : Set Y} (hS : S.Finite) (x : Y) : ∀ᶠ y in 𝓝[≠] x, y ∉ S

exists_holomorphicOneForm_ne_zero

Positive genus yields a nonzero holomorphic 1-form (genus X = dim_ℂ Ω(X) > 0).

theorem exists_holomorphicOneForm_ne_zero (hgenus : 0 < genus X) :
    ∃ ω₀ : HolomorphicOneForms X, ω₀ ≠ 0

localRep_eq_zero_of_toFun_eq_zero

A vanishing 1-form value kills every local representative (the representative is the form paired with a tangent vector).

theorem localRep_eq_zero_of_toFun_eq_zero (α : HolomorphicOneForms X) (x₀ : X) {y : X}
    (h : α.toFun y = 0) : Jacobians.Montel.localRep α x₀ y = 0

toFun_eq_zero_of_localRep_eq_zero

Conversely, on the chart source a vanishing local representative kills the 1-form value: the transported unit tangent spans the 1-dimensional fibre (off-centre generalization of the exists_localRep_self_ne_zero argument).

theorem toFun_eq_zero_of_localRep_eq_zero (α : HolomorphicOneForms X) {x₀ y : X}
    (hy : y ∈ (chartAt (H := ℂ) x₀).source)
    (h : Jacobians.Montel.localRep α x₀ y = 0) : α.toFun y = 0

toFun_eventually_zero_of_coeffAt_eventually_zero

Chart-side eventual vanishing of the coefficient pushes to manifold-side eventual vanishing of the 1-form (the fibres are 1-dimensional, spanned by the chart tangent).

theorem toFun_eventually_zero_of_coeffAt_eventually_zero (α : HolomorphicOneForms X) {p : X}
    (h : ∀ᶠ w in 𝓝 ((chartAt (H := ℂ) p) p), coeffAt α p w = 0) :
    ∀ᶠ y in 𝓝 p, α.toFun y = 0

eq_zero_of_coeffAt_eventually_zero

Identity theorem for holomorphic 1-forms (global propagation). If the canonical-chart coefficient of α vanishes on a neighbourhood of one chart centre, then α = 0 — the set where α vanishes locally is clopen (openness is trivial; closedness is the one-variable isolated-zeros dichotomy applied to the analytic coefficient), and X is connected.

theorem eq_zero_of_coeffAt_eventually_zero (α : HolomorphicOneForms X) {x : X}
    (h : ∀ᶠ w in 𝓝 ((chartAt (H := ℂ) x) x), coeffAt α x w = 0) : α = 0

coeffAt_eventually_ne_zero

Isolated zeros of a nonzero holomorphic 1-form: at every chart centre, the canonical-chart coefficient is eventually nonzero on the punctured neighbourhood.

theorem coeffAt_eventually_ne_zero (α : HolomorphicOneForms X) (hα : α ≠ 0) (x : X) :
    ∀ᶠ w in 𝓝[≠] ((chartAt (H := ℂ) x) x), coeffAt α x w ≠ 0

finite_localRep_self_eq_zero

The zero set of a nonzero holomorphic 1-form is FINITE (the div(ω₀) ≥ 0 finiteness atom: zeros are isolated by coeffAt_eventually_ne_zero + the chart-transition comparison, and X is compact).

theorem finite_localRep_self_eq_zero (α : HolomorphicOneForms X) (hα : α ≠ 0) :
    {x : X | Jacobians.Montel.localRep α x x = 0}.Finite

chartTransitionFactor_eq_deriv_transition

chartTransitionFactor = derivative of the chart transition. The Montel tangent-bundle transition factor at y (converting x₀'-chart tangent coordinates to x₀-chart ones) is the honest one-variable derivative of the chart-transition map chartAt x₀ ∘ (chartAt x₀').symm at chartAt x₀' y. Unwinds tangentBundleCore_coordChange_achart; this is the bridge that makes the dg₀-coefficient (chain rule) and the ω₀-coefficient (localRep_chart_transition) transform with the SAME factor.

theorem chartTransitionFactor_eq_deriv_transition {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {x₀ x₀' y : X}
    (h' : y ∈ (chartAt (H := ℂ) x₀').source) (h : y ∈ (chartAt (H := ℂ) x₀).source) :
    Jacobians.Montel.chartTransitionFactor x₀ x₀' y
      = deriv ((chartAt (H := ℂ) x₀) ∘ (chartAt (H := ℂ) x₀').symm)
          ((chartAt (H := ℂ) x₀') y)

derivQuotient

The quotient dg₀/ω₀ as a function on X (Miranda Ch. VI p. 186: any meromorphic 1-form is a meromorphic-function multiple of a fixed nonzero ω₀). Value at y: the dg₀-coefficient deriv (g₀ ∘ chart_y⁻¹) over the ω₀-coefficient localRep ω₀ y, both read in y's OWN canonical chart at its centre (junk 0 where the denominator vanishes, matching repo div-conventions).

noncomputable def derivQuotient (ω₀ : HolomorphicOneForms X) (g₀ : MeromorphicFunction X) :
    X → ℂ

derivQuotient_eventuallyEq_chart

Chart-coherence of the quotient. Near any chart centre chartAt x x (off the centre), the pullback of derivQuotient ω₀ g₀ agrees with the single-chart quotient deriv (g₀ ∘ chart_x⁻¹) / coeffAt ω₀ x: at each nearby point both the numerator (chain rule) and the denominator (localRep_chart_transition) pick up the SAME nonzero transition-derivative factor (chartTransitionFactor_eq_deriv_transition), which cancels in the ratio. The finitely many points where g₀'s own-chart pullback fails honest analyticity are avoided eventually (MeromorphicFunction.finite_nonAnalyticAt).

theorem derivQuotient_eventuallyEq_chart (ω₀ : HolomorphicOneForms X)
    (g₀ : MeromorphicFunction X) (x : X) :
    (fun z => derivQuotient ω₀ g₀ ((chartAt (H := ℂ) x).symm z))
      =ᶠ[𝓝[≠] ((chartAt (H := ℂ) x) x)]
      fun z => deriv (fun w => g₀.toFun ((chartAt (H := ℂ) x).symm w)) z / coeffAt ω₀ x z

isMeromorphic_derivQuotient

The quotient dg₀/ω₀ is globally meromorphic: at each chart centre it agrees off the centre with deriv (g₀ ∘ chart_x⁻¹) / coeffAt ω₀ x (chart-coherence), which is meromorphic by MeromorphicAt.deriv + MeromorphicAt.div, and meromorphy is a punctured-germ invariant.

theorem isMeromorphic_derivQuotient (ω₀ : HolomorphicOneForms X) (g₀ : MeromorphicFunction X) :
    IsMeromorphic X (derivQuotient ω₀ g₀)

derivQuotientFn

The quotient dg₀/ω₀ bundled as a MeromorphicFunction.

noncomputable def derivQuotientFn (ω₀ : HolomorphicOneForms X) (g₀ : MeromorphicFunction X) :
    MeromorphicFunction X

derivQuotientFn_toFun

@[simp] theorem derivQuotientFn_toFun (ω₀ : HolomorphicOneForms X)
    (g₀ : MeromorphicFunction X) :
    (derivQuotientFn ω₀ g₀).toFun = derivQuotient ω₀ g₀