30.9. Abel.AbelLogDbar🔗

Jacobians.Abel.AbelLogDbar — source

exists_smoothCFunction_eventuallyEq

Bump-glued global extension: a function smooth on an open neighbourhood of a agrees near a with a global SmoothCFunctions. (Planar bump in the chart at a × the chart read, lifted by exists_smoothLift_of_chartFun.)

theorem exists_smoothCFunction_eventuallyEq {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {w : X → ℂ}
    {V : Set X} (hV : IsOpen V)
    {a : X} (ha : a ∈ V)
    (hw : ∀ x ∈ V, ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) w x) :
    ∃ u : SmoothCFunctions X, ⇑u =ᶠ[𝓝 a] w

logDbarFiber

The logarithmic ∂̄-fiber of a weak solution at x: (ψ_x x)⁻¹ • ∂̄ψ_x|_x with ψ_x = F.unit x the centred local unit (Forster 20.2: d″f/f = d″ψ/ψ).

def logDbarFiber {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] {D : Divisor X}
    (F : WeakSolution D) (x : X) : ℂ →L[ℝ] ℂ

logDbarFiber_eventuallyEq

Locality of the logarithmic fiber (the Forster 20.2 mechanism): on nbhd a the fiber is computed from the single unit ψ_a — the holomorphic normal-form factor z_a^k is killed by ∂̄.

theorem logDbarFiber_eventuallyEq {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    (a : X) :
    ∀ x ∈ F.nbhd a, F.logDbarFiber x
      = (F.unit a x)⁻¹ • proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (F.unit a) x)

proj01_logDbarFiber

The logarithmic fiber is (0,1) (fixed by proj01).

theorem proj01_logDbarFiber {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {D : Divisor X} (F : WeakSolution D) (x : X) :
    proj01 (F.logDbarFiber x) = F.logDbarFiber x

contMDiff_logDbarFiber

Smoothness of the logarithmic fiber section: near each a, replace ψ_a by a bump-glued global smooth function and use the smoothness of (u⁻¹) • ∂̄u.

theorem contMDiff_logDbarFiber {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    :
    ContMDiff (𝓘(ℝ, ℂ)) (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ →L[ℝ] ℂ)) (⊤ : ℕ∞)
      (fun x => (⟨x, F.logDbarFiber x⟩ : Bundle.TotalSpace (ℂ →L[ℝ] ℂ)
        (fun x : X => TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x)))

logDbar

The global (0,1)-datum σ_f = d″f/f of a weak solution (Forster 20.2), as a smooth ℂ-valued 1-form.

def logDbar {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D) :
    SmoothCOneForms X where

logDbar_apply

@[simp] theorem logDbar_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    (x : X) :
    F.logDbar x = F.logDbarFiber x

logDbar_mem_zeroOne

σ_f is a (0,1)-form.

theorem logDbar_mem_zeroOne {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    : F.logDbar ∈ OneFormsZeroOne X

logDbarFiber_mul

σ_{f₁f₂} = σ_{f₁} + σ_{f₂} (pointwise).

theorem logDbarFiber_mul {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D₁ D₂ : Divisor X}
    (F₁ : WeakSolution D₁) (F₂ : WeakSolution D₂) (x : X) :
    (F₁.mul F₂).logDbarFiber x = F₁.logDbarFiber x + F₂.logDbarFiber x

logDbarFiber_one

σ_1 = 0.

theorem logDbarFiber_one {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (x : X) :
    (one X).logDbarFiber x = 0

logDbarFiber_inv

σ_{1/f} = −σ_f (pointwise) — via the product rule on the germ ψ·ψ⁻¹ = 1.

theorem logDbarFiber_inv {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    (x : X) :
    F.inv.logDbarFiber x = -F.logDbarFiber x

logDbarFiber_recast

Recasting along a divisor equality does not change the fiber.

theorem logDbarFiber_recast {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {D₁ D₂ : Divisor X} (h : D₁ = D₂) (F : WeakSolution D₁) (x : X) :
    (F.recast h).logDbarFiber x = F.logDbarFiber x

logDbarFiber_pow

σ_{f^n} = n·σ_f for natural powers (pointwise).

theorem logDbarFiber_pow {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    (n : ℕ) (x : X) :
    (F.pow n).logDbarFiber x = (n : ℤ) • F.logDbarFiber x

logDbarFiber_zpow

σ_{f^n} = n·σ_f for integer powers (pointwise).

theorem logDbarFiber_zpow {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    (n : ℤ) (x : X) :
    (F.zpow n).logDbarFiber x = n • F.logDbarFiber x

logDbarFiber_eq_zero_of_eventually_one

Where f ≡ 1 locally, the logarithmic fiber vanishes.

theorem logDbarFiber_eq_zero_of_eventually_one {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X}
    (F : WeakSolution D) {x : X}
    (h : ∀ᶠ y in 𝓝 x, F.toFun y = 1) : F.logDbarFiber x = 0

read01_logDbar_of_coeff_zero

The chart read of σ_f off the divisor: read01 σ_f y x = ∂̄(f∘chart_y⁻¹)/f at points x ∈ source_y with D x = 0.

theorem read01_logDbar_of_coeff_zero {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    {y x : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source) (hD : D x = 0) :
    Dolbeault.AbelPairing.read01 F.logDbar y x
      = (F.toFun x)⁻¹
        * DbarDisk.dbar (F.toFun ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) x)