17.5. DolbeaultComparison.DolbeaultComparisonEquiv🔗

Jacobians.DolbeaultComparison.DolbeaultComparisonEquiv — source

diskVal

The disk-primitive value function wₖ = planarPrimitive k g ∘ e_k : X → ℂ (smooth on U_k; = diskSection k g there). The global stand-in for the local section diskSection k g.

noncomputable def diskVal (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) (g : SmoothCOneForms X) :
    X → ℂ

contMDiffAt_diskVal

theorem contMDiffAt_diskVal (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) (g : SmoothCOneForms X)
    {y : X} (hy : y ∈ (𝔇.U k : Set X)) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (diskVal 𝔇 k g) y

dbar_eq_of_apply_one

A value-at-1 equation upgrades to the full (0,1)-CLM equation, for a *bare* function w (MDifferentiableAt version of dbar_eq_of_apply_one: both sides are (0,1), determined by their value at 1).

theorem dbar_eq_of_apply_one' {g : SmoothCOneForms X} (hg : g ∈ OneFormsZeroOne X) {w : X → ℂ}
    {x : X} (h1 : proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) (1 : ℂ) = (g x) (1 : ℂ)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) = g x

gdTerm

The k-th global primitive term ρ_k·wₖ : A⁰ (a genuine SmoothCFunctions; smooth because ρ_k is supported in U_k where wₖ is smooth — the primFn construction with diskVal in place of holoFn).

noncomputable def gdTerm (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) (g : SmoothCOneForms X) :
    SmoothCFunctions X

gdTerm_apply

@[simp] theorem gdTerm_apply (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) (g : SmoothCOneForms X)
    (x : X) : gdTerm 𝔇 k g x = rhoC 𝔇 k x * diskVal 𝔇 k g x

dbarL_gdTerm_apply

∂̄(ρ_k·wₖ) = wₖ·∂̄ρ_k + ρ_k·g (the Leibniz identity; unlike dbarL_primFn_apply the ρ_k·∂̄wₖ term does not vanish — ∂̄wₖ = g on U_k by dbar_diskValue_eq_g). Pointwise, 2-case (on tsupport ρ_k ⊆ U_k the product rule; off it ρ_k = ∂̄ρ_k = 0).

theorem dbarL_gdTerm_apply (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (k : 𝔇.toFiniteCover.ι) (x : X) :
    (dbarL (gdTerm 𝔇 k g)) x = diskVal 𝔇 k g x • (dbarRho 𝔇 k x) + rhoC 𝔇 k x • (g x)

holoFn_cocycle_eq_diskValDiff

The holomorphic representative of the forward cocycle is the disk-primitive difference. For y ∈ U_j ⊓ U_k, the holoFn of the (j,k) component of the Dolbeault → Čech cocycle of g equals wₖ y − wⱼ y (the cocycle component is the germ of diskSection k g − diskSection j g, whose continuous representative holoFn reads off via holoFn_eq_of_tendsto).

theorem holoFn_cocycle_eq_diskValDiff (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (j k : 𝔇.toFiniteCover.ι) {y : X}
    (hy : y ∈ (𝔇.U j ⊓ 𝔇.U k : Opens X)) :
    holoFn (cocycle_mem 𝔇 (dolbeaultToCechCocycle 𝔇 ⟨g, hg⟩) j k) y
      = diskVal 𝔇 k g y - diskVal 𝔇 j g y

etaTermFn

The k-th local-primitive term ρ_k·holoFn(f_ik) : X → ℂ, smooth on U_i.

noncomputable def etaTermFn (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i k : 𝔇.toFiniteCover.ι) : X → ℂ

contMDiffAt_etaTermFn

Each term is ContMDiffAt at points of U_i: on tsupport ρ_k (⊆ U_k, and x ∈ U_i) it is a product of smooth functions on U_i ⊓ U_k; off tsupport ρ_k it vanishes (ρ_k = 0).

theorem contMDiffAt_etaTermFn (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i k : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (etaTermFn 𝔇 f i k) x

etaFn

The local primitive η_i := ∑_k ρ_k·holoFn(f_ik) : X → ℂ, smooth on U_i.

noncomputable def etaFn (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) : X → ℂ

contMDiffAt_etaFn

theorem contMDiffAt_etaFn (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (etaFn 𝔇 f i) x

dbarL_globalPrim_eq

The global primitive's ∂̄ equals ω + g. With h = ∑_k ρ_k·wₖ, the partition-of-unity telescoping (∑ρ = 1, ∑∂̄ρ = 0) gives ∂̄h = ω + g, where ω = cechToDolbeaultForm of the forward cocycle of g. This is the heart of the round-trip: it exhibits ω + g as a ∂̄-image, so [ω] = −[g] in H^{0,1}.

theorem dbarL_globalPrim_eq (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) :
    dbarL (∑ k, gdTerm 𝔇 k g)
      = ((cechToDolbeaultForm 𝔇 (dolbeaultToCechCocycle 𝔇 ⟨g, hg⟩) : ↥(OneFormsZeroOne X)) :
          SmoothCOneForms X) + g

dbar_etaTermFn_apply

∂̄(ρ_k·holoFn(f_ik)) = holoFn(f_ik)·∂̄ρ_k on U_i (the Leibniz identity, with the holomorphic factor holoFn(f_ik) killed by holoFn_dbar_eq_zero). Pointwise at x ∈ U_i; the proof is the dbarL_primFn_apply pattern but with holoFn on the overlap U_i ⊓ U_k. Two-case: on tsupport ρ_k the product rule; off it ρ_k = ∂̄ρ_k = 0.

theorem dbar_etaTermFn_apply (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i k : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (etaTermFn 𝔇 f i k) x)
      = holoFn (cocycle_mem 𝔇 f i k) x • (dbarRho 𝔇 k x)

dbar_etaFn_apply

∂̄η_i = ∑_k holoFn(f_ik)·∂̄ρ_k on U_i (sum the per-term Leibniz).

theorem dbar_etaFn_apply (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (etaFn 𝔇 f i) x)
      = ∑ k, holoFn (cocycle_mem 𝔇 f i k) x • (dbarRho 𝔇 k x)

cechToDolbeaultForm_eq_on_Ui

ω = ∑_k holoFn(f_ik)·∂̄ρ_k on U_i (= ∂̄η_i). The double-sum ω = ∑_{j,k} (ρ_j·holoFn(f_jk))·∂̄ρ_k telescopes once the cocycle relation holoFn(f_jk) = holoFn(f_ik) − holoFn(f_ij) (holoFn_cocycle_add, valid on the triple overlap, the only place both ρ_j and ∂̄ρ_k survive) replaces holoFn(f_jk) by holoFn(f_ik) − holoFn(f_ij); then telescope_sum (∑ρ=1, ∑∂̄ρ=0) collapses to ∑_k holoFn(f_ik)·∂̄ρ_k.

theorem cechToDolbeaultForm_eq_on_Ui (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    ((cechToDolbeaultForm 𝔇 f : ↥(OneFormsZeroOne X)) : SmoothCOneForms X) x
      = ∑ k, holoFn (cocycle_mem 𝔇 f i k) x • (dbarRho 𝔇 k x)

dbar_holDiff_eq_zero

The local primitive diskVal_i ω − η_i has vanishing intrinsic ∂̄ on U_i. Both have ∂̄ = ω there: diskVal_i ω via dbar_diskValue_eq_g (upgraded to the full CLM by dbar_eq_of_apply_one'), η_i via dbar_etaFn_apply = cechToDolbeaultForm_eq_on_Ui = ω.

theorem dbar_holDiff_eq_zero (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)
      (fun y => diskVal 𝔇 i ((cechToDolbeaultForm 𝔇 f : ↥(OneFormsZeroOne X)) :
          SmoothCOneForms X) y - etaFn 𝔇 f i y) x) = 0

holDiffFn

The local primitive difference diskVal_i ω − η_i, as a function X → ℂ. Smooth and holomorphic on U_i (∂̄ = 0 there, dbar_holDiff_eq_zero).

noncomputable def holDiffFn (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) : X → ℂ

contMDiffAt_holDiffFn

theorem contMDiffAt_holDiffFn (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (holDiffFn 𝔇 f i) x

differentiableAt_holDiffFn_ownChart

holDiffFn is holomorphic (ℂ-differentiable) in each point's own chart on U_i. From the intrinsic ∂̄ = 0 (dbar_holDiff_eq_zero): the own-chart bridge dbar_apply_one_eq_dbarDisk' turns proj01 (mfderiv …) 1 = 0 into a planar DbarDisk.dbar = 0, and local Cauchy–Riemann (differentiableAt_cplx_of_dbarDisk_eq_zero) upgrades the (real) chart-smoothness to ℂ-differentiability.

theorem differentiableAt_holDiffFn_ownChart (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    DifferentiableAt ℂ (fun z => holDiffFn 𝔇 f i ((extChartAt 𝓘(ℝ, ℂ) x).symm z))
      ((extChartAt 𝓘(ℝ, ℂ) x) x)

holDiffFn_chart_analyticAt

holDiffFn read in each point's own chart is analytic (the OmegaD-membership input). For v ∈ U_i, the analytic representative of the germ [holDiffFn] on ↥U_i is analytic at (chartAt v) v. Proof: holDiffFn ∘ (chartAt v).symm is ℂ-differentiable on the open W = chartAt v.target ∩ preimage U_i — at each z ∈ W with p = chartAt v.symm z ∈ U_i, write it as (holDiffFn ∘ chartAt p.symm) ∘ (chartAt p ∘ chartAt v.symm), the own-chart holomorphy (differentiableAt_holDiffFn_ownChart) composed with the analytic transition — so DifferentiableOn.analyticAt.

theorem holDiffFn_chart_analyticAt (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i : 𝔇.toFiniteCover.ι)
    (F : ↥(𝔇.U i) → ℂ) (hFeq : ∀ v : ↥(𝔇.U i), F v = holDiffFn 𝔇 f i v.1) (v : ↥(𝔇.U i)) :
    AnalyticAt ℂ (Gext F ∘ (chartAt (H := ℂ) (v : X)).symm)
      ((chartAt (H := ℂ) (v : X)) (v : X))

cech_to_dolbeault_comp_dolbeault_to_cech

comparison_bijective, part 1: Dolbeault → Čech → Dolbeault is the identity. Globalizing the forward cocycle of g via the partition of unity returns [g] (the global primitive h = ∑ρ_k·wₖ has ∂̄h = ω + g, so cech_to_dolbeault — carrying the boundary sign — sends [ω] to [g]).

theorem cech_to_dolbeault_comp_dolbeault_to_cech (𝔇 : ChartDiskCover X)
    (_hL : 𝔇.toFiniteCover.IsLeray) :
    (cech_to_dolbeault 𝔇) ∘ₗ (dolbeault_to_cech 𝔇) = LinearMap.id

etaFn_germ_diff_eq

The eta-difference germ identity (η_i − η_l = f_il on the overlap). As MGerm (U_i ⊓ U_l): the germ of (holoFn ∘ η_i) − (holoFn ∘ η_l) restricted to the overlap equals f_il. On the overlap, η_i − η_l = ∑_k ρ_k·(holoFn(f_ik) − holoFn(f_lk)) = ∑_k ρ_k·holoFn(f_il) = holoFn(f_il) (cocycle relation holoFn_cocycle_add + ∑ρ = 1); then toGerm(holoFn(f_il)) = f_il (toGerm_holoFn).

theorem etaFn_germ_diff_eq (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i l : 𝔇.toFiniteCover.ι) :
    toGerm (𝔇.U i ⊓ 𝔇.U l)
        (fun v : ↥(𝔇.U i ⊓ 𝔇.U l) => etaFn 𝔇 f i v.1 - etaFn 𝔇 f l v.1)
      = (f : 𝔇.toFiniteCover.Cochain1) (i, l)

holCochain

The holomorphic 0-cochain {hol_i} of round-trip 2: hol_i = diskVal_i ω − η_i (germ on ↥U_i), holomorphic by holDiffFn_chart_analyticAt. Lives in sections0 0.

noncomputable def holCochain (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) : 𝔇.toFiniteCover.Cochain0

holCochain_mem_sections0

theorem holCochain_mem_sections0 (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    holCochain 𝔇 f ∈ 𝔇.toFiniteCover.sections0 (0 : Divisor X)

cechDelta0_holCochain_eq

The Čech identity cechDelta0 {hol_i} = cechDelta0 (rawCochain ω) + f. Componentwise on U_i ⊓ U_l: hol_l − hol_i = (diskVal_l ω − diskVal_i ω) − (η_l − η_i); the first bracket is cechDelta0 (rawCochain ω)(i,l) (the disk-primitive difference germ), the second is −f_il (etaFn_germ_diff_eq). So the coboundary of the holomorphic {hol_i} is cechDelta0(rawCochain ω) + f.

theorem cechDelta0_holCochain_eq (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    𝔇.toFiniteCover.cechDelta0 (holCochain 𝔇 f)
      = 𝔇.toFiniteCover.cechDelta0 (𝔇.rawCochain
          ((cechToDolbeaultForm 𝔇 f : ↥(OneFormsZeroOne X)) : SmoothCOneForms X))
        + (f : 𝔇.toFiniteCover.Cochain1)

dolbeault_to_cech_comp_cech_to_dolbeault

theorem dolbeault_to_cech_comp_cech_to_dolbeault (𝔇 : ChartDiskCover X)
    (_hL : 𝔇.toFiniteCover.IsLeray) :
    (dolbeault_to_cech 𝔇) ∘ₗ (cech_to_dolbeault 𝔇) = LinearMap.id

comparison_linearEquiv

The Dolbeault isomorphism H^{0,1}(X) ≃ₗ[ℝ] H¹(X, 𝒪) — assembled *completely* from the two maps and the two round-trip identities above (LinearEquiv.ofLinear). All remaining content is in the four named sub-kernels.

noncomputable def comparison_linearEquiv (𝔇 : ChartDiskCover X) (hL : 𝔇.toFiniteCover.IsLeray) :
    DolbeaultH01 X ≃ₗ[ℝ] 𝔇.toFiniteCover.cechH1 0

cechH1_dolbeault_comparison_proof

The L3 kernel: Čech ↔ Dolbeault comparison — the standalone proof of the comparison statement (DolbeaultComparison.lean's deliverable 5; IsLeray-free form in GoodCover.lean). Proven completely from comparison_linearEquiv: the ℝ-linear iso transports finrank ℝ, and the ℝ-vs-ℂ factor on the ℂ-module cechH1 is finrank_real_of_complex. The entire remaining content sits in the four named sub-kernels (dolbeault_to_cech, cech_to_dolbeault, and the two round-trip identities).

theorem cechH1_dolbeault_comparison_proof (𝔇 : ChartDiskCover X) (hL : 𝔇.toFiniteCover.IsLeray) :
    Module.finrank ℝ (DolbeaultH01 X) = 2 * Module.finrank ℂ (𝔇.toFiniteCover.cechH1 0)