30.6. Abel.AbelEngineSigma🔗

Jacobians.Abel.AbelEngineSigma — source

proj01_logDeriv_mul

The two-factor logarithmic-∂̄ product rule (function form of logDbarFiber_mul).

theorem proj01_logDeriv_mul {f g : X → ℂ} {x : X}
    (hf : ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) f x)
    (hg : ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) g x)
    (hf0 : f x ≠ 0) (hg0 : g x ≠ 0) :
    ((f x * g x)⁻¹ : ℂ) • Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (fun y => f y * g y) x)
      = (f x)⁻¹ • Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) f x)
        + (g x)⁻¹ • Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) g x)

proj01_logDeriv_prod

The finite logarithmic-∂̄ product rule.

theorem proj01_logDeriv_prod {x : X} (n : ℕ) (f : ℕ → X → ℂ)
    (hf : ∀ k < n, ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (f k) x)
    (hf0 : ∀ k < n, f k x ≠ 0) :
    ((∏ k ∈ Finset.range n, f k x)⁻¹ : ℂ) •
        Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)
          (fun y => ∏ k ∈ Finset.range n, f k y) x)
      = ∑ k ∈ Finset.range n,
          (f k x)⁻¹ • Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (f k) x)

AbelPlanar.PlanarPieceSolution.inv_mul_dbar_F

Away from the two endpoints, the planar ∂̄-datum is the logarithmic ∂̄ of the piece solution: U = F⁻¹·∂̄F.

theorem AbelPlanar.PlanarPieceSolution.inv_mul_dbar_F {c₀ α β : ℂ} {ρ : ℝ}
    (S : PlanarPieceSolution c₀ ρ α β) {z : ℂ} (hzα : z ≠ α) (hzβ : z ≠ β) :
    (S.F z)⁻¹ * DbarDisk.dbar S.F z = S.U z

WeakSolution.logDbarFiber_eq_of_coeff_zero

Off the divisor the logarithmic fiber is f⁻¹·∂̄f directly.

theorem WeakSolution.logDbarFiber_eq_of_coeff_zero [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {D : Divisor X} (F : WeakSolution D)
    {x : X} (hD : D x = 0) :
    F.logDbarFiber x
      = (F.toFun x)⁻¹ • Dolbeault.proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) F.toFun x)

Dolbeault.AbelPairing.read01_congr_of_apply_eq

theorem Dolbeault.AbelPairing.read01_congr_of_apply_eq [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] {g₁ g₂ : SmoothCOneForms X} {x : X}
    (h : (g₁ x) = (g₂ x)) (y : X) : read01 g₁ y x = read01 g₂ y x

Dolbeault.AbelPairing.pairForm_congr_off_finite

The pairing ignores finitely many fiber values (a finite set of chart points is volume-null).

theorem Dolbeault.AbelPairing.pairForm_congr_off_finite [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (η : HolomorphicOneForms X)
    {g₁ g₂ : SmoothCOneForms X} {E : Set X} (hE : E.Finite)
    (h : ∀ x ∉ E, (g₁ x) = (g₂ x)) :
    pairForm η g₁ = pairForm η g₂

pairForm_logDbar_piece

The per-piece pairing value: the pairing of η against the piece ∂̄-datum is the planar integral ∫ Uₖ·η̂ₖ of Forster 20.5.

theorem pairForm_logDbar_piece [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) {γ : ℝ → X}
    {hγ : ContinuousOn γ (Icc 0 1)} (S : CurveWeakSolution γ hγ) (k : ℕ) :
    pairForm η (S.pieceSol k).logDbar
      = ∫ z, (S.planar k).U z
          * Jacobians.Montel.localRep η (S.center k)
            ((chartAt (H := ℂ) (S.center k)).symm z)

pairForm_logDbar_curve

The per-curve pairing value (Forster 20.5): ⟨η, σ_{f_γ}⟩ = π·∫_γ η.

theorem pairForm_logDbar_curve [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) {γ : ℝ → X}
    {hγ : ContinuousOn γ (Icc 0 1)} (S : CurveWeakSolution γ hγ) :
    pairForm η S.sol.logDbar = (π : ℂ) * pathPrimValue η γ hγ

exists_weakSolution_finsum

The zpow-fold of a finite family of weak solutions, with the logDbar sum rule.

theorem exists_weakSolution_finsum [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {n : ℕ} (D : Fin n → Divisor X)
    (F : (m : Fin n) → WeakSolution (D m)) :
    ∃ G : WeakSolution (∑ m, D m),
      ∀ x, G.logDbarFiber x = ∑ m, (F m).logDbarFiber x

exists_dbar_potential_of_oneChain

The chain ∂̄-potential (Forster 20.7 (a), the analytic heart): a 1-chain with all basis periods zero has a weak solution G of its boundary whose ∂̄-datum is exact: σ_G = ∂̄u.

theorem exists_dbar_potential_of_oneChain [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (c : OneChain X)
    (hper : ∀ i : Fin (genus X), c.period (periodBasisForm X i) = 0) :
    ∃ (G : WeakSolution c.boundary) (u : SmoothCFunctions X), dbarL u = G.logDbar