16.13. Dbar.RealForms🔗

Jacobians.Dbar.RealForms — source

SmoothCFunctions

Real-smooth ℂ-valued functions A⁰ on X — the source of ∂̄: real-C^∞ maps X → ℂ (over the real model, i.e. NOT holomorphic). A real vector space.

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

trivial_continuousSMul_real

The trivial ℂ-bundle is a continuous ℝ-module — the one instance Mathlib's hom-of-bundles machinery needs but does not auto-derive for the sub-field ℝ (Trivial X ℂ x is defeq ℂ, and the ℂ-ℝ-module diamond is resolved by the file set_option).

instance trivial_continuousSMul_real {X : Type*} (x : X) :
    ContinuousSMul ℝ (Bundle.Trivial X ℂ x)

SmoothCOneForms

Smooth ℂ-valued 1-forms on X: smooth sections of the real cotangent valued in ℂ (real-linear maps TangentSpace 𝓘(ℝ,ℂ) x → ℂ). The intrinsic container for the Dolbeault complex A¹ = A^{1,0} ⊕ A^{0,1}. A real (Module ℝ) vector space.

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

differential

The de Rham differential d : A⁰ → A¹ — the real differential du = mfderiv u of a smooth ℂ-valued function, a smooth ℂ-valued 1-form. (∂̄u is its (0,1)-part; ∂u the (1,0)-part.) The section-smoothness is the standard "the differential of a C^∞ function is a C^∞ 1-form" (mfderiv_const in tangent coordinates, bridged to the trivial-bundle codomain ℂ).

noncomputable def differential {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (u : SmoothCFunctions X) :
    SmoothCOneForms X where

mulI

Multiplication by i as a real-linear endomorphism of ℂ (= J, the complex structure on the real tangent space T_x ≅ ℂ).

noncomputable def mulI : ℂ →L[ℝ] ℂ

proj01

The (0,1)-projection on real-linear forms ℂ →L[ℝ] ℂ: P(α) = ½(α + i·α(i·−)), the conjugate-ℂ-linear (Cauchy–Riemann) part. A fixed continuous-linear fiber endomorphism; applied fiberwise to du it carves ∂̄u out of the de Rham differential.

noncomputable def proj01 : (ℂ →L[ℝ] ℂ) →L[ℝ] (ℂ →L[ℝ] ℂ)

proj01_apply

proj01 written out: P(α) = ½(α + i·α(i·−)).

theorem proj01_apply (α : ℂ →L[ℝ] ℂ) :
    proj01 α = (2 : ℝ)⁻¹ • (α + mulI.comp (α.comp mulI))

restrictScalars_comp_mulI

A real-restricted ℂ-linear map commutes with mulI = (·*i) (the ℂ-(i·) action).

theorem restrictScalars_comp_mulI (L : ℂ →L[ℂ] ℂ) :
    (L.restrictScalars ℝ).comp mulI = mulI.comp (L.restrictScalars ℝ)

tangentCoordChange_comp_mulI

The tangent coordChange of the complex manifold is ℂ-linear, hence commutes with mulI: fderiv ℝ of a holomorphic transition is restrictScalars of fderiv ℂ.

theorem tangentCoordChange_comp_mulI {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {a b z : X}
    (hz : z ∈ (extChartAt 𝓘(ℝ, ℂ) a).source ∩ (extChartAt 𝓘(ℝ, ℂ) b).source) :
    (tangentCoordChange 𝓘(ℝ, ℂ) a b z).comp mulI =
      mulI.comp (tangentCoordChange 𝓘(ℝ, ℂ) a b z)

dbar

The Dolbeault ∂̄ operator A⁰ → A^{0,1} ⊆ A¹: the (0,1)-part of the de Rham differential, ∂̄u = proj01 ∘ du. A smooth ℂ-valued 1-form.

noncomputable def dbar {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (u : SmoothCFunctions X) :
    SmoothCOneForms X where