17.6. DolbeaultComparison.DolbeaultComparisonInverse🔗

Jacobians.DolbeaultComparison.DolbeaultComparisonInverse — source

exists_smoothPartitionOfUnity_subordinate

(Čech → Dolbeault backbone, complete.) A smooth partition of unity subordinate to the finite cover 𝔘, over the real-manifold structure 𝓘(ℝ, ℂ). The input for the globalization h_i := ∑_k ρ_k · f_ik.

theorem exists_smoothPartitionOfUnity_subordinate {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (𝔘 : FiniteCover X) :
    ∃ ρ : SmoothPartitionOfUnity 𝔘.ι 𝓘(ℝ, ℂ) X (Set.univ : Set X),
      ρ.IsSubordinate (fun i => (𝔘.U i : Set X))

ofRealCM

ℝ → ℂ as a smooth map, for coercing the real-valued PoU functions to SmoothCFunctions.

noncomputable def ofRealCM : ContMDiffMap (𝓘(ℝ)) (𝓘(ℝ, ℂ)) ℝ ℂ (⊤ : ℕ∞)

cechPoU

A fixed smooth partition of unity subordinate to the cover (exists\_smoothPartitionOfUnity\_ subordinate) — the globalization input for the inverse map.

noncomputable def cechPoU (𝔇 : ChartDiskCover X) :
    SmoothPartitionOfUnity 𝔇.toFiniteCover.ι 𝓘(ℝ, ℂ) X (Set.univ : Set X)

cechPoU_subordinate

theorem cechPoU_subordinate (𝔇 : ChartDiskCover X) :
    (cechPoU 𝔇).IsSubordinate (fun i => (𝔇.U i : Set X))

rhoC

The k-th PoU function as a complex SmoothCFunctions (ρ̃_k = ofReal ∘ ρ_k).

noncomputable def rhoC (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) : SmoothCFunctions X

dbarRho

∂̄ρ_k as a global (0,1)-form.

noncomputable def dbarRho (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) : SmoothCOneForms X

sum_rhoC

The PoU functions sum to the constant 1 (finite cover ⇒ plain Finset.sum).

theorem sum_rhoC (𝔇 : ChartDiskCover X) : ∑ k, rhoC 𝔇 k = 1

dbarL_one_eq_zero

The gluing relation ∑_k ∂̄ρ_k = 0 (∂̄ of ∑ρ_k = 1 is ∂̄1 = 0). This is what makes the local ∂̄η_i agree on overlaps.

theorem dbarL_one_eq_zero : dbarL (1 : SmoothCFunctions X) = 0

sum_dbarRho_eq_zero

The gluing relation ∑_k ∂̄ρ_k = 0 — ∂̄ of ∑_k ρ_k = 1 is ∂̄1 = 0. This is what makes the local primitives ∂̄η_i agree on overlaps (so they glue to a global (0,1)-form). The summand forms are dbarRho 𝔇 k = dbarL (rhoC 𝔇 k); dbarL is ℝ-linear, so the sum commutes through it (map_sum) onto ∑_k ρ_k = 1 (sum_rhoC).

Historical note: summing SmoothCOneForms (Finset.sum) was once thought to be blocked by the Module ℝ section-instance diamond (reference_module_real_diamond). It is not: with the file-level set_option backward.isDefEq.respectTransparency false already in force (for the hom-bundle section instances), AddCommMonoid (SmoothCOneForms X) synthesises and the form-sum elaborates normally.

theorem sum_dbarRho_eq_zero (𝔇 : ChartDiskCover X) :
    ∑ k, dbarRho 𝔇 k = 0

sum_rhoC_apply

Value form of sum_rhoC: ∑_k ρ_k x = 1 pointwise.

theorem sum_rhoC_apply (𝔇 : ChartDiskCover X) (x : X) : ∑ k, (rhoC 𝔇 k x) = 1

sum_dbarRho_apply

Value form of sum_dbarRho_eq_zero: ∑_k ∂̄ρ_k x = 0 pointwise.

theorem sum_dbarRho_apply (𝔇 : ChartDiskCover X) (x : X) :
    ∑ k, ((dbarRho 𝔇 k) x) = 0

contMDiffAt_cSmul_section

(ContMDiffAt form, the workhorse.) Scaling a smooth (0,1)-valued section by a ℂ-valued function, fiberwise, is smooth at x₀ when both are. The ℂ-smul is post-composition on the trivial codomain (z • β = (mul ℝ ℂ z).comp β), so it slides through the tangent symmL, reducing to clm_comp of the smooth x ↦ mul ℝ ℂ (F x) and the smooth in-coordinates of s.

theorem contMDiffAt_cSmul_section {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {F : X → ℂ}
    {s : ∀ x : X, TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x} {x₀ : X}
    (hF : ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) F x₀)
    (hs : ContMDiffAt 𝓘(ℝ, ℂ) (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ →L[ℝ] ℂ)) (⊤ : ℕ∞)
      (fun x => (⟨x, s x⟩ : Bundle.TotalSpace (ℂ →L[ℝ] ℂ)
        (fun x : X => TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x))) x₀) :
    ContMDiffAt 𝓘(ℝ, ℂ) (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ →L[ℝ] ℂ)) (⊤ : ℕ∞)
      (fun x => (⟨x, (F x) • (s x)⟩ : Bundle.TotalSpace (ℂ →L[ℝ] ℂ)
        (fun x : X => TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x))) x₀

contMDiff_cSmul_section

Global form of contMDiffAt_cSmul_section for a SmoothCFunctions scalar and a smooth form.

theorem contMDiff_cSmul_section (c : SmoothCFunctions X) (g : SmoothCOneForms X) :
    ContMDiff (𝓘(ℝ, ℂ)) (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ →L[ℝ] ℂ)) (⊤ : ℕ∞)
      (fun x => (⟨x, (c x) • (g x)⟩ : Bundle.TotalSpace (ℂ →L[ℝ] ℂ)
        (fun x : X => TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x)))

cSmulForm

ℂ-valued smooth-function scaling of a (0,1)-valued smooth form (the double-sum term builder): (c • g) x = c x • g x, a smooth (0,1)-valued form.

noncomputable def cSmulForm (c : SmoothCFunctions X) (g : SmoothCOneForms X) :
    SmoothCOneForms X where

cSmulForm_apply

@[simp] theorem cSmulForm_apply (c : SmoothCFunctions X) (g : SmoothCOneForms X) (x : X) :
    cSmulForm c g x = (c x) • (g x)

proj01_smul

The (0,1)-projection commutes with ℂ-scaling of the codomain: proj01 (z • α) = z • proj01 α (z factors out of the Wirtinger average).

theorem proj01_smul (z : ℂ) (α : ℂ →L[ℝ] ℂ) : proj01 (z • α) = z • proj01 α

cSmulForm_mem_zeroOne

ℂ-scaling preserves the (0,1)-forms: c • g ∈ A^{0,1} whenever g ∈ A^{0,1}. (Witness c • h where g = proj01L h; proj01 commutes with the ℂ-scale, proj01_smul.)

theorem cSmulForm_mem_zeroOne (c : SmoothCFunctions X) {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) : cSmulForm c g ∈ OneFormsZeroOne X

contMDiffMul_real_complex

ℂ-multiplication is real-C^∞ (it is ℝ-bilinear) — the instance Mathlib provides only over the *complex* model 𝓘(ℂ), supplied here over the real model 𝓘(ℝ,ℂ) so that SmoothCFunctions X is a ring (needed for the ∂̄ Leibniz rule).

instance contMDiffMul_real_complex : ContMDiffMul 𝓘(ℝ, ℂ) (⊤ : ℕ∞) ℂ

dbarL_eq_zero_of_notMem_tsupport

∂̄ shrinks support: ∂̄u x = 0 wherever u is locally constant (x ∉ tsupport u). (Stated pointwise — section coes are dependently typed, so tsupport of a section is not available.)

theorem dbarL_eq_zero_of_notMem_tsupport (u : SmoothCFunctions X) {x : X}
    (hx : x ∉ tsupport (⇑u : X → ℂ)) : (dbarL u) x = 0

dbarRho_eq_zero_of_notMem

∂̄ρ_k x = 0 for x ∉ tsupport ρ_k — so ∂̄ρ_k is supported in U_k (ρ_k subordinate).

theorem dbarRho_eq_zero_of_notMem (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) {x : X}
    (hx : x ∉ tsupport (cechPoU 𝔇 k)) : (dbarRho 𝔇 k) x = 0

nhdsNE_neBot_of_chart

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

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

Gext_add

Gext is additive (extension by 0).

theorem Gext_add {X : Type*} [TopologicalSpace X] {U : Opens X} (f g : U → ℂ) :
    Gext (f + g) = Gext f + Gext g

Gext_smul

Gext is homogeneous (extension by 0).

theorem Gext_smul {X : Type*} [TopologicalSpace X] {U : Opens X} (c : ℂ) (g : U → ℂ) :
    Gext (c • g) = c • Gext g

Gext_sub

Gext respects subtraction (extension by 0).

theorem Gext_sub {X : Type*} [TopologicalSpace X] {U : Opens X} (f g : U → ℂ) :
    Gext (f - g) = Gext f - Gext g

holoFn_tendsto

For a holomorphic (OmegaDGerm 0) class, the analytic representative Gext(holoRep) has a genuine limit along 𝓝[≠] x at every x ∈ V (order ≥ 0 ⟹ the limit exists; this is holoFn x).

theorem holoFn_tendsto {V : Opens X} {g : MGerm V} (hg : g ∈ OmegaDGerm (0 : Divisor X) V) {x : X}
    (hx : x ∈ V) : ∃ c, Tendsto (Gext (holoRep hg)) (𝓝[≠] x) (𝓝 c)

holoFn_add

holoFn is additive at every x ∈ V (the choice in holoRep washes out: the limit-repair limUnder is insensitive to codiscrete junk, so it depends only on the germ class, and the limit is additive).

theorem holoFn_add {V : Opens X} {g₁ g₂ : MGerm V} (hg₁ : g₁ ∈ OmegaDGerm (0 : Divisor X) V)
    (hg₂ : g₂ ∈ OmegaDGerm (0 : Divisor X) V) (hg : g₁ + g₂ ∈ OmegaDGerm (0 : Divisor X) V)
    {x : X} (hx : x ∈ V) : holoFn hg x = holoFn hg₁ x + holoFn hg₂ x

holoFn_smul

holoFn is homogeneous at every x ∈ V (same washout as holoFn_add).

theorem holoFn_smul {V : Opens X} (c : ℂ) {g : MGerm V} (hg : g ∈ OmegaDGerm (0 : Divisor X) V)
    (hcg : c • g ∈ OmegaDGerm (0 : Divisor X) V) {x : X} (hx : x ∈ V) :
    holoFn hcg x = c • holoFn hg x

holoFn_sub

holoFn respects subtraction at x ∈ V (same washout as holoFn_add).

theorem holoFn_sub {V : Opens X} {g₁ g₂ : MGerm V} (hg₁ : g₁ ∈ OmegaDGerm (0 : Divisor X) V)
    (hg₂ : g₂ ∈ OmegaDGerm (0 : Divisor X) V) (hg : g₁ - g₂ ∈ OmegaDGerm (0 : Divisor X) V)
    {x : X} (hx : x ∈ V) : holoFn hg x = holoFn hg₁ x - holoFn hg₂ x

holoFn_congr

holoFn depends only on the germ class. Two memberships of equal germs give the same holoFn at points of V (the holoRep choice washes out).

theorem holoFn_congr {V : Opens X} {g g' : MGerm V} (hg : g ∈ OmegaDGerm (0 : Divisor X) V)
    (hg' : g' ∈ OmegaDGerm (0 : Divisor X) V) (hgg : g = g') {x : X} (hx : x ∈ V) :
    holoFn hg x = holoFn hg' x

cocycle_mem

The (j,k) component of a Čech 1-cocycle is a holomorphic (OmegaDGerm 0) germ-class on the overlap U_j ⊓ U_k (the sections1 part of cocycles1).

theorem cocycle_mem (𝔇 : ChartDiskCover X) (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)))
    (j k : 𝔇.toFiniteCover.ι) :
    (f : 𝔇.toFiniteCover.Cochain1) (j, k) ∈ OmegaDGerm (0 : Divisor X) (𝔇.U j ⊓ 𝔇.U k)

cechTerm

The (j,k) double-sum term T_jk = (ρ_j · F_jk) • ∂̄ρ_k, a global smooth (0,1)-valued form (F_jk = holoFn = the analytic representative). Globally smooth by a 3-case ContMDiffAt argument: on the overlap U_j ⊓ U_k everything is smooth (F_jk via holoFn_contMDiffAt); off tsupport ρ_j the factor ρ_j vanishes; off tsupport ρ_k the factor ∂̄ρ_k vanishes — and these three opens cover X (a point in neither support-complement lies in tsupport ρ_j ∩ tsupport ρ_k ⊆ U_j ⊓ U_k).

noncomputable def cechTerm (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (j k : 𝔇.toFiniteCover.ι) :
    SmoothCOneForms X where

proj01_apply_val

proj01 α at a vector, written out: proj01 α v = ½(α v + i·α(i·v)) (the Wirtinger average).

theorem proj01_apply_val (α : ℂ →L[ℝ] ℂ) (v : ℂ) :
    proj01 α v = (2 : ℂ)⁻¹ * (α v + Complex.I * α (Complex.I * v))

proj01_idempotent

The (0,1)-projection is idempotent (proj01²= proj01).

theorem proj01_idempotent (α : ℂ →L[ℝ] ℂ) : proj01 (proj01 α) = proj01 α

holoFn_restrict

holoFn is restriction-compatible. For V ≤ U and x ∈ V, the analytic rep of the restricted germ agrees with the original at x (limUnder depends only on the germ, which restriction preserves at x).

theorem holoFn_restrict {U V : Opens X} (h : V ≤ U) {g : MGerm U}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) U) {x : X} (hx : x ∈ V) :
    holoFn (rawRestrictG_omegaDGerm h hg) x = holoFn hg x

holoFn_cocycle_add

The Čech cocycle relation, at the holoFn value level. For a 1-cocycle f (so δ¹f = 0) and y ∈ U_i ⊓ U_j ⊓ U_k, the holomorphic representatives satisfy holoFn(f_ik) = holoFn(f_ij) + holoFn(f_jk). From δ¹f = 0 the germs obey f_ik = f_jk + f_ij on the triple overlap; holoFn is additive (holoFn_add) and restriction-compatible (holoFn_restrict). The gateway to round-trip 2.

theorem holoFn_cocycle_add (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (i j k : 𝔇.toFiniteCover.ι) {y : X}
    (hy : y ∈ (𝔇.U i ⊓ 𝔇.U j ⊓ 𝔇.U k : Opens X)) :
    holoFn (cocycle_mem 𝔇 f i k) y
      = holoFn (cocycle_mem 𝔇 f i j) y + holoFn (cocycle_mem 𝔇 f j k) y

primFn

The global primitive summand ρ_k · holoFn(s_k) as a SmoothCFunctions (globally smooth: on U_k both factors are smooth, off tsupport ρ_k it vanishes). The ∂̄ of h = ∑_k primFn is the coboundary's image, since each holoFn(s_k) is holomorphic (holoFn_dbar_eq_zero).

noncomputable def primFn (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) {g : MGerm (𝔇.U k)}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) (𝔇.U k)) : SmoothCFunctions X

primFn_apply

@[simp] theorem primFn_apply (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) {g : MGerm (𝔇.U k)}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) (𝔇.U k)) (x : X) :
    primFn 𝔇 k hg x = rhoC 𝔇 k x * holoFn hg x

dbarL_primFn_apply

∂̄(ρ_k·holoFn(s_k)) = holoFn(s_k)·∂̄ρ_k (the Leibniz identity, with the holoFn term killed since holoFn(s_k) is holomorphic, holoFn_dbar_eq_zero). Pointwise, 2-case (on tsupport ρ_k ⊆ U_k the product rule; off it both sides vanish).

theorem dbarL_primFn_apply (𝔇 : ChartDiskCover X) (k : 𝔇.toFiniteCover.ι) {g : MGerm (𝔇.U k)}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) (𝔇.U k)) (x : X) :
    (dbarL (primFn 𝔇 k hg)) x = holoFn hg x • (dbarRho 𝔇 k x)

cechTerm_mem_zeroOne

Each double-sum term T_jk is a (0,1)-form: its fiber value c • (∂̄ρ_k x) lies in the range of proj01 because ∂̄ρ_k x does (dbarL_mem_zeroOne/idempotence) and proj01 commutes with the ℂ-scale (proj01_smul).

theorem cechTerm_mem_zeroOne (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (j k : 𝔇.toFiniteCover.ι) :
    cechTerm 𝔇 f j k ∈ OneFormsZeroOne X

cechTerm_add

The double-sum term is additive in the cocycle (holoFn_add washout on the overlap; off it both sides vanish).

theorem cechTerm_add (𝔇 : ChartDiskCover X)
    (f₁ f₂ : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (j k : 𝔇.toFiniteCover.ι) :
    cechTerm 𝔇 (f₁ + f₂) j k = cechTerm 𝔇 f₁ j k + cechTerm 𝔇 f₂ j k

cechTerm_smul

The double-sum term is ℝ-homogeneous in the cocycle (holoFn_smul washout; the ℝ-action on the ℂ-module is ↑r-scaling).

theorem cechTerm_smul (𝔇 : ChartDiskCover X) (r : ℝ)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) (j k : 𝔇.toFiniteCover.ι) :
    cechTerm 𝔇 (r • f) j k = r • cechTerm 𝔇 f j k

cechToDolbeaultForm

(Analytic sub-kernel — the Čech → Dolbeault glued-form operator.) The ℝ-linear map sending a holomorphic Čech 1-cocycle f = {f_ij} to the global (0,1)-form ω with ω = ∂̄η_i on U_i, η_i := ∑_k ρ_k·f_ik (partition-of-unity globalization). The genuine analytic content of the inverse: lift the germ-class cocycle to holomorphic reps, the PoU smooth globalization (SmoothPartitionOfUnity.IsSubordinate.contMDiff_finsum_smul), and glue the local ∂̄η_i (which agree on overlaps, cechCoboundary_telescoping) into a global section (gluedFun-for-forms). Plan:

noncomputable def cechToDolbeaultForm (𝔇 : ChartDiskCover X) :
    ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)) →ₗ[ℝ] ↥(OneFormsZeroOne X) where

cechToDolbeaultForm_val

cechToDolbeaultForm 𝔇 f is (the section underlying) the finite sum ∑_{(j,k)} T_jk. Isolates the single subtype-coercion-through-a-Finset.sum step (the only place the transparency-option isDefEq cost on cechTerm bodies appears), so downstream uses go through section_finsetSum_apply cheaply.

theorem cechToDolbeaultForm_val (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    ((cechToDolbeaultForm 𝔇 f : ↥(OneFormsZeroOne X)) : SmoothCOneForms X)
      = ∑ p : 𝔇.toFiniteCover.ι × 𝔇.toFiniteCover.ι, cechTerm 𝔇 f p.1 p.2

section_finsetSum_apply

Section-eval commutes with finite sums of (0,1)-forms (generic; applied by unification, so it never whnfs the heavy cechTerm body — avoiding the transparency-option isDefEq blowup).

theorem section_finsetSum_apply {ι : Type*} (s : ι → SmoothCOneForms X) (t : Finset ι) (x : X) :
    (∑ i ∈ t, s i) x = ∑ i ∈ t, (s i) x

telescope_sum

The double-sum telescoping ∑_{j,k} ρ_j·(H_k − H_j) • D_k = ∑_k H_k • D_k when ∑_j ρ_j = 1 and ∑_k D_k = 0 — pure module algebra over any ℂ-module M, extracted so it elaborates without the manifold-instance / transparency cost of the section setting.

theorem telescope_sum {ι : Type*} [Fintype ι] {M : Type*} [AddCommGroup M] [Module ℂ M]
    (R H : ι → ℂ) (D : ι → M) (hR : ∑ j, R j = 1) (hD : ∑ k, D k = 0) :
    (∑ p : ι × ι, (R p.1 * (H p.2 - H p.1)) • D p.2) = ∑ k, H k • D k

cechToDolbeaultForm_coboundary_le

(Analytic sub-kernel — well-definedness of Čech → Dolbeault.) A Čech coboundary cocycle maps to a ∂̄-image (its glued form ω is ∂̄ of the global primitive that the coboundary's holomorphic 0-cochain supplies), hence to 0 in H^{0,1} = A^{0,1}/im ∂̄. This is the kernel inclusion that makes the lift to cechH1 = Z¹/B¹ well-defined.

theorem cechToDolbeaultForm_coboundary_le (𝔇 : ChartDiskCover X) :
    ((𝔇.toFiniteCover.coboundaries1 (0 : Divisor X)).submoduleOf
        (𝔇.toFiniteCover.cocycles1 (0 : Divisor X))).restrictScalars ℝ
      ≤ LinearMap.ker ((Submodule.mkQ (dbarImageInZeroOne X)) ∘ₗ cechToDolbeaultForm 𝔇)

cech_to_dolbeault

Čech → Dolbeault. The ℝ-linear inverse H¹(X, 𝒪) → H^{0,1}(X). Assembled completely from the analytic glued-form operator cechToDolbeaultForm and its well-definedness cechToDolbeaultForm_coboundary_le via Submodule.liftQ through the Čech quotient Z¹/B¹ (scalar ℂ → ℝ). The overall minus sign is the boundary-map sign convention ((δc)(i,j) = c_j − c_i in cechDelta0): without it the round-trips would be −id. All genuine content lives in the two named sub-kernels above.

noncomputable def cech_to_dolbeault (𝔇 : ChartDiskCover X) :
    𝔇.toFiniteCover.cechH1 0 →ₗ[ℝ] DolbeaultH01 X

cech_to_dolbeault_mk

cech_to_dolbeault on a cocycle representative: −[ω] for ω = cechToDolbeaultForm f.

theorem cech_to_dolbeault_mk (𝔇 : ChartDiskCover X)
    (f : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    cech_to_dolbeault 𝔇 (Submodule.Quotient.mk f)
      = -(Submodule.Quotient.mk (cechToDolbeaultForm 𝔇 f))