A machine-checked solution to the Jacobians challenge

16.5. Dbar.CechDiskAcyclicAssembly🔗

Jacobians.Dbar.CechDiskAcyclicAssemblysource

omegaD_zero_of_chart_analyticAt

Chart-analytic ambient ⟹ holomorphic section. If H : X → ℂ reads -analytically in the chart at every y ∈ U, then H ∘ val ∈ OmegaD 0 U.

theorem omegaD_zero_of_chart_analyticAt {U : Opens X} {H : X → ℂ}
    (hH : ∀ y ∈ U, AnalyticAt ℂ (H ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y)) :
    (H ∘ (Subtype.val : U → X)) ∈ OmegaD (0 : Divisor X) U