20.4. CanonicalForms.CanonicalFormDifferential🔗

Jacobians.CanonicalForms.CanonicalFormDifferential — source

mfderiv_apply_symmL_eq_deriv

The intrinsic-differential / chart-derivative bridge. For y in the chart source at x where f is MDifferentiableAt, the covector mfderiv f y paired with the spanning tangent vector symmL ℂ y 1 equals the ordinary derivative of the chart pullback f ∘ chart⁻¹ at chart y.

This is the chain rule mfderiv f ∘ mfderiv chart⁻¹ = mfderiv (f ∘ chart⁻¹), with symmL ℂ y = mfderiv chart⁻¹ (chart y) (TangentBundle.symmL_trivializationAt) and mfderiv (f ∘ chart⁻¹) = fderiv on the model space (mfderiv_eq_fderiv).

theorem mfderiv_apply_symmL_eq_deriv {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : X → ℂ)
    {x y : X} (hy : y ∈ (chartAt ℂ x).source)
    (hf : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f y) :
    mfderiv 𝓘(ℂ) 𝓘(ℂ) f y
        ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1)
      = deriv (f ∘ (chartAt ℂ x).symm) ((chartAt ℂ x) y)

mdifferentiableAt_of_differentiableAt_comp

Chart-pullback differentiability ⇒ MDifferentiableAt f. If f ∘ chart⁻¹ is DifferentiableAt at a chart-target point z, then f is MDifferentiableAt at chart⁻¹ z. (For the codomain ℂ the extended chart is the identity, so the manifold-differentiability criterion mdifferentiableAt_iff_of_mem_source is just chart-pullback differentiability.)

theorem mdifferentiableAt_of_differentiableAt_comp {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (f : X → ℂ)
    {x : X} {z : ℂ}
    (hz : z ∈ (chartAt ℂ x).target)
    (hdiff : DifferentiableAt ℂ (f ∘ (chartAt ℂ x).symm) z) :
    MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f ((chartAt ℂ x).symm z)

differentialSection

The underlying cotangent-bundle section of the differential df: x ↦ mfderiv f x.

noncomputable def differentialSection (f : MeromorphicFunction X) : ∀ x, FormFiber X x

formCoeff_differentialSection_eventuallyEq

formCoeff (df) x agrees with the chart-pullback derivative (f ∘ chart⁻¹)' on a punctured neighbourhood of chart x x (precisely where f ∘ chart⁻¹ is analytic, hence f is MDifferentiableAt).

theorem formCoeff_differentialSection_eventuallyEq {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) (x : X) :
    (fun z => deriv (f.toFun ∘ (chartAt ℂ x).symm) z) =ᶠ[𝓝[≠] ((chartAt ℂ x) x)]
      formCoeff (differentialSection f) x

isMeromorphicOneForm_differentialSection

df is a meromorphic 1-form: its chart coefficient is MeromorphicAt because it germ-agrees with (f ∘ chart⁻¹)', the derivative of a meromorphic function (MeromorphicAt.deriv).

theorem isMeromorphicOneForm_differentialSection {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (f : MeromorphicFunction X) :
    IsMeromorphicOneForm (differentialSection f)

differentialForm

The canonical meromorphic 1-form ω₀ = df of a meromorphic function f.

noncomputable def differentialForm (f : MeromorphicFunction X) : MeromorphicOneForm X

formOrderW_differentialForm

formOrderW (df) at x is the meromorphic order of the chart-pullback derivative (f ∘ chart⁻¹)' (via the germ-agreement of formCoeff (df) with it).

theorem formOrderW_differentialForm (f : MeromorphicFunction X) (x : X) :
    (differentialForm f).formOrderW x
      = meromorphicOrderAt (deriv (f.toFun ∘ (chartAt ℂ x).symm)) ((chartAt ℂ x) x)

deriv_eventually_zero_meromorphicOrderAt_nonneg

No pole from a vanishing-derivative germ. If g is meromorphic at z₀ and its derivative vanishes on a punctured neighbourhood of z₀, then g has *no pole* at z₀ (meromorphicOrderAt g z₀ ≥ 0). Proof: were meromorphicOrderAt g z₀ = n < 0, the Laurent form g =ᶠ (·−z₀)ⁿ • G (G analytic, G z₀ ≠ 0) makes deriv g =ᶠ (n·(·−z₀)ⁿ⁻¹)·G + (·−z₀)ⁿ·G', whose order is exactly n − 1 (the first term dominates, as n ≠ 0, G z₀ ≠ 0); but deriv g =ᶠ 0 forces order ⊤ ≠ n − 1. Pure planar complex analysis (mirrors Mathlib's MeromorphicAt.deriv).

theorem deriv_eventually_zero_meromorphicOrderAt_nonneg {g : ℂ → ℂ} {z₀ : ℂ}
    (hg : MeromorphicAt g z₀) (hdz : ∀ᶠ z in 𝓝[≠] z₀, deriv g z = 0) :
    0 ≤ meromorphicOrderAt g z₀

differentialForm_ne_zero

df ≠ 0 for a nonconstant f (Forster §17.4's nontriviality of ω₀ = df). If f is not germ-constant then df's germ is nonzero somewhere. Contrapositive: if formOrderW (df) = ⊤ everywhere, then deriv (f ∘ chart⁻¹) vanishes on a punctured neighbourhood at every point, so f has no pole anywhere (deriv_eventually_zero_meromorphicOrderAt_nonneg), i.e. f ∈ L(0); then f is germ-constant by the repo Liouville germ_eq_const_of_mem_linearSystem_zero.

theorem differentialForm_ne_zero {f : MeromorphicFunction X} (hf : ¬ IsGermConstant f) :
    ∃ x, (differentialForm f).formOrderW x ≠ ⊤

canonicalForm17DataOfDivisor

Assembly of CanonicalForm17Data from f, df ≠ 0, and the canonical divisor K. Given a meromorphic function f (whose df ≠ 0 is supplied by hf : ¬ IsGermConstant f) together with its form-divisor K (a Divisor X with formOrderW (df) x = K x for all x), this is the Forster §17.4 canonical-form datum ω₀ = df, K = div ω₀ (modulo the divisor input).

noncomputable def canonicalForm17DataOfDivisor (f : MeromorphicFunction X)
    (hf : ¬ IsGermConstant f) (K : Divisor X)
    (hK : ∀ x, (differentialForm f).formOrderW x = (K x : WithTop ℤ)) :
    CanonicalForm17Data X where

symmL_frame_change

Frame-change law for the canonical trivialization. The spanning tangent vector symmL_x q 1 (of the canonical trivialization at x, read at q) and symmL_y q 1 (at y) are related by the holomorphic chart-transition derivative: symmL_x q 1 = (chart_y ∘ chart_x⁻¹)' (chart_x q) • symmL_y q 1. This is the chain rule mfderiv (chart_x⁻¹) = mfderiv (chart_y⁻¹) ∘ mfderiv (chart_y ∘ chart_x⁻¹) (symmL_· = mfderiv (chart_·⁻¹)).

theorem symmL_frame_change {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {x y q : X}
    (hqx : q ∈ (chartAt ℂ x).source)
    (hqy : q ∈ (chartAt ℂ y).source) :
    (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ q (1 : ℂ)
      = deriv (chartAt ℂ y ∘ (chartAt ℂ x).symm) ((chartAt ℂ x) q)
          • (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) y).symmL ℂ q (1 : ℂ)

formCoeff_change

The chart-coefficient transformation law. Near chart_z y, the coefficient of α read in the chart at z equals ψ' · (coeff at y ∘ ψ), where ψ = chart_y ∘ chart_z⁻¹ is the chart transition: formCoeff α z (w) = ψ'(w) · formCoeff α y (ψ w). (From symmL_frame_change + covector linearity; the classical c_z = ψ' · c_y law for 1-form coefficients.)

theorem formCoeff_change (α : MeromorphicOneForm X) (z y : X) (hy : y ∈ (chartAt ℂ z).source) :
    formCoeff α.toFun z =ᶠ[𝓝 ((chartAt ℂ z) y)]
      (fun w => deriv (chartAt ℂ y ∘ (chartAt ℂ z).symm) w
          • formCoeff α.toFun y ((chartAt ℂ y ∘ (chartAt ℂ z).symm) w))

formOrderW_chart_invariant

Chart-invariance of formOrderW. The order of α at y (read in the canonical chart at y) equals the meromorphicOrderAt of α's coefficient in the chart at z, at chart_z y. The two coefficients differ by ψ' (non-vanishing holomorphic transition Jacobian) and composition with the biholomorphism ψ, both order-preserving (meromorphicOrderAt_smul, meromorphicOrderAt_comp_of_deriv_ne_zero). This makes the form's zeros/poles a chart-independent set, the key to the finite support of K = div ω₀.

theorem formOrderW_chart_invariant (α : MeromorphicOneForm X) (z y : X)
    (hy : y ∈ (chartAt ℂ z).source) :
    α.formOrderW y = meromorphicOrderAt (formCoeff α.toFun z) ((chartAt ℂ z) y)

planar_order_zero

Isolated zeros/poles of a meromorphic function (planar). A meromorphic g of finite order at c has meromorphicOrderAt g w = 0 for all w on a punctured neighbourhood of c: the Laurent form g =ᶠ (·−c)ⁿ • G (G analytic, G c ≠ 0) is analytic and nonvanishing at every w ≠ c near c. The planar core of MeromorphicFunction.orderAtPoint_isolated_at.

theorem planar_order_zero (g : ℂ → ℂ) (c : ℂ) (hg : MeromorphicAt g c)
    (hne : meromorphicOrderAt g c ≠ ⊤) :
    ∀ᶠ w in 𝓝[≠] c, meromorphicOrderAt g w = 0

formOrderW_isolated

Isolated zeros/poles of a nonzero meromorphic 1-form. If α's germ is nonzero everywhere (formOrderW α ≠ ⊤), then around each z the only point of nonzero order is z itself: in the chart at z the coefficient formCoeff α z is meromorphic of finite order, so its zeros/poles are isolated (planar_order_zero), and formOrderW is chart-invariant.

theorem formOrderW_isolated (α : MeromorphicOneForm X) (hα : ∀ x, α.formOrderW x ≠ ⊤) (z : X) :
    ∃ t ∈ 𝓝 z, ∀ y ∈ t, y ≠ z → α.formOrderW y = 0

exists_form_divisor

The canonical divisor of a nonzero meromorphic 1-form div α. The order function x ↦ (formOrderW α x).untop₀ has finite support (zeros/poles isolated by formOrderW_isolated, finite on the compact X via locallyFinsuppWithin.finiteSupport), and since formOrderW α ≠ ⊤ everywhere the untop₀ loses nothing, so formOrderW α x = (div α) x. The 1-form analog of MeromorphicFunction.div.

theorem exists_form_divisor (α : MeromorphicOneForm X) (hα : ∀ x, α.formOrderW x ≠ ⊤) :
    ∃ K : Divisor X, ∀ x, α.formOrderW x = (K x : WithTop ℤ)

exists_differentialForm_divisor

The canonical divisor K = div (df). The form-divisor of df (a nonzero form, by hf + the form identity theorem), via exists_form_divisor.

theorem exists_differentialForm_divisor (f : MeromorphicFunction X)
    (hf : ∃ x, (differentialForm f).formOrderW x ≠ ⊤) :
    ∃ K : Divisor X, ∀ x, (differentialForm f).formOrderW x = (K x : WithTop ℤ)