17.8. DolbeaultComparison.DolbeaultH01🔗

Jacobians.DolbeaultComparison.DolbeaultH01 — source

dbar_add

∂̄ is additive (differential is additive via mfderiv_add; proj01 is linear).

theorem dbar_add (u v : SmoothCFunctions X) : dbar (u + v) = dbar u + dbar v

dbar_smul

∂̄ is ℝ-homogeneous (const_smul_mfderiv; proj01 is linear).

theorem dbar_smul (c : ℝ) (u : SmoothCFunctions X) : dbar (c • u) = c • dbar u

dbarL

The intrinsic ∂̄ operator as an ℝ-linear map A⁰ →ₗ[ℝ] A¹ (upgrade of the bare dbar), so that LinearMap.range dbarL — the image needed to form H^{0,1} — is available.

noncomputable def dbarL : SmoothCFunctions X →ₗ[ℝ] SmoothCOneForms X where

dbarL_apply

@[simp] theorem dbarL_apply (u : SmoothCFunctions X) : dbarL u = dbar u