30.4. Abel.AbelDbarKill🔗

Jacobians.Abel.AbelDbarKill — source

pairForm_smul

theorem pairForm_smul (η : HolomorphicOneForms X) (r : ℝ) (g : SmoothCOneForms X) :
    pairForm η (r • g) = r • pairForm η g

pairMatrix

The period Gram matrix Nᵢⱼ = ⟨ωᵢ, ω̄ⱼ⟩ of the basis forms against their conjugates.

def pairMatrix (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    Matrix (Fin (genus X)) (Fin (genus X)) ℂ

ambientIso_eq_sum

The expansion of ambientIso over the period basis (cf. PeriodLatticeNondegenerate).

theorem ambientIso_eq_sum (d : Fin (genus X) → ℂ) :
    ambientIso X d = ∑ j, d j • periodBasisForm X j

pairMatrix_det_ne_zero

The period Gram matrix is nonsingular (the 19.9 positivity argument): a kernel vector v would make g = ∑ v̄ⱼ·ωⱼ ≠ 0 pair to zero against its own conjugate.

theorem pairMatrix_det_ne_zero : (pairMatrix X).det ≠ 0

pairFormL

pairForm η as an ℝ-linear functional on A¹, bundling its ℝ-linearity in the form argument (pairForm_add / pairForm_smul).

def pairFormL (η : HolomorphicOneForms X) : SmoothCOneForms X →ₗ[ℝ] ℂ where

pairFunctional

The pairing functional Λ : A^{0,1} →ₗ[ℝ] ℂ^g, Λ(σ)ᵢ = ⟨ωᵢ, σ⟩. Assembled from combinators (LinearMap.pi of pairFormL ∘ subtype) so additivity and homogeneity are inherited, rather than re-proved by hand against the Fin g → ℂ real-module diamond.

def pairFunctional (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    ↥(OneFormsZeroOne X) →ₗ[ℝ] (Fin (genus X) → ℂ)

pairFunctional_apply

theorem pairFunctional_apply (s : ↥(OneFormsZeroOne X)) (i : Fin (genus X)) :
    pairFunctional X s i = pairForm (periodBasisForm X i) (s : SmoothCOneForms X)

dbarImage_le_ker_pairFunctional

The functional kills im ∂̄ (Stokes vanishing).

theorem dbarImage_le_ker_pairFunctional :
    dbarImageInZeroOne X ≤ LinearMap.ker (pairFunctional X)

pairFunctionalH01

The descended functional Λ̄ : H^{0,1} →ₗ[ℝ] ℂ^g.

def pairFunctionalH01 (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    DolbeaultH01 X →ₗ[ℝ] (Fin (genus X) → ℂ)

pairFunctionalH01_mk

theorem pairFunctionalH01_mk (s : ↥(OneFormsZeroOne X)) :
    pairFunctionalH01 X (Submodule.Quotient.mk s) = pairFunctional X s

pairFunctionalH01_surjective

Surjectivity of the descended functional: the range contains every c·colⱼ of the nonsingular Gram matrix, hence all of ℂ^g.

theorem pairFunctionalH01_surjective : Function.Surjective (pairFunctionalH01 X)

chartDiskCover_isLeray

The canonical chart-disk cover is Leray.

theorem chartDiskCover_isLeray : (chartDiskCover (X := X)).toFiniteCover.IsLeray

finrank_dolbeaultH01

dim_ℝ H^{0,1}(X) = 2g (Dolbeault comparison + the h¹ = g dimension count).

theorem finrank_dolbeaultH01 : finrank ℝ (DolbeaultH01 X) = 2 * genus X

exists_dbarL_eq_of_pairForm_eq_zero

Forster 19.10 (the ∂̄-solvability criterion): a smooth (0,1)-form pairing to zero against every basis holomorphic form is a ∂̄-coboundary.

theorem exists_dbarL_eq_of_pairForm_eq_zero {s : SmoothCOneForms X}
    (hs : s ∈ OneFormsZeroOne X)
    (h0 : ∀ i : Fin (genus X), pairForm (periodBasisForm X i) s = 0) :
    ∃ u : SmoothCFunctions X, dbarL u = s