16.12. Dbar.HoloRep🔗

Jacobians.Dbar.HoloRep — source

nhdsNE_neBot

The punctured neighbourhood of a point of a ℂ-manifold is NeBot (no isolated points).

theorem nhdsNE_neBot {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X) :
    (𝓝[≠] x).NeBot

holoRep

A holomorphic representative function of an OmegaDGerm 0-class (chosen).

noncomputable def holoRep {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) : W → ℂ

holoRep_mem

theorem holoRep_mem {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) : holoRep hg ∈ OmegaD (0 : Divisor X) W

toGerm_holoRep

theorem toGerm_holoRep {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) : toGerm W (holoRep hg) = g

holoFn

The analytic representative F = limit-repair(Gext (holoRep hg)) : X → ℂ.

noncomputable def holoFn {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) : X → ℂ

gextLimRep_chart_analyticAt

(Chart-analyticity of the analytic representative.) For a holomorphic (OmegaD 0) function g on ↥W, the limit-repair x ↦ limUnder (𝓝[≠] x) (Gext g) is chart-analytic at every y ∈ W (it discards the removable-singularity junk of Gext g, agreeing with the normal-form representative toMeromorphicNFOn of the chart-read). Re-derivation of DolbeaultComparisonInverse.gextLimRep_chart_analyticAt.

theorem gextLimRep_chart_analyticAt {W : Opens X} {g : W → ℂ} (hg : g ∈ OmegaD 0 W)
    {y : X} (hy : y ∈ W) :
    AnalyticAt ℂ ((fun x => limUnder (𝓝[≠] x) (Gext g)) ∘ (chartAt (H := ℂ) y).symm)
      ((chartAt (H := ℂ) y) y)

holoFn_chart_analyticAt

The chart-read of the analytic representative holoFn hg is AnalyticAt at the chart centre.

theorem holoFn_chart_analyticAt {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) {y : X} (hy : y ∈ W) :
    AnalyticAt ℂ (holoFn hg ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y)

contMDiffAt_real_of_chart_analyticAt

Chart-analytic ⟹ real-smooth. If a ℂ-valued function h read in the chart at y is complex-analytic at the chart image, then h is real-C^∞ at y.

theorem contMDiffAt_real_of_chart_analyticAt {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {h : X → ℂ} {y : X}
    (ha : AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y)) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) h y

holoFn_contMDiffAt

The analytic representative is real-smooth at every point of the open.

theorem holoFn_contMDiffAt {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) {y : X} (hy : y ∈ W) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (holoFn hg) y

proj01_restrictScalars_eq_zero

proj01 annihilates the ℝ-restriction of a complex-linear map.

theorem proj01_restrictScalars_eq_zero (L : ℂ →L[ℂ] ℂ) : proj01 (L.restrictScalars ℝ) = 0

holoFn_dbar_eq_zero

A holomorphic representative has vanishing ∂̄. For g ∈ OmegaDGerm 0 W, the intrinsic ∂̄ of its analytic representative holoFn hg is 0 at every x ∈ W.

theorem holoFn_dbar_eq_zero {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) {x : X} (hx : x ∈ W) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (holoFn hg) x) = 0

holoFn_eq_of_tendsto

holoFn reads off a continuous representative's value. If the holomorphic germ class g has a representative F : ↥W → ℂ (toGerm W F = g) whose extension Gext F has limit c along 𝓝[≠] y, then holoFn hg y = c.

theorem holoFn_eq_of_tendsto {W : Opens X} {g : MGerm W} (hg : g ∈ OmegaDGerm (0 : Divisor X) W)
    (F : W → ℂ) (hgF : toGerm W F = g) {y : X} (hy : y ∈ W) {c : ℂ}
    (hc : Tendsto (Gext F) (𝓝[≠] y) (𝓝 c)) : holoFn hg y = c

holoFn_eq_holoRep_of_chart_analyticAt

holoFn reads off holoRep at analytic points. If at z ∈ W the chart-read of Gext (holoRep hg) is analytic at the chart image, the limit-repair recovers the genuine value holoFn hg z = holoRep hg ⟨z, hz⟩.

theorem holoFn_eq_holoRep_of_chart_analyticAt {W : Opens X} {g : MGerm W}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) W) {z : X} (hz : z ∈ W)
    (ha : AnalyticAt ℂ (Gext (holoRep hg) ∘ (chartAt (H := ℂ) z).symm) ((chartAt (H := ℂ) z) z)) :
    holoFn hg z = holoRep hg ⟨z, hz⟩

toGerm_holoFn

The analytic representative reads back the germ. toGerm W (holoFn hg ∘ val) = g.

theorem toGerm_holoFn {W : Opens X} {g : MGerm W} (hg : g ∈ OmegaDGerm (0 : Divisor X) W) :
    toGerm W (fun v : W => holoFn hg v.1) = g