17.7. DolbeaultComparison.DolbeaultComparisonProof🔗

Jacobians.DolbeaultComparison.DolbeaultComparisonProof — source

cechDelta0_mem_ker_cechDelta1

(Algebraic backbone, complete.) cechDelta0 of any germ-class 0-cochain is a Čech 1-cocycle. This is the abstract reason {[u_i] − [u_j]} (the Dolbeault → Čech cochain) lies in ker cechDelta1; it holds for the smooth-not-holomorphic primitives u_i because germ-class cochains carry no holomorphy constraint. Immediate from δ¹ ∘ δ⁰ = 0.

theorem cechDelta0_mem_ker_cechDelta1 {X : Type*} [TopologicalSpace X] (𝔘 : FiniteCover X)
    (c : 𝔘.Cochain0) :
    𝔘.cechDelta0 c ∈ LinearMap.ker 𝔘.cechDelta1

proj01_apply_one

proj01 α 1 = ½(α 1 + i·α i) — the value of the (0,1)-projection at the tangent vector 1 is the Wirtinger combination (the same ½(· + i·(i·)) that defines DbarDisk.dbar).

theorem proj01_apply_one (α : ℂ →L[ℝ] ℂ) :
    proj01 α 1 = (2 : ℂ)⁻¹ * (α 1 + Complex.I * α Complex.I)

proj01_conjLinear

proj01 α is conjugate-ℂ-linear: (proj01 α)(i·v) = −i·(proj01 α) v. (It is the (0,1) = anti-holomorphic part, by construction.)

theorem proj01_conjLinear (α : ℂ →L[ℝ] ℂ) (v : ℂ) :
    proj01 α (Complex.I * v) = -(Complex.I * proj01 α v)

proj01_eq_conj_smul

A (0,1)-form's value is conj-homogeneous: proj01 α v = conj v · (proj01 α 1).

theorem proj01_eq_conj_smul (α : ℂ →L[ℝ] ℂ) (v : ℂ) :
    proj01 α v = (starRingEnd ℂ) v * proj01 α 1

proj01_ext_of_apply_one

A (0,1)-form is determined by its value at the tangent vector 1. Anything in the range of proj01 (fixed by it) that agrees at 1 agrees everywhere — this is what lets the single scalar equation DbarDisk.dbar … = g … recover the full CLM equation dbar u x = g x.

theorem proj01_ext_of_apply_one {α β : ℂ →L[ℝ] ℂ} (hαβ : proj01 α 1 = proj01 β 1) :
    proj01 α = proj01 β

mfderiv_apply_eq_fderiv_pullback

mfderiv of u at x, applied to a tangent vector v, is the plain fderiv of the chart-pullback u ∘ (extChartAt _ x).symm at the chart coordinate extChartAt _ x x, applied to v. (The boundaryless model has range = univ, so fderivWithin = fderiv; the codomain chart on ℂ is the identity, so writtenInExtChartAt is the bare pullback.)

theorem mfderiv_apply_eq_fderiv_pullback (u : SmoothCFunctions X) (x : X) (v : ℂ) :
    (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⇑u) x) v =
      fderiv ℝ (fun z => u ((extChartAt 𝓘(ℝ, ℂ) x).symm z)) (extChartAt 𝓘(ℝ, ℂ) x x) v

dbar_apply_one_eq_dbarDisk

The chart bridge. The intrinsic dbar u at x (i.e. proj01 (mfderiv … u x)), evaluated at the tangent vector 1, equals the planar Wirtinger DbarDisk.dbar of the chart-pullback of u, read at the chart coordinate of x. This is the dbar(intrinsic)= DbarDisk.dbar(chart) identity that transports the planar solvability to the manifold.

theorem dbar_apply_one_eq_dbarDisk (u : SmoothCFunctions X) (x : X) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⇑u) x) (1 : ℂ) =
      DbarDisk.dbar (fun z => u ((extChartAt 𝓘(ℝ, ℂ) x).symm z)) (extChartAt 𝓘(ℝ, ℂ) x x)

mfderiv_apply_eq_fderiv_pullback

Generalized chart bridge for a *bare* MDifferentiableAt function w : X → ℂ (not just a SmoothCFunctions): mfderiv w x v is the plain fderiv of the chart-pullback. Same proof as mfderiv_apply_eq_fderiv_pullback but with the smoothness replaced by the weaker MDifferentiableAt hypothesis — used to read the intrinsic ∂̄ of a *locally*-smooth value function like planarPrimitive ∘ extChartAt.

theorem mfderiv_apply_eq_fderiv_pullback' {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {w : X → ℂ} {x : X}
    (hw : MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) (v : ℂ) :
    (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) v =
      fderiv ℝ (fun z => w ((extChartAt 𝓘(ℝ, ℂ) x).symm z)) (extChartAt 𝓘(ℝ, ℂ) x x) v

dbar_apply_one_eq_dbarDisk

Generalized chart bridge at 1 for a bare MDifferentiableAt function: the intrinsic Wirtinger scalar proj01 (mfderiv w x) 1 equals the planar DbarDisk.dbar of the chart-pullback. The MDifferentiableAt form of dbar_apply_one_eq_dbarDisk.

theorem dbar_apply_one_eq_dbarDisk' {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    {w : X → ℂ} {x : X}
    (hw : MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) (1 : ℂ) =
      DbarDisk.dbar (fun z => w ((extChartAt 𝓘(ℝ, ℂ) x).symm z)) (extChartAt 𝓘(ℝ, ℂ) x x)

dbar_eq_of_apply_one

A value-at-1 equation upgrades to the full CLM equation dbar u x = g x (complete). Both dbar u x = proj01 (mfderiv … u x) and (since g ∈ OneFormsZeroOne X) g x = proj01 (β x) are (0,1)-forms, hence determined by their value at the tangent vector 1 (proj01_ext_of_apply_one). So matching the single Wirtinger scalar suffices. This is the mechanism by which the planar (scalar) ∂̄-solvability recovers the intrinsic CLM-valued equation.

theorem dbar_eq_of_apply_one {g : SmoothCOneForms X} (hg : g ∈ OneFormsZeroOne X)
    (u : SmoothCFunctions X) (x : X)
    (h1 : proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⇑u) x) (1 : ℂ) = (g x) (1 : ℂ)) :
    (dbar u) x = g x

exists_smoothLift_of_chartFun

The smooth lift of a chart-local planar function to a global manifold function (complete). Given a smooth f : ℂ → ℂ and a base point x₀, the cutoff product χ • (f ∘ extChartAt x₀) — with χ a SmoothBumpFunction at x₀ (= 1 near x₀, supported in the chart) — is a *global* SmoothCFunctions X (via SmoothBumpFunction.contMDiff_smul) that equals f ∘ extChartAt x₀ on the open neighborhood where χ = 1. This is the "extend a chart-local smooth function to the whole manifold" half of the smooth-section ↔ chart-function dictionary; it is exactly how the planar local primitive ũ becomes a global u.

theorem exists_smoothLift_of_chartFun (f : ℂ → ℂ) (hf : ContDiff ℝ (⊤ : ℕ∞) f) (x₀ : X) :
    ∃ (V : Set X) (u : SmoothCFunctions X), IsOpen V ∧ x₀ ∈ V ∧
      ∀ x ∈ V, (u x : ℂ) = f (extChartAt 𝓘(ℝ, ℂ) x₀ x)

dbarDisk_comp_holo

Wirtinger chain rule for a holomorphic inner map. For f real-differentiable and τ holomorphic at ζ, the planar ∂̄ of the composite transforms by the conjugate of the complex derivative of τ: DbarDisk.dbar (f ∘ τ) ζ = conj(τ′(ζ)) · DbarDisk.dbar f (τ ζ). (The anti-holomorphic Wirtinger derivative is conjugate-linear in the holomorphic frame change — the defining feature of a (0,1)-quantity.)

theorem dbarDisk_comp_holo (f : ℂ → ℂ) (τ : ℂ → ℂ) (ζ : ℂ)
    (hf : DifferentiableAt ℝ f (τ ζ)) (hτ : DifferentiableAt ℂ τ ζ) :
    DbarDisk.dbar (f ∘ τ) ζ = (starRingEnd ℂ) (deriv τ ζ) * DbarDisk.dbar f (τ ζ)

dbarDisk_congr

DbarDisk.dbar depends only on the germ of its argument: it agrees on functions equal in a neighborhood of the base point (it is a fixed combination of fderiv ℝ, which respects Filter.EventuallyEq).

theorem dbarDisk_congr {f₁ f₂ : ℂ → ℂ} {z : ℂ} (h : f₁ =ᶠ[nhds z] f₂) :
    DbarDisk.dbar f₁ z = DbarDisk.dbar f₂ z

differentiableAt_chartTransition

The chart-transition e₀ ∘ eₓ.symm is holomorphic (ℂ-differentiable). On the analytic (ω) manifold X, chart transition maps are holomorphic; here at the chart coordinate eₓ x of any point x in the x₀-chart's source. (ContMDiffAt of the two charts composed, transferred to ContDiffAt ℂ ω and hence DifferentiableAt ℂ; chartAt ℂ = extChartAt 𝓘(ℝ,ℂ) for the identity model.)

theorem differentiableAt_chartTransition {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x : X)
    (hxsrc : x ∈ (extChartAt 𝓘(ℝ, ℂ) x₀).source) :
    DifferentiableAt ℂ ((extChartAt 𝓘(ℝ, ℂ) x₀) ∘ (extChartAt 𝓘(ℝ, ℂ) x).symm)
      ((extChartAt 𝓘(ℝ, ℂ) x) x)

differentiableAt_chartTransition_symm

The inverse chart-transition eₓ ∘ e₀.symm is holomorphic at e₀ x. Companion to differentiableAt_chartTransition with the two charts swapped and read at the point e₀ x = τ_x(eₓ x) (rather than eₓ x); the local inverse of the transition e₀ ∘ eₓ.symm. Same mechanism: the two charts of the analytic (ω) manifold composed, transferred to DifferentiableAt ℂ.

theorem differentiableAt_chartTransition_symm {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x : X)
    (hxsrc : x ∈ (extChartAt 𝓘(ℝ, ℂ) x₀).source) :
    DifferentiableAt ℂ ((extChartAt 𝓘(ℝ, ℂ) x) ∘ (extChartAt 𝓘(ℝ, ℂ) x₀).symm)
      ((extChartAt 𝓘(ℝ, ℂ) x₀) x)

deriv_chartTransition_ne_zero

Nonvanishing of the holomorphic transition derivative. On the analytic (ω) manifold, for x in the x₀-chart, the complex derivative of the chart transition τ_x = e₀ ∘ eₓ.symm at eₓ x is nonzero: τ_x has the holomorphic local inverse eₓ ∘ e₀.symm, so deriv τ_x · deriv (inverse) = 1 by the chain rule on (eₓ ∘ e₀.symm) ∘ τ_x = id near eₓ x, forcing the factor ≠ 0.

theorem deriv_chartTransition_ne_zero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x : X)
    (hxsrc : x ∈ (extChartAt 𝓘(ℝ, ℂ) x₀).source) :
    deriv ((extChartAt 𝓘(ℝ, ℂ) x₀) ∘ (extChartAt 𝓘(ℝ, ℂ) x).symm)
      ((extChartAt 𝓘(ℝ, ℂ) x) x) ≠ 0

differentiableAt_transition_of_mem

Transition holomorphy at a general overlap point. The chart transition e_a ∘ e_b.symm is ℂ-differentiable at any w in e_b's target whose e_b-preimage lies in e_a's source (not only at the chart centre, as in differentiableAt_chartTransition). Same mechanism: the two analytic (ω) charts composed, ContMDiffAt → ContDiffAt ℂ → DifferentiableAt ℂ.

theorem differentiableAt_transition_of_mem {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (a b : X) {w : ℂ}
    (hwt : w ∈ (chartAt ℂ b).target) (hws : (chartAt ℂ b).symm w ∈ (chartAt ℂ a).source) :
    DifferentiableAt ℂ ((extChartAt 𝓘(ℝ, ℂ) a) ∘ (extChartAt 𝓘(ℝ, ℂ) b).symm) w

frameVector_eq_deriv_transition_symm

The frame vector as the (forward) inverse-transition derivative (direct form). For x in the x₀-chart, Sₓ 1 = symmL ℝ (trivAt x₀) x 1 equals deriv σ_x (e₀ x) with σ_x = eₓ ∘ e₀.symm the *inverse* chart transition. (Same symmL = tangentCoordChange = fderivWithin σ_x chain as frameVector_eq_inv_deriv_transition, stopping at fderiv σ_x = deriv σ_x • 1 before inverting; the reciprocal of the deriv τ_x form.) Used to read ∂̄h in another chart without the inverse.

theorem frameVector_eq_deriv_transition_symm {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x : X)
    (hxsrc : x ∈ (extChartAt 𝓘(ℝ, ℂ) x₀).source) :
    (Bundle.Trivialization.symmL ℝ (trivializationAt ℂ (TangentSpace (𝓘(ℝ, ℂ))) x₀) x) (1 : ℂ)
      = deriv ((extChartAt 𝓘(ℝ, ℂ) x) ∘ (extChartAt 𝓘(ℝ, ℂ) x₀).symm)
        ((extChartAt 𝓘(ℝ, ℂ) x₀) x)

contMDiffAt_chartRead_datum

The chart-read datum of g at the fixed x₀-trivialization is a smooth map X → ℂ at every point y of the x₀-chart source: x ↦ (g x) (Sₓ 1), with Sₓ = symmL ℝ (trivializationAt ℂ (TangentSpace 𝓘(ℝ,ℂ)) x₀) x the symmL of the fixed x₀-trivialization.

Mechanism: by contMDiffAt_hom_bundle at y (the codomain trivial ℂ-bundle has identity trivialisation), x ↦ (g x).comp (symmL(trivAt y)(x)) is smooth into ℂ →L[ℝ] ℂ. The frame at y and at x₀ differ by the bundle coordChangeL (x ↦ coordChangeL (trivAt x₀) (trivAt y) x, smooth by contMDiffAt_coordChangeL), so the value (g x)(Sₓ 1) rewrites as ((g x).comp (symmL(trivAt y)(x))) (coordChangeL (trivAt x₀) (trivAt y) x 1) near y (coordChangeL_apply + symmL_continuousLinearMapAt); both factors are smooth, so ContMDiffAt.clm_apply closes it. (No varying chart-at-x: Sₓ uses only the fixed x₀-trivialization; the y-frame is an internal device.)

theorem contMDiffAt_chartRead_datum (g : SmoothCOneForms X) (x₀ y : X)
    (hy : y ∈ (extChartAt 𝓘(ℝ, ℂ) x₀).source) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞)
      (fun x => (g x) ((Bundle.Trivialization.symmL ℝ
        (trivializationAt ℂ (TangentSpace (𝓘(ℝ, ℂ))) x₀) x) (1 : ℂ))) y

frameVector_eq_inv_deriv_transition

The frame vector is the inverse transition derivative. For x in the x₀-chart source, the constant x₀-frame tangent vector Sₓ 1 = symmL ℝ (trivAt x₀) x 1 equals (τ_x′(eₓ x))⁻¹, the reciprocal of the holomorphic chart-transition derivative τ_x = e₀ ∘ eₓ.symm. (symmL (trivAt x₀) x is the tangent coordChange (achart x₀) (achart x) x = tangentCoordChange x₀ x x = fderivWithin ℝ (eₓ ∘ e₀.symm) (range) (e₀ x); on the boundaryless model this is fderiv ℝ σ_x (e₀ x), and σ_x = eₓ ∘ e₀.symm is holomorphic so fderiv ℝ σ_x (e₀ x) = (deriv σ_x (e₀ x)) • 1; finally deriv σ_x (e₀ x) = (deriv τ_x (eₓ x))⁻¹ since σ_x is the local inverse of τ_x.)

theorem frameVector_eq_inv_deriv_transition {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] (x₀ x : X)
    (hxsrc : x ∈ (extChartAt 𝓘(ℝ, ℂ) x₀).source) :
    (Bundle.Trivialization.symmL ℝ (trivializationAt ℂ (TangentSpace (𝓘(ℝ, ℂ))) x₀) x) (1 : ℂ)
      = (deriv ((extChartAt 𝓘(ℝ, ℂ) x₀) ∘ (extChartAt 𝓘(ℝ, ℂ) x).symm)
          ((extChartAt 𝓘(ℝ, ℂ) x) x))⁻¹

oneForm_apply_conjLinear

The (0,1)-form g x is conjugate-ℂ-linear (since g ∈ OneFormsZeroOne X): (g x) v = conj v · (g x) 1. Reduces to proj01\_eq\_conj\_smul via g x = proj01 (β x) for the representative β with proj01L β = g.

theorem oneForm_apply_conjLinear {g : SmoothCOneForms X} (hg : g ∈ OneFormsZeroOne X)
    (x : X) (v : ℂ) : (g x) v = (starRingEnd ℂ) v * (g x) (1 : ℂ)

exists_chartPullback_zeroOne_datum

(Finer analytic sub-kernel — the chart-pullback (0,1)-datum.) A smooth (0,1)-form g read in the x₀-chart is a *smooth planar function* G : ℂ → ℂ (its Wirtinger / value-1 datum) that reproduces the intrinsic value g x 1 after the holomorphic frame change: on a *neighborhood* V of x₀, with τ_x = e₀ ∘ eₓ.symm the holomorphic transition, conj(τ_x′(eₓ x)) · G(e₀ x) = g x 1.

LOCALITY (why a neighborhood V, not the whole chart source): the datum G is the chart-pullback of g; on a non-compact chart-disk it is genuinely *unbounded at the chart boundary*, so the global "for all x ∈ e₀.source" form is FALSE. The honest statement gives the law only near x₀ (where the local primitive is built); this is all exists_localPrimitive_apply_one consumes.

This is the genuine smooth-section ↔ planar-form dictionary entry that Mathlib lacks: it packages (i) the smoothness of the chart-read datum G and (ii) the (0,1)-transformation law (the conj(τ′) frame factor) into the exact form consumed by exists_localPrimitive_apply_one. The conj(τ′) here is the *same* factor produced on the ∂̄u side by the Wirtinger chain rule dbarDisk_comp_holo , so the two cancel and the planar PDE DbarLocal.dbar_solvable_locally closes the local primitive. It is the standard statement that a (0,1)-form pulls back along a chart to a smooth (0,1)-form, whose anti-holomorphic component transforms by conj of the transition derivative (proj01_eq_conj_smul gives the conjugate-homogeneity fiberwise; the content is the *smoothness* of G and the chart-derivative bookkeeping mfderiv of charts ↔ planar deriv τ).

theorem exists_chartPullback_zeroOne_datum (g : SmoothCOneForms X)
    (hg : g ∈ OneFormsZeroOne X) (x₀ : X) :
    ∃ (G : ℂ → ℂ) (V : Set X), ContDiff ℝ (⊤ : ℕ∞) G ∧ IsOpen V ∧ x₀ ∈ V ∧
      ∀ x ∈ V, (starRingEnd ℂ) (deriv (extChartAt 𝓘(ℝ, ℂ) x₀ ∘ (extChartAt 𝓘(ℝ, ℂ) x).symm)
            (extChartAt 𝓘(ℝ, ℂ) x x)) * G (extChartAt 𝓘(ℝ, ℂ) x₀ x) = (g x) (1 : ℂ)

exists_localPrimitive_apply_one

theorem exists_localPrimitive_apply_one (g : SmoothCOneForms X) (hg : g ∈ OneFormsZeroOne X)
    (x₀ : X) :
    ∃ (V : Set X) (u : SmoothCFunctions X), IsOpen V ∧ x₀ ∈ V ∧
      ∀ x ∈ V, proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⇑u) x) (1 : ℂ) = (g x) (1 : ℂ)

mem_OmegaD_zero_of_gext_analytic

Chart-holomorphy ⟹ 𝒪-section (OmegaD 0). A function F on an open V whose extension-by-zero Gext F, read in each point's own ℂ-chart, is *analytic* there, is a holomorphic section: F ∈ OmegaD 0 V. Both halves go through the Gext bridge — IsMeromorphic via Gext_chart_bridge (analytic ⟹ meromorphic), and 0 ≤ ordU via ordU_eq_orderAt_Gext plus AnalyticAt.meromorphicOrderAt_nonneg. The bridge that turns the planar cocycle holomorphy into a genuine cechH1 cocycle.

theorem mem_OmegaD_zero_of_gext_analytic {V : TopologicalSpace.Opens X} {F : V → ℂ}
    (hF : ∀ v : V, AnalyticAt ℂ (Gext F ∘ (chartAt (H := ℂ) (v : X)).symm)
      ((chartAt (H := ℂ) (v : X)) (v : X))) :
    F ∈ OmegaD (0 : Divisor X) V

diskBump

The cutoff bump for disk i: 1 on the closed disk closedBall (eᵢ) (radius i) (so on U_i), supported in closedBall (eᵢ) R ⊆ target, with R from exists_bumpOuterRadius.

noncomputable def diskBump (𝔇 : ChartDiskCover X) (i : 𝔇.ι) :
    ContDiffBump (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i) (𝔇.center i)) where

diskBump_support_subset_target

theorem diskBump_support_subset_target (𝔇 : ChartDiskCover X) (i : 𝔇.ι) :
    Metric.closedBall (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i) (𝔇.center i)) (𝔇.diskBump i).rOut
      ⊆ (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).target

cutoffPullback

The cutoff chart-pullback of g over disk i: the planar function w ↦ χᵢ(w) · (g (eᵢ.symm w)) (frame 1). Smooth, compactly supported, ℝ-linear in g.

noncomputable def cutoffPullback (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) :
    ℂ → ℂ

cutoffPullback_add

theorem cutoffPullback_add (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g₁ g₂ : SmoothCOneForms X) :
    𝔇.cutoffPullback i (g₁ + g₂) = 𝔇.cutoffPullback i g₁ + 𝔇.cutoffPullback i g₂

cutoffPullback_smul

theorem cutoffPullback_smul (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (c : ℝ) (g : SmoothCOneForms X) :
    𝔇.cutoffPullback i (c • g) = c • 𝔇.cutoffPullback i g

contDiff_cutoffPullback

The cutoff chart-pullback is globally smooth (the bump χᵢ times the chart-read datum, which is smooth on the chart target by contMDiffAt_chartRead_datum; outside the support χᵢ = 0).

theorem contDiff_cutoffPullback (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) :
    ContDiff ℝ (⊤ : ℕ∞) (𝔇.cutoffPullback i g)

hasCompactSupport_cutoffPullback

The cutoff chart-pullback is compactly supported (in closedBall (eᵢ) χᵢ.rOut, outside which the bump vanishes).

theorem hasCompactSupport_cutoffPullback (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) :
    HasCompactSupport (𝔇.cutoffPullback i g)

planarPrimitive

The planar primitive over disk i: the Cauchy transform of the cutoff chart-pullback. It is the explicit ℝ-linear witness whose planar ∂̄ is the cutoff pullback everywhere (so equals the chart-read g on U_i, where χᵢ = 1).

noncomputable def planarPrimitive (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) :
    ℂ → ℂ

contDiff_planarPrimitive

theorem contDiff_planarPrimitive (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) :
    ContDiff ℝ (⊤ : ℕ∞) (𝔇.planarPrimitive i g)

dbar_planarPrimitive

The planar ∂̄ of the primitive is the cutoff pullback (Cauchy–Pompeiu).

theorem dbar_planarPrimitive (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) (z : ℂ) :
    DbarDisk.dbar (𝔇.planarPrimitive i g) z = 𝔇.cutoffPullback i g z

planarPrimitive_add

theorem planarPrimitive_add (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g₁ g₂ : SmoothCOneForms X) :
    𝔇.planarPrimitive i (g₁ + g₂) = 𝔇.planarPrimitive i g₁ + 𝔇.planarPrimitive i g₂

planarPrimitive_smul

theorem planarPrimitive_smul (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (c : ℝ) (g : SmoothCOneForms X) :
    𝔇.planarPrimitive i (c • g) = c • 𝔇.planarPrimitive i g

diskSection

The disk-i primitive read back as a section on U i: x ↦ planarPrimitive i g (eᵢ x). The local ∂̄-primitive u_i of g on the disk U_i.

noncomputable def diskSection (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g : SmoothCOneForms X) :
    𝔇.U i → ℂ

diskSection_add

theorem diskSection_add (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (g₁ g₂ : SmoothCOneForms X) :
    𝔇.diskSection i (g₁ + g₂) = 𝔇.diskSection i g₁ + 𝔇.diskSection i g₂

diskSection_smul

theorem diskSection_smul (𝔇 : ChartDiskCover X) (i : 𝔇.ι) (c : ℝ) (g : SmoothCOneForms X) :
    𝔇.diskSection i (c • g) = c • 𝔇.diskSection i g

dbar_planarDiff_eq_zero

Cross-chart cancellation (planar form). On the overlap U_i ⊓ U_j, the difference of disk primitives read in chart i — z ↦ u_j(e_j(e_i⁻¹ z)) − u_i(z) — has vanishing planar ∂̄ at e_i x for every x ∈ U_i ∩ U_j. Mechanism: ∂̄(u_j∘τ) = conj(τ′)·(∂̄u_j ∘ τ) (Wirtinger chain rule), ∂̄u_i = cutoffPullback_i, ∂̄u_j = cutoffPullback_j; on the disks χ = 1, so these are g x (frameᵢ 1) and g x (frameⱼ 1); the (0,1) law turns them into conj(frame)·(g x 1), the frame is the inverse transition derivative, and the transition cocycle A_j = τ′·A_i cancels.

theorem dbar_planarDiff_eq_zero (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (i j : 𝔇.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) (hxj : x ∈ (𝔇.U j : Set X)) :
    DbarDisk.dbar (fun z => 𝔇.planarPrimitive j g
        ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center j)) ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).symm z))
        - 𝔇.planarPrimitive i g z)
      ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)) x) = 0

dbar_diskValue_eq_g

The disk primitive solves ∂̄ = g intrinsically on U_k. For x ∈ U_k, the intrinsic Wirtinger scalar of the disk-primitive *value function* wₖ = planarPrimitive k g ∘ e_k equals g x 1 — i.e. ∂̄wₖ = g at x. Mechanism (single-chart, mirroring dbar_planarDiffH_eq_zero): the generalized bridge dbar_apply_one_eq_dbarDisk' reads ∂̄wₖ in x's own chart as DbarDisk.dbar (planarPrimitive k g ∘ τ') (τ' = e_k ∘ eₓ.symm); the Wirtinger chain rule dbarDisk_comp_holo peels a conj(deriv τ') factor; dbar_planarPrimitive gives the cutoff pullback (χ = 1 on the disk), and frameVector_eq_deriv_transition_symm + oneForm_apply_conjLinear introduce a second conj(deriv σ) factor (σ = eₓ ∘ e_k.symm). The two cancel because σ ∘ τ' = id (deriv σ · deriv τ' = 1), leaving exactly g x 1.

theorem dbar_diskValue_eq_g (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (k : 𝔇.ι) {x : X} (hxk : x ∈ (𝔇.U k : Set X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ)
        (fun y => 𝔇.planarPrimitive k g ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center k)) y)) x) (1 : ℂ)
      = (g x) (1 : ℂ)

differentiableAt_planarDiff

The chart-i read of the cochain difference is holomorphic (ℂ-differentiable) at e_i x for x ∈ U_i ⊓ U_j: Lemma A dbar_planarDiff_eq_zero (∂̄ = 0) + local smoothness (the transition is holomorphic, the primitives are C^∞) via local Cauchy–Riemann.

theorem differentiableAt_planarDiff (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (i j : 𝔇.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) (hxj : x ∈ (𝔇.U j : Set X)) :
    DifferentiableAt ℂ (fun z => 𝔇.planarPrimitive j g
        ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center j)) ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).symm z))
        - 𝔇.planarPrimitive i g z)
      ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)) x)

dbar_planarDiffH_eq_zero

Second cancellation (the ∂̄-image is a coboundary). For a global potential h, the chart-i read of u_i − h (with u_i = planarPrimitive i (∂̄h)) has vanishing planar ∂̄ at e_i x: both are ∂̄-primitives of ∂̄h. Mechanism mirrors Lemma A — ∂̄u_i = cutoffPullback i (∂̄h), while ∂̄(h∘e_i.symm) = conj(deriv σ)·(∂̄h x 1) via the Wirtinger chain rule + the own-chart bridge dbar_apply_one_eq_dbarDisk; the *direct* frame form frameVector_eq_deriv_transition_symm makes the two equal (no inverse-derivative needed).

theorem dbar_planarDiffH_eq_zero (𝔇 : ChartDiskCover X) (h : SmoothCFunctions X) (i : 𝔇.ι) {x : X}
    (hxi : x ∈ (𝔇.U i : Set X)) :
    DbarDisk.dbar (fun z => 𝔇.planarPrimitive i (dbarL h) z
        - h ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).symm z))
      ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)) x) = 0

differentiableAt_planarDiffH

The chart-i read of u_i − h is holomorphic at e_i x (dbar_planarDiffH_eq_zero + local smoothness + local Cauchy–Riemann). The single-chart analogue of differentiableAt_planarDiff.

theorem differentiableAt_planarDiffH (𝔇 : ChartDiskCover X) (h : SmoothCFunctions X) (i : 𝔇.ι)
    {x : X} (hxi : x ∈ (𝔇.U i : Set X)) :
    DifferentiableAt ℂ (fun z => 𝔇.planarPrimitive i (dbarL h) z
        - h ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).symm z))
      ((extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)) x)

gextH_diff_analyticAt

Gext (u_i − h), read in each point's own chart, is analytic — single-chart analogue of gext_diff_analyticAt (using differentiableAt_planarDiffH).

theorem gextH_diff_analyticAt (𝔇 : ChartDiskCover X) (h : SmoothCFunctions X) (i : 𝔇.ι)
    (F : ↥(𝔇.U i) → ℂ)
    (hFeq : ∀ v : ↥(𝔇.U i), F v
      = 𝔇.planarPrimitive i (dbarL h) (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i) v.1) - h v.1)
    (w : ↥(𝔇.U i)) :
    AnalyticAt ℂ (Gext F ∘ (chartAt (H := ℂ) (w : X)).symm)
      ((chartAt (H := ℂ) (w : X)) (w : X))

rawCochain

The linear 0-cochain of disk primitives: g ↦ (i ↦ [u_i]), the germ-classes of the local ∂̄-primitives. ℝ-linear in g (via planarPrimitive linearity + toGerm). Its cechDelta0 is the Dolbeault → Čech cocycle.

noncomputable def rawCochain (𝔇 : ChartDiskCover X) :
    SmoothCOneForms X →ₗ[ℝ] 𝔇.toFiniteCover.Cochain0 where

gext_diff_analyticAt

The cochain difference F = u_j − u_i on the overlap V = U_i ⊓ U_j, read in *each point's own* chart via the extension-by-zero Gext, is analytic there. Chart-i holomorphy (differentiableAt_planarDiff, an open DifferentiableOn ⟹ AnalyticAt) transported to the point's own chart by analyticAt_chart_change. The hypothesis on F is its overlap value.

theorem gext_diff_analyticAt (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (i j : 𝔇.ι) (F : ↥(𝔇.U i ⊓ 𝔇.U j) → ℂ)
    (hFeq : ∀ w : ↥(𝔇.U i ⊓ 𝔇.U j),
      F w = 𝔇.planarPrimitive j g (extChartAt 𝓘(ℝ, ℂ) (𝔇.center j) w.1)
        - 𝔇.planarPrimitive i g (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i) w.1))
    (w : ↥(𝔇.U i ⊓ 𝔇.U j)) :
    AnalyticAt ℂ (Gext F ∘ (chartAt (H := ℂ) (w : X)).symm)
      ((chartAt (H := ℂ) (w : X)) (w : X))

cechDelta0_rawCochain_mem_cocycles1

The cocycle lands in Z¹(𝒪). cechDelta0 (rawCochain g) is a Čech 1-cocycle of 𝒪: it is in ker cechDelta1 (any germ cochain) and its overlap germs are holomorphic (gext_diff_analyticAt + the mem_OmegaD_zero_of_gext_analytic bridge). Needs g a (0,1)-form (the conjugate-linearity used by Lemma A).

theorem cechDelta0_rawCochain_mem_cocycles1 (𝔇 : ChartDiskCover X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) :
    𝔇.toFiniteCover.cechDelta0 (𝔇.rawCochain g) ∈ 𝔇.toFiniteCover.cocycles1 (0 : Divisor X)

dbar_solvable_locally_manifold

(Analytic sub-kernel.) Local ∂̄-solvability on the manifold: any smooth (0,1)-form g (in OneFormsZeroOne X) is, near every point x₀, the ∂̄ of a smooth function u. Proven completely from the value-1 local primitive exists_localPrimitive_apply_one (the finer sub-kernel) via the value-1-to-CLM upgrade dbar_eq_of_apply_one: the full intrinsic CLM equation dbar u x = g x follows because both sides are (0,1)-forms determined by their Wirtinger scalar. The local primitives u it produces are the u_i whose differences u_i − u_j are the Dolbeault → Čech cocycle.

theorem dbar_solvable_locally_manifold (g : SmoothCOneForms X) (hg : g ∈ OneFormsZeroOne X)
    (x₀ : X) :
    ∃ (V : Set X) (u : SmoothCFunctions X), IsOpen V ∧ x₀ ∈ V ∧ ∀ x ∈ V, (dbar u) x = g x

dolbeaultToCechCocycle

(Analytic sub-kernel — the Dolbeault → Čech cocycle operator.) The ℝ-linear map sending a (0,1)-form g ∈ A^{0,1} to the Čech 1-cocycle {[u_j] − [u_i]} = cechDelta0 {[u_i]} ∈ Z¹(𝔘, 𝒪), where u_i solves ∂̄u_i = g on the (simply-connected / disk) cover set U_i.

This packages the *only* PDE content of the Dolbeault → Čech direction: global ∂̄-solvability on each Leray cover set (DbarLocal.dbar_solvable_locally only gives a *point*-neighborhood; the disk-global solve, via the Cauchy transform, is what is needed) — crucially linear in g (the Cauchy-transform solution operator is linear), so the whole assignment is ℝ-linear. The output lands in cocycles1 because (i) cechDelta0 c ∈ ker cechDelta1 for *any* germ-class cochain c (cechDelta0_mem_ker_cechDelta1, complete), and (ii) on each overlap U_i ∩ U_j the difference u_j − u_i is holomorphic (∂̄(u_j − u_i) = g − g = 0), so cechDelta0 {[u_i]} ∈ sections1 0.

noncomputable def dolbeaultToCechCocycle (𝔇 : ChartDiskCover X) :
    ↥(OneFormsZeroOne X) →ₗ[ℝ] ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))

dolbeaultToCechCocycle_dbarImage_le

(Analytic sub-kernel — well-definedness of Dolbeault → Čech.) A global ∂̄-image g = ∂̄h is sent to a Čech coboundary, hence to 0 in H¹: each local primitive difference u_i − h is holomorphic on U_i (∂̄(u_i − h) = g − g = 0), so {[u_i − h]} ∈ sections0 0 and cechDelta0 {[u_i]} = cechDelta0 {[u_i − h]} ∈ coboundaries1 0 (the global h contributes 0 to cechDelta0). This is exactly the statement that dbarImageInZeroOne X lies in the kernel of the composite A^{0,1} → Z¹ → H¹, which makes the lift to DolbeaultH01 = A^{0,1}/im ∂̄ well-defined.

theorem dolbeaultToCechCocycle_dbarImage_le (𝔇 : ChartDiskCover X) :
    dbarImageInZeroOne X ≤ LinearMap.ker
      ((Submodule.mkQ ((𝔇.toFiniteCover.coboundaries1 (0 : Divisor X)).submoduleOf
          (𝔇.toFiniteCover.cocycles1 (0 : Divisor X)))).restrictScalars ℝ
        ∘ₗ dolbeaultToCechCocycle 𝔇)

dolbeault_to_cech

Dolbeault → Čech. The ℝ-linear map H^{0,1}(X) → H¹(X, 𝒪). Assembled completely from the analytic cocycle operator dolbeaultToCechCocycle and its well-definedness dolbeaultToCechCocycle_dbarImage_le: project the cocycle to cechH1 = Z¹/B¹ (Submodule.mkQ, scalar-restricted ℂ → ℝ), then lift through the Dolbeault quotient A^{0,1}/im ∂̄ (Submodule.liftQ, justified by the kernel inclusion). All genuine content lives in the two named sub-kernels above.

noncomputable def dolbeault_to_cech (𝔇 : ChartDiskCover X) :
    DolbeaultH01 X →ₗ[ℝ] 𝔇.toFiniteCover.cechH1 0