17.4. DolbeaultComparison.DolbeaultComparison🔗

Jacobians.DolbeaultComparison.DolbeaultComparison — source

contMDiff_proj01_section

x ↦ proj01 (α x) is a smooth section whenever α is. This is exactly the smoothness mechanism of RealForms.dbar (proj01 is a fixed CLM and slides through the tangent symmL because mulI commutes with tangentCoordChange), with the concrete section differential u replaced by an arbitrary smooth section α.

theorem contMDiff_proj01_section (α : SmoothCOneForms X) :
    ContMDiff (𝓘(ℝ, ℂ)) (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ →L[ℝ] ℂ)) (⊤ : ℕ∞)
      (fun x => (⟨x, proj01 (α x)⟩ : Bundle.TotalSpace (ℂ →L[ℝ] ℂ)
        (fun x : X => TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x)))

proj01Section

proj01 applied fiberwise to a smooth 1-form, packaged as a smooth 1-form.

noncomputable def proj01Section (α : SmoothCOneForms X) : SmoothCOneForms X where

proj01Section_apply

@[simp] theorem proj01Section_apply (α : SmoothCOneForms X) (x : X) :
    (proj01Section α) x = proj01 (α x)

proj01L

proj01 as an ℝ-linear endomorphism of A¹ (deliverable 1): the (0,1)-fiber projection applied fiberwise. map_add'/map_smul' mirror dbar_add/dbar_smul — proj01 is ℝ-linear on each fiber.

noncomputable def proj01L : SmoothCOneForms X →ₗ[ℝ] SmoothCOneForms X where

proj01L_apply

@[simp] theorem proj01L_apply (α : SmoothCOneForms X) : proj01L α = proj01Section α

OneFormsZeroOne

The (0,1)-forms A^{0,1} X (deliverable 2): the image of the (0,1)-projection proj01L. A Submodule ℝ of A¹ = SmoothCOneForms X. (proj01 is an idempotent picking out the conjugate-ℂ-linear part of each fiber, so its range is exactly the (0,1)-forms.)

noncomputable def OneFormsZeroOne (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    Submodule ℝ (SmoothCOneForms X)

dbarL_eq_proj01L_differential

∂̄u = proj01L (du) as 1-forms: both have fiber x ↦ proj01 ((differential u) x).

theorem dbarL_eq_proj01L_differential (u : SmoothCFunctions X) :
    dbarL u = proj01L (differential u)

dbarL_mem_zeroOne

im ∂̄ ⊆ A^{0,1} (deliverable 3): ∂̄u is a (0,1)-form, since ∂̄u = proj01L (du) lies in the range of proj01L. This is what makes LinearMap.range dbarL a submodule of OneFormsZeroOne, hence the cokernel DolbeaultH01 below well-formed.

theorem dbarL_mem_zeroOne (u : SmoothCFunctions X) : dbarL u ∈ OneFormsZeroOne X

dbarImageInZeroOne

im ∂̄ viewed inside A^{0,1} (legitimate as a submodule of ↥(OneFormsZeroOne X) precisely by range_dbarL_le_zeroOne / dbarL_mem_zeroOne).

noncomputable def dbarImageInZeroOne (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    Submodule ℝ ↥(OneFormsZeroOne X)

DolbeaultH01

Dolbeault cohomology H^{0,1}(X) (deliverable 4): the cokernel of ∂̄ on the (0,1)-forms, A^{0,1} ⧸ im ∂̄. On a (compact) Riemann surface A^{0,2} = 0, so the Dolbeault complex A⁰ →[∂̄] A^{0,1} → 0 has this single nontrivial cohomology and H^{0,1} *is* this cokernel. An ℝ-module (the section space A¹ carries only Module ℝ; the hom-bundle fiber ℂ →L[ℝ] ℂ is not propagated to a Module ℂ on the sections — see the comparison's scalar note).

abbrev DolbeaultH01 (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] : Type _