8.4. ResidueCalculus.FormCoeff🔗

Jacobians.ResidueCalculus.FormCoeff — source

coeffAt

The coefficient of a holomorphic 1-form α read in the canonical chart at a: near a, α = coeffAt α a (z) · dz in the coordinate z = chartAt ℂ a. It is Montel.localRep α a transported to the chart target; analytic by coeffAt_analyticOn.

noncomputable def coeffAt (α : HolomorphicOneForms X) (a : X) : ℂ → ℂ

coeffAt_analyticOn

coeffAt α a is analytic on the chart target (reuse of the Montel analyticity bridge).

theorem coeffAt_analyticOn (α : HolomorphicOneForms X) (a : X) :
    AnalyticOn ℂ (coeffAt α a) (chartAt ℂ a).target

coeffAt_analyticAt

coeffAt α a is analytic at the chart image of any point of the chart source.

theorem coeffAt_analyticAt (α : HolomorphicOneForms X) (a : X) {z : ℂ}
    (hz : z ∈ (chartAt ℂ a).target) :
    AnalyticAt ℂ (coeffAt α a) z

formFnResidue

The residue at a of the meromorphic 1-form α·g (a holomorphic form α times a function g : X → ℂ), computed in the canonical chart: there α·g = (coeffAt α a · (g ∘ chart.symm)) · dz, so the residue is resAt of that coefficient at the chart image of a.

noncomputable def formFnResidue (α : HolomorphicOneForms X) (g : X → ℂ) (a : X) : ℂ

formFnResidue_eq_zero_of_analyticAt

Res(holo) = 0. If g's chart-pullback is holomorphic at a (so α·g is holomorphic at a, no pole), the local residue vanishes.

theorem formFnResidue_eq_zero_of_analyticAt (α : HolomorphicOneForms X) (g : X → ℂ) (a : X)
    (hg : AnalyticAt ℂ (fun z => g ((chartAt ℂ a).symm z)) ((chartAt ℂ a) a)) :
    formFnResidue α g a = 0

exists_localRep_self_ne_zero

A nonzero holomorphic 1-form has a nonzero coefficient at its own chart centre. Needed to place the dz/z pole in Forster's §17.6 injectivity witness. (The coefficient localRep α a a is α paired with the unit coordinate tangent at a; that tangent spans the 1-dim fibre, so if every such pairing vanished, α would be the zero section.)

theorem exists_localRep_self_ne_zero (α : HolomorphicOneForms X) (hα : α ≠ 0) :
    ∃ a : X, Jacobians.Montel.localRep α a a ≠ 0

coeffAt_chartCenter

The coefficient at the chart centre is the centred local representative: coeffAt α a (chartAt a a) = localRep α a a.

theorem coeffAt_chartCenter (α : HolomorphicOneForms X) (a : X) :
    coeffAt α a ((chartAt ℂ a) a) = Jacobians.Montel.localRep α a a