A machine-checked solution to the Jacobians challenge

19.22. Finiteness.ChartDiskFinitenessComplete🔗

Jacobians.Finiteness.ChartDiskFinitenessComplete — source

overlapData_Wov_eq

𝔇.overlapData.Wov = 𝔇.Wov (rfl) — exposed as a simp lemma so the rhoRaw-introduced overlapData.Wov terms normalize to the 𝔇.Wov used by the geometric witnesses.

@[simp] theorem overlapData_Wov_eq : 𝔇.overlapData.Wov = 𝔇.Wov

overlapData_Uov_eq

𝔇.overlapData.Uov = 𝔇.Uov (rfl).

@[simp] theorem overlapData_Uov_eq : 𝔇.overlapData.Uov = 𝔇.Uov

analyticOn_coverTransition_Wov

The cover transition τ_{ab} is analytic on the OPEN shrinking overlap 𝔇.Wov (a,b) (chart-a image of V a ∩ V b): at each point it is analytic by transition_analyticAt_of_mem, both centres' chart sources containing the overlap point (V a, V b ⊆ closure ⊆ U ⊆ source).

theorem analyticOn_coverTransition_Wov (a b : 𝔇.ι) :
    AnalyticOn ℂ (𝔇.coverTransition a b) (𝔇.Wov (a, b))

mapsTo_coverTransition_Wov

The cover transition τ_{ab} maps the OPEN shrinking overlap 𝔇.Wov (a,b) (chart-a coordinates) into the b-side DIAGONAL shrinking 𝔇.Wov (b,b) (chart-b image of V b). A point φ_a x with x ∈ V a ∩ V b maps to φ_b x with x ∈ V b, so φ_b x ∈ φ_b '' (V b) = Wov (b,b). (Using the diagonal SHRINKING Wov (b,b) rather than the full Uov (b,b) makes the 0-cochain space C0Holo a SHRINKING space — bounded on a relatively-compact image — so the comparison descent of a germ coboundary to a δ⁰-image is provable; cf. the Montel model's full-image C0.)

theorem mapsTo_coverTransition_Wov (a b : 𝔇.ι) :
    Set.MapsTo (𝔇.coverTransition a b) (𝔇.Wov (a, b)) (𝔇.Wov (b, b))

Wov_subset_Wov_diag_fst

The shrinking overlap 𝔇.Wov (a,b) lies in the a-side DIAGONAL shrinking 𝔇.Wov (a,a) (chart-a image of V a ∩ V b ⊆ V a), so the diagonal a-component restricts directly.

theorem Wov_subset_Wov_diag_fst (a b : 𝔇.ι) :
    𝔇.Wov (a, b) ⊆ 𝔇.Wov (a, a)

C0Holo

Sup-norm 0-cochains, holomorphic side C0Holo — bounded-holomorphic on each DIAGONAL shrinking Wov (a,a) = chartAt (center a) '' (V a). The shrinking (relatively-compact) image makes a germ section's analytic representative bounded there (the descent of coboundaries needs this).

abbrev C0Holo (𝔇 : ChartDiskCover X) : Type _

delta0Model

The cross-chart Čech δ⁰ of the chart-disk model: c.Cshr-valued from C0Holo. Componentwise on overlap (a,b), (δ⁰f)_{ab} = (transport of f_b to chart-a) − (restriction of f_a) on the OPEN Wov (a,b), the genuine Čech coboundary with the b-side transported through the holomorphic transition τ_{ab}. Both pieces stay BddHol on the open Wov.

noncomputable def delta0Model :
    𝔇.C0Holo →L[ℂ] 𝔇.overlapData.Cshr

delta0Model_apply

theorem delta0Model_apply (f : 𝔇.C0Holo)
    (p : 𝔇.overlapData.J) :
    𝔇.delta0Model f p
      = BddHol.precompHolCLM (𝔇.analyticOn_coverTransition_Wov p.1 p.2)
          (𝔇.mapsTo_coverTransition_Wov p.1 p.2) (f p.2)
        - BddHol.restrictOpenCLM (𝔇.Wov_subset_Wov_diag_fst p.1 p.2) (f p.1)

delta0Model_apply_apply

theorem delta0Model_apply_apply (f : 𝔇.C0Holo)
    (p : 𝔇.overlapData.J) {z : ℂ} (hz : z ∈ 𝔇.Wov p) :
    (𝔇.delta0Model f p).toFun z
      = (f p.2).toFun (𝔇.coverTransition p.1 p.2 z) - (f p.1).toFun z

WovTriple

Open chart-a image of the triple shrinking overlap V a ∩ V b ∩ V c — the shrinking-side 2-cochain domain.

noncomputable def WovTriple (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) : Set ℂ

isOpen_WovTriple

theorem isOpen_WovTriple (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) : IsOpen (𝔇.WovTriple t)

C2Holo

Sup-norm 2-cochains, holomorphic shrinking side C2Holo — bounded-holomorphic on each open triple WovTriple t.

abbrev C2Holo (𝔇 : ChartDiskCover X) : Type _

analyticOn_coverTransition_WovTriple

theorem analyticOn_coverTransition_WovTriple (a b c : 𝔇.ι) :
    AnalyticOn ℂ (𝔇.coverTransition a b) (𝔇.WovTriple (a, b, c))

mapsTo_coverTransition_WovTriple_shrink

τ_{ab} maps the OPEN triple WovTriple (a,b,c) (chart-a coords) into the shrinking Wov (b,c) (chart-b image of V b ∩ V c). A point φ_a x with x ∈ V a ∩ V b ∩ V c maps to φ_b x with x ∈ V b ∩ V c.

theorem mapsTo_coverTransition_WovTriple_shrink (a b c : 𝔇.ι) :
    Set.MapsTo (𝔇.coverTransition a b) (𝔇.WovTriple (a, b, c)) (𝔇.Wov (b, c))

WovTriple_subset_Wov_fst_snd

theorem WovTriple_subset_Wov_fst_snd (a b c : 𝔇.ι) :
    𝔇.WovTriple (a, b, c) ⊆ 𝔇.Wov (a, b)

WovTriple_subset_Wov_fst_trd

theorem WovTriple_subset_Wov_fst_trd (a b c : 𝔇.ι) :
    𝔇.WovTriple (a, b, c) ⊆ 𝔇.Wov (a, c)

delta1Model

The cross-chart Čech δ¹ on the shrinking side c.Cshr →L[ℂ] C2Holo. Componentwise on the triple (a,b,c), (δ¹s)_{abc} = (s_{bc} ∘ τ_{ab}) − s_{ac} + s_{ab} on the OPEN WovTriple (a,b,c).

noncomputable def delta1Model :
    𝔇.overlapData.Cshr →L[ℂ] 𝔇.C2Holo

delta1Model_apply

theorem delta1Model_apply (s : 𝔇.overlapData.Cshr) (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) :
    𝔇.delta1Model s t
      = BddHol.precompHolCLM (𝔇.analyticOn_coverTransition_WovTriple t.1 t.2.1 t.2.2)
          (𝔇.mapsTo_coverTransition_WovTriple_shrink t.1 t.2.1 t.2.2) (s (t.2.1, t.2.2))
        - BddHol.restrictOpenCLM (𝔇.WovTriple_subset_Wov_fst_trd t.1 t.2.1 t.2.2) (s (t.1, t.2.2))
        + BddHol.restrictOpenCLM (𝔇.WovTriple_subset_Wov_fst_snd t.1 t.2.1 t.2.2)
            (s (t.1, t.2.1))

delta1Model_apply_apply

theorem delta1Model_apply_apply (s : 𝔇.overlapData.Cshr) (t : 𝔇.ι × 𝔇.ι × 𝔇.ι)
    {z : ℂ} (hz : z ∈ 𝔇.WovTriple t) :
    (𝔇.delta1Model s t).toFun z
      = (s (t.2.1, t.2.2)).toFun (𝔇.coverTransition t.1 t.2.1 z)
        - (s (t.1, t.2.2)).toFun z + (s (t.1, t.2.1)).toFun z

UovTriple

Open chart-a image of the triple cover overlap U a ∩ U b ∩ U c — the cover-side 2-cochain domain.

noncomputable def UovTriple (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) : Set ℂ

C2Cov

abbrev C2Cov (𝔇 : ChartDiskCover X) : Type _

analyticOn_coverTransition_UovTriple

theorem analyticOn_coverTransition_UovTriple (a b c : 𝔇.ι) :
    AnalyticOn ℂ (𝔇.coverTransition a b) (𝔇.UovTriple (a, b, c))

mapsTo_coverTransition_UovTriple

τ_{ab} maps the cover triple UovTriple (a,b,c) into the cover overlap Uov (b,c).

theorem mapsTo_coverTransition_UovTriple (a b c : 𝔇.ι) :
    Set.MapsTo (𝔇.coverTransition a b) (𝔇.UovTriple (a, b, c)) (𝔇.Uov (b, c))

UovTriple_subset_Uov_fst_snd

theorem UovTriple_subset_Uov_fst_snd (a b c : 𝔇.ι) :
    𝔇.UovTriple (a, b, c) ⊆ 𝔇.Uov (a, b)

UovTriple_subset_Uov_fst_trd

theorem UovTriple_subset_Uov_fst_trd (a b c : 𝔇.ι) :
    𝔇.UovTriple (a, b, c) ⊆ 𝔇.Uov (a, c)

delta1CovModel

The cross-chart Čech δ¹ on the COVER side c.Ccov →L[ℂ] C2Cov. Same shape as the shrinking δ¹, on the full cover overlaps.

noncomputable def delta1CovModel :
    𝔇.overlapData.Ccov →L[ℂ] 𝔇.C2Cov

delta1CovModel_apply

theorem delta1CovModel_apply (s : 𝔇.overlapData.Ccov) (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) :
    𝔇.delta1CovModel s t
      = BddHol.precompHolCLM (𝔇.analyticOn_coverTransition_UovTriple t.1 t.2.1 t.2.2)
          (𝔇.mapsTo_coverTransition_UovTriple t.1 t.2.1 t.2.2) (s (t.2.1, t.2.2))
        - BddHol.restrictOpenCLM (𝔇.UovTriple_subset_Uov_fst_trd t.1 t.2.1 t.2.2) (s (t.1, t.2.2))
        + BddHol.restrictOpenCLM (𝔇.UovTriple_subset_Uov_fst_snd t.1 t.2.1 t.2.2)
            (s (t.1, t.2.1))

delta1CovModel_apply_apply

theorem delta1CovModel_apply_apply (s : 𝔇.overlapData.Ccov) (t : 𝔇.ι × 𝔇.ι × 𝔇.ι)
    {z : ℂ} (hz : z ∈ 𝔇.UovTriple t) :
    (𝔇.delta1CovModel s t).toFun z
      = (s (t.2.1, t.2.2)).toFun (𝔇.coverTransition t.1 t.2.1 z)
        - (s (t.1, t.2.2)).toFun z + (s (t.1, t.2.1)).toFun z

coverTransition_cocycle_Wov

The chart-transition cocycle identity on the OPEN triple WovTriple: τ\_\{bc\}(τ\_\{ab\} z) = τ\_\{ac\} z for z ∈ WovTriple (a,b,c).

theorem coverTransition_cocycle_Wov (a b c : 𝔇.ι) {z : ℂ} (hz : z ∈ 𝔇.WovTriple (a, b, c)) :
    𝔇.coverTransition b c (𝔇.coverTransition a b z) = 𝔇.coverTransition a c z

delta1_comp_delta0

δ¹ ∘ δ⁰ = 0 (the shrinking-side Čech hδδ).

theorem delta1_comp_delta0 :
    (𝔇.delta1Model).comp 𝔇.delta0Model = 0

WovTriple_subset_UovTriple

theorem WovTriple_subset_UovTriple (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) :
    𝔇.WovTriple t ⊆ 𝔇.UovTriple t

rho2Model

The 2-cochain restriction ρ² : C2Cov →L C2Holo (cover → shrinking).

noncomputable def rho2Model : 𝔇.C2Cov →L[ℂ] 𝔇.C2Holo

rho2Model_apply

@[simp] theorem rho2Model_apply (g : 𝔇.C2Cov) (t : 𝔇.ι × 𝔇.ι × 𝔇.ι) :
    𝔇.rho2Model g t = BddHol.restrictOpenCLM (𝔇.WovTriple_subset_UovTriple t) (g t)

delta1_comp_rhoRaw_eq_rho2_comp_delta1Cov

The commuting square δ¹_shr ∘ ρ = ρ² ∘ δ¹_cov.

theorem delta1_comp_rhoRaw_eq_rho2_comp_delta1Cov :
    (𝔇.delta1Model).comp 𝔇.overlapData.rhoRaw
      = (𝔇.rho2Model).comp 𝔇.delta1CovModel

hcomm

theorem hcomm (x : 𝔇.overlapData.Ccov) (hx : 𝔇.delta1CovModel x = 0) :
    𝔇.delta1Model (𝔇.overlapData.rhoRaw x) = 0

shrinkOpens

The shrinking sets V a := shrinkSet a as Opens X.

noncomputable def shrinkOpens (a : 𝔇.ι) : Opens X

shrinkOpens_coe

@[simp] theorem shrinkOpens_coe (a : 𝔇.ι) : ((𝔇.shrinkOpens a : Opens X) : Set X) = 𝔇.shrinkSet a

shrinkCover

The shrinking cover (V a) — a FiniteCover (covers X by iUnion_shrinkSet_eq_univ).

noncomputable def shrinkCover : FiniteCover X where

shrinkCover_U

@[simp] theorem shrinkCover_U (a : 𝔇.ι) : 𝔇.shrinkCover.U a = 𝔇.shrinkOpens a

shrinkOpens_le_U

V a ⊆ U a (the shrinking sits in the cover set).

theorem shrinkOpens_le_U (a : 𝔇.ι) : 𝔇.shrinkOpens a ≤ 𝔇.U a

isRefinement_shrinkCover

The refinement shrinkCover ⪯ 𝔇 via the identity index map.

theorem isRefinement_shrinkCover :
    FiniteCover.IsRefinement 𝔇.shrinkCover 𝔇.toFiniteCover id

shrinkOpens_subset_source

V a ⊆ (chartAt (center a)).source.

theorem shrinkOpens_subset_source (a : 𝔇.ι) :
    ((𝔇.shrinkOpens a : Opens X) : Set X) ⊆ (chartAt (H := ℂ) (𝔇.center a)).source

Wov_eq_chartImage_shrinkInter

Wov (a,b) is exactly the chart-a image of the open shrinkOpens a ⊓ shrinkOpens b.

theorem Wov_eq_chartImage_shrinkInter (a b : 𝔇.ι) :
    𝔇.Wov (a, b)
      = (chartAt (H := ℂ) (𝔇.center a)) ''
        ((𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b : Opens X) : Set X)

shrinkInter_subset_source

V_a ∩ V_b ⊆ (chartAt (center a)).source.

theorem shrinkInter_subset_source (a b : 𝔇.ι) :
    ((𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b : Opens X) : Set X) ⊆
      (chartAt (H := ℂ) (𝔇.center a)).source

shrinkBddHolRetype

The BddHol component s_{ab}, retyped to live on the exact chart image of shrinkOpens a ⊓ shrinkOpens b (which is Wov (a,b)), ready for bddHolToOmegaDGerm\_zero\_image.

noncomputable def shrinkBddHolRetype (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) :
    BddHol ((chartAt (H := ℂ) (𝔇.center a)) ''
      ((𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b : Opens X) : Set X))

shrinkBddHolRetype_toFun_of_mem

theorem shrinkBddHolRetype_toFun_of_mem (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) {z : ℂ}
    (hz : z ∈ 𝔇.Wov (a, b)) :
    (𝔇.shrinkBddHolRetype s a b).toFun z = (s (a, b)).toFun z

shrinkGerm

The germ section σ_{ab} on V_a ⊓ V_b read back from s_{ab} through chart a.

noncomputable def shrinkGerm (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) :
    ↥(OmegaDGerm (0 : Divisor X) (𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b))

shrinkGerm_holoFn

The value of holoFn σ_{ab} at y ∈ V_a ∩ V_b is s_{ab}.toFun (φ_a y). (Mirror of diagPullbackGerm_holoFn.)

theorem shrinkGerm_holoFn (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) {y : X}
    (hy : y ∈ (𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b : Opens X)) :
    holoFn (𝔇.shrinkGerm s a b).2 y = (s (a, b)).toFun ((chartAt (H := ℂ) (𝔇.center a)) y)

chart_mem_WovTriple

chart_i y ∈ WovTriple (i,j,k) for y ∈ V_i ∩ V_j ∩ V_k.

theorem chart_mem_WovTriple (i j k : 𝔇.ι) {y : X}
    (hy : y ∈ (𝔇.shrinkOpens i ⊓ 𝔇.shrinkOpens j ⊓ 𝔇.shrinkOpens k : Opens X)) :
    (chartAt (H := ℂ) (𝔇.center i)) y ∈ 𝔇.WovTriple (i, j, k)

coverTransition_chart_shrink

For y ∈ V_i ∩ V_j ⊆ V_i ∩ V_j, the transition point identity (chart_j).symm (τ_{ij}(chart_i y)) = ... collapses: τ_{ij}(chart_i y) = chart_j y.

theorem coverTransition_chart_shrink (i j : 𝔇.ι) {y : X}
    (hyi : y ∈ (𝔇.shrinkOpens i : Opens X)) (hyj : y ∈ (𝔇.shrinkOpens j : Opens X)) :
    𝔇.coverTransition i j ((chartAt (H := ℂ) (𝔇.center i)) y) =
      (chartAt (H := ℂ) (𝔇.center j)) y

shrinkGerm_cocycle_add

The germ cocycle relation at the holoFn value level. For a Cshr cocycle s (i.e. δ¹s = 0) and y ∈ V_i ∩ V_j ∩ V_k, holoFn σ_{ik} y = holoFn σ_{ij} y + holoFn σ_{jk} y. Direct from delta1Model s = 0 evaluated at chart_i y ∈ WovTriple (i,j,k), via shrinkGerm_holoFn and the transition identity.

theorem shrinkGerm_cocycle_add (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0)
    (i j k : 𝔇.ι) {y : X}
    (hy : y ∈ (𝔇.shrinkOpens i ⊓ 𝔇.shrinkOpens j ⊓ 𝔇.shrinkOpens k : Opens X)) :
    holoFn (𝔇.shrinkGerm s i k).2 y
      = holoFn (𝔇.shrinkGerm s i j).2 y + holoFn (𝔇.shrinkGerm s j k).2 y

shrinkGerm_diag_eq_zero

holoFn σ_{ii} y = 0 on V_i (diagonal vanishing). From the cocycle relation with j = k = i: holoFn σ_{ii} = holoFn σ_{ii} + holoFn σ_{ii}.

theorem shrinkGerm_diag_eq_zero (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0)
    (i : 𝔇.ι) {y : X} (hy : y ∈ (𝔇.shrinkOpens i : Opens X)) :
    holoFn (𝔇.shrinkGerm s i i).2 y = 0

shrinkRhoC

ρ_a as a complex SmoothCFunctions (ρ̃_a = ofReal ∘ shrinkPoU a).

noncomputable def shrinkRhoC (a : 𝔇.ι) : SmoothCFunctions X

shrinkDbarRho

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

noncomputable def shrinkDbarRho (a : 𝔇.ι) : SmoothCOneForms X

shrinkRhoC_eq_zero_of_notMem

theorem shrinkRhoC_eq_zero_of_notMem (a : 𝔇.ι) {x : X}
    (hx : x ∉ tsupport (𝔇.shrinkPoU a)) : 𝔇.shrinkRhoC a x = 0

shrinkDbarRho_eq_zero_of_notMem

theorem shrinkDbarRho_eq_zero_of_notMem (a : 𝔇.ι) {x : X}
    (hx : x ∉ tsupport (𝔇.shrinkPoU a)) : (𝔇.shrinkDbarRho a) x = 0

sum_shrinkRhoC

theorem sum_shrinkRhoC (𝔇 : ChartDiskCover X) : ∑ a, 𝔇.shrinkRhoC a = 1

sum_shrinkRhoC_apply

theorem sum_shrinkRhoC_apply (𝔇 : ChartDiskCover X) (x : X) : ∑ a, (𝔇.shrinkRhoC a x) = 1

sum_shrinkDbarRho

theorem sum_shrinkDbarRho (𝔇 : ChartDiskCover X) : ∑ a, 𝔇.shrinkDbarRho a = 0

sum_shrinkDbarRho_apply

theorem sum_shrinkDbarRho_apply (𝔇 : ChartDiskCover X) (x : X) :
    ∑ a, ((𝔇.shrinkDbarRho a) x) = 0

shrinkTerm

The Bott–Tu double-sum term (ρ_a · holoFn σ_{ac}) • ∂̄ρ_c as a global smooth (0,1)-form. Globally smooth by the 3-case tsupport argument: on V_a ∩ V_c (where holoFn σ_{ac} is smooth) everything is smooth; off tsupport ρ_a the factor ρ_a vanishes; off tsupport ρ_c the factor ∂̄ρ_c vanishes.

noncomputable def shrinkTerm (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) : SmoothCOneForms X where

shrinkTerm_apply

@[simp] theorem shrinkTerm_apply (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) (x : X) :
    (𝔇.shrinkTerm s a c) x
      = (𝔇.shrinkRhoC a x * holoFn (𝔇.shrinkGerm s a c).2 x) • (𝔇.shrinkDbarRho c x)

shrinkTerm_mem_zeroOne

Each Bott–Tu term is a (0,1)-form (∂̄ρ_c is, and ℂ-scaling preserves (0,1)).

theorem shrinkTerm_mem_zeroOne (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) :
    𝔇.shrinkTerm s a c ∈ OneFormsZeroOne X

glueForm

The global Bott–Tu form ω̂ as a (0,1)-form: ∑_{a,c} (ρ_a · holoFn σ_{ac}) • ∂̄ρ_c.

noncomputable def glueForm (s : 𝔇.overlapData.Cshr) : ↥(OneFormsZeroOne X)

glueForm_val

The underlying form of glueForm is the finite sum of shrinkTerms.

theorem glueForm_val (s : 𝔇.overlapData.Cshr) :
    ((𝔇.glueForm s : ↥(OneFormsZeroOne X)) : SmoothCOneForms X)
      = ∑ p : 𝔇.ι × 𝔇.ι, 𝔇.shrinkTerm s p.1 p.2

globalPrim

The chart-a smooth split G_a := ∑_c ρ_c · holoFn σ_{ac} (a function on V_a).

noncomputable def globalPrim (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) : X → ℂ

globalPrim_apply

theorem globalPrim_apply (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) (x : X) :
    𝔇.globalPrim s a x = ∑ c, 𝔇.shrinkRhoC c x * holoFn (𝔇.shrinkGerm s a c).2 x

globalPrim_diff

The difference identity G_a(x) − G_b(x) = holoFn σ_{ab}(x) on V_a ∩ V_b. Pointwise via the cocycle relation holoFn σ_{ac} = holoFn σ_{ab} + holoFn σ_{bc} and ∑ ρ = 1. (Mirror of chartDiskCoverPrim_diff.)

theorem globalPrim_diff (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a b : 𝔇.ι) {x : X}
    (hx : x ∈ (𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b : Opens X)) :
    𝔇.globalPrim s a x - 𝔇.globalPrim s b x = holoFn (𝔇.shrinkGerm s a b).2 x

globalPrimTerm

A single summand ρ_c · holoFn σ_{ac} of G_a, as a bare function X → ℂ.

noncomputable def globalPrimTerm (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) : X → ℂ

mdifferentiableAt_globalPrimTerm

Each summand of G_a is MDifferentiableAt at any point of V_a (in tsupport ρ_c both factors are smooth — using x ∈ V_a ∩ V_c; off tsupport ρ_c the term is locally 0).

theorem mdifferentiableAt_globalPrimTerm (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.shrinkOpens a : Opens X)) :
    MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.globalPrimTerm s a c) x

dbar_globalPrimTerm

The Wirtinger value of one summand proj01(mfderiv (ρ_c·holoFn σ_{ac}) x) = holoFn σ_{ac}(x) • ∂̄ρ_c x at x ∈ V_a (product rule + holoFn holomorphic; off tsupport ρ_c both sides vanish).

theorem dbar_globalPrimTerm (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.shrinkOpens a : Opens X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.globalPrimTerm s a c) x)
      = holoFn (𝔇.shrinkGerm s a c).2 x • (𝔇.shrinkDbarRho c x)

shrinkGerm_antisymm

Antisymmetry of holoFn σ (from diagonal vanishing + cocycle): holoFn σ_{pa} = −holoFn σ_{ap} on V_a ∩ V_p.

theorem shrinkGerm_antisymm (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a p : 𝔇.ι) {y : X}
    (hya : y ∈ (𝔇.shrinkOpens a : Opens X)) (hyp : y ∈ (𝔇.shrinkOpens p : Opens X)) :
    holoFn (𝔇.shrinkGerm s p a).2 y = -holoFn (𝔇.shrinkGerm s a p).2 y

glueForm_apply_on_V

glueForm value telescopes on V_a: ω̂ x = ∑_c holoFn σ_{ac}(x) • ∂̄ρ_c(x) for x ∈ V_a. Via the cocycle substitution holoFn σ_{pq} = holoFn σ_{aq} − holoFn σ_{ap} (on V_a) and telescope_sum (∑ ρ = 1, ∑ ∂̄ρ = 0).

theorem glueForm_apply_on_V (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.shrinkOpens a : Opens X)) :
    ((𝔇.glueForm s : ↥(OneFormsZeroOne X)) : SmoothCOneForms X) x
      = ∑ c, holoFn (𝔇.shrinkGerm s a c).2 x • (𝔇.shrinkDbarRho c x)

globalPrim_eq_sum

G_a = ∑_c (ρ_c · holoFn σ_{ac}) as a sum of functions.

theorem globalPrim_eq_sum (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) :
    𝔇.globalPrim s a = ∑ c, 𝔇.globalPrimTerm s a c

dbar_globalPrim

The intrinsic ∂̄ identity proj01(mfderiv G_a x) = ω̂ x for x ∈ V_a. The per-term Wirtinger values (dbar_globalPrimTerm) summed (HasMFDerivAt.sum), matched to glueForm by its V_a telescoping.

theorem dbar_globalPrim (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.shrinkOpens a : Opens X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.globalPrim s a) x)
      = ((𝔇.glueForm s : ↥(OneFormsZeroOne X)) : SmoothCOneForms X) x

primVal

The per-disk ∂̄-primitive value u_a := diskVal a ω̂ (a smooth function on U_a).

noncomputable def primVal (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) : X → ℂ

dbar_primVal

proj01(mfderiv u_a x) = ω̂ x on U_a (Forster 13.2 primitive; dbar_diskValue_eq_g upgraded to the full CLM by dbar_eq_of_apply_one').

theorem dbar_primVal (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) {x : X} (hxa : x ∈ (𝔇.U a : Set X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.primVal s a) x)
      = ((𝔇.glueForm s : ↥(OneFormsZeroOne X)) : SmoothCOneForms X) x

mdifferentiableAt_primVal

theorem mdifferentiableAt_primVal (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.U a : Set X)) :
    MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.primVal s a) x

dbar_chartFixed_of_intrinsic_zero

Chart-a Wirtinger bridge from intrinsic vanishing. If w is MDifferentiableAt y with intrinsic Wirtinger scalar proj01(mfderiv w y)(1) = 0, then for any chart a whose source contains y, the chart-a planar ∂̄(w ∘ φ_a⁻¹)(φ_a y) = 0. Proof: w∘φ_a⁻¹ = (w∘φ_y⁻¹)∘(φ_y∘φ_a⁻¹), the inner map is holomorphic, so by the Wirtinger chain rule the chart-a ∂̄ is conj(τ′) times the own-chart ∂̄(w∘φ_y⁻¹)(φ_y y) = proj01(mfderiv w y)(1) = 0.

theorem dbar_chartFixed_of_intrinsic_zero {w : X → ℂ} {y : X} (a : 𝔇.ι)
    (hya : y ∈ (chartAt (H := ℂ) (𝔇.center a)).source)
    (hwmd : MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w y)
    (hw0 : proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w y) (1 : ℂ) = 0) :
    DbarDisk.dbar (fun z => w ((chartAt (H := ℂ) (𝔇.center a)).symm z))
      ((chartAt (H := ℂ) (𝔇.center a)) y) = 0

etaFn

The corrector function η_a := u_a − G_a (a bare X → ℂ, holomorphic on V_a).

noncomputable def etaFn (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) : X → ℂ

mdifferentiableAt_etaFn

η_a is MDifferentiableAt at x ∈ V_a (difference of two MDifferentiableAt functions).

theorem mdifferentiableAt_etaFn (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.shrinkOpens a : Opens X)) :
    MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.etaFn s a) x

dbar1_etaFn

The intrinsic Wirtinger scalar of η_a vanishes on V_a: proj01(mfderiv η_a y)(1) = 0 (both u_a and G_a have it = (ω̂ y)(1)).

theorem dbar1_etaFn (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a : 𝔇.ι) {y : X}
    (hya : y ∈ (𝔇.shrinkOpens a : Opens X)) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (𝔇.etaFn s a) y) (1 : ℂ) = 0

etaFn_chartA_analyticOn

η_a chart-a-read is AnalyticOn Wov (a,a). At each z = φ_a y (y ∈ V_a) the chart-a planar ∂̄(η_a ∘ φ_a⁻¹) = 0 (dbar_chartFixed_of_intrinsic_zero + dbar1_etaFn), and the pullback is ℝ-differentiable on the open W = φ_a.target ∩ φ_a.symm⁻¹'(V_a); an open DifferentiableOn ℂ ⟹ AnalyticOn.

theorem etaFn_chartA_analyticOn (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a : 𝔇.ι) :
    AnalyticOn ℂ (𝔇.etaFn s a ∘ (chartAt (H := ℂ) (𝔇.center a)).symm) (𝔇.Wov (a, a))

norm_shrinkGerm_holoFn_le

‖holoFn σ_{ac} x‖ ≤ ‖s_{ac}‖ on V_a ∩ V_c (the germ-section value is s.toFun∘φ_a, bounded by the BddHol norm).

theorem norm_shrinkGerm_holoFn_le (s : 𝔇.overlapData.Cshr) (a c : 𝔇.ι) {x : X}
    (hx : x ∈ (𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens c : Opens X)) :
    ‖holoFn (𝔇.shrinkGerm s a c).2 x‖ ≤ ‖s (a, c)‖

norm_globalPrim_le

G_a is bounded by ∑_c ‖s_{ac}‖ on V_a.

theorem norm_globalPrim_le (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) {x : X}
    (hxa : x ∈ (𝔇.shrinkOpens a : Opens X)) :
    ‖𝔇.globalPrim s a x‖ ≤ ∑ c, ‖s (a, c)‖

etaFn_chartA_bounded

η_a chart-a-read is bounded on Wov (a,a): ‖planarPrimitive a ω̂ z‖ is bounded on the compact closure (Wov (a,a)) (planarPrimitive is globally continuous), and ‖G_a‖ ≤ ∑‖s_{a·}‖.

theorem etaFn_chartA_bounded (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) :
    ∃ C, ∀ z ∈ 𝔇.Wov (a, a),
      ‖(𝔇.etaFn s a ∘ (chartAt (H := ℂ) (𝔇.center a)).symm) z‖ ≤ C

etaBddHol

The holomorphic corrector η_a ∈ BddHol (Wov (a,a)) (C0Holo's a-component).

noncomputable def etaBddHol (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a : 𝔇.ι) :
    BddHol (𝔇.Wov (a, a))

etaBddHol_toFun_of_mem

theorem etaBddHol_toFun_of_mem (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) (a : 𝔇.ι)
    {z : ℂ} (hz : z ∈ 𝔇.Wov (a, a)) :
    (𝔇.etaBddHol s hs a).toFun z = 𝔇.etaFn s a ((chartAt (H := ℂ) (𝔇.center a)).symm z)

etaCochain

η : C0Holo — the holomorphic 0-cochain.

noncomputable def etaCochain (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) : 𝔇.C0Holo

coverCocycleGerm

The germ cover cocycle x' := dolbeaultToCechCocycle 𝔇 ω̂ (an element of cocycles1).

noncomputable def coverCocycleGerm (s : 𝔇.overlapData.Cshr) :
    ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))

coverCocycleGerm_component

The (a,b)-component germ is cechDelta0 (rawCochain ω̂) — its representative on U_a ⊓ U_b is diskSection b ω̂ − diskSection a ω̂.

theorem coverCocycleGerm_component (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) :
    ((𝔇.coverCocycleGerm s : 𝔇.toFiniteCover.Cochain1)) (a, b)
      = toGerm (𝔇.U a ⊓ 𝔇.U b)
          (𝔇.diskSection b (𝔇.glueForm s) ∘ openIncl inf_le_right
            - 𝔇.diskSection a (𝔇.glueForm s) ∘ openIncl inf_le_left)

coverCocycleGerm_holoFn

holoFn(x'_{ab}) y = u_b y − u_a y on U_a ∩ U_b (u := diskVal ω̂). The germ's representative diskSection b − diskSection a extends continuously to diskVal b − diskVal a.

theorem coverCocycleGerm_holoFn (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) {y : X}
    (hy : y ∈ (𝔇.U a ⊓ 𝔇.U b : Opens X)) :
    holoFn (cocycle_mem 𝔇 (𝔇.coverCocycleGerm s) a b) y
      = diskVal 𝔇 b (𝔇.glueForm s) y - diskVal 𝔇 a (𝔇.glueForm s) y

chartSymm_mem_Uov

φ_a.symm z ∈ U_a ∩ U_b for z ∈ Uov (a,b).

theorem chartSymm_mem_Uov (a b : 𝔇.ι) {z : ℂ} (hz : z ∈ 𝔇.Uov (a, b)) :
    (chartAt (H := ℂ) (𝔇.center a)).symm z ∈ ((𝔇.U a ⊓ 𝔇.U b : Opens X) : Set X)

exists_bound_diskVal

‖diskVal a ω̂ x‖ is bounded (uniformly in x) by the sup of planarPrimitive a ω̂ on the compact closedBall (e a) (radius a) (diskVal a ω̂ x = planarPrimitive a ω̂ (φ_a x)).

theorem exists_bound_diskVal (s : 𝔇.overlapData.Cshr) (a : 𝔇.ι) :
    ∃ C, ∀ x : X, x ∈ (𝔇.U a : Set X) → ‖diskVal 𝔇 a (𝔇.glueForm s) x‖ ≤ C

coverCocycle_analyticOn

The cover-cochain analyticity input: holoFn(x'_{ab}) ∘ φ_a⁻¹ is AnalyticOn (Uov (a,b)).

theorem coverCocycle_analyticOn (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) :
    AnalyticOn ℂ (holoFn (cocycle_mem 𝔇 (𝔇.coverCocycleGerm s) a b)
      ∘ (chartAt (H := ℂ) (𝔇.center a)).symm) (𝔇.Uov (a, b))

coverBddHol

The cover cochain component x_{ab} ∈ BddHol (Uov (a,b)) (analytic + bounded by 2·max diskVal).

noncomputable def coverBddHol (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) : BddHol (𝔇.Uov (a, b))

coverBddHol_toFun_of_mem

theorem coverBddHol_toFun_of_mem (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) {z : ℂ}
    (hz : z ∈ 𝔇.Uov (a, b)) :
    (𝔇.coverBddHol s a b).toFun z
      = holoFn (cocycle_mem 𝔇 (𝔇.coverCocycleGerm s) a b)
        ((chartAt (H := ℂ) (𝔇.center a)).symm z)

coverCochain

x : Ccov — the holomorphic cover cocycle (the NEGATED per-disk cocycle: the boundary-map sign convention (δ⁰c)(a,b) = c_b − c_a makes the lift s = δ⁰η + ρx come out with x = −x').

noncomputable def coverCochain (s : 𝔇.overlapData.Cshr) : 𝔇.overlapData.Ccov

coverCochain_toFun_of_mem

theorem coverCochain_toFun_of_mem (s : 𝔇.overlapData.Cshr) (a b : 𝔇.ι) {z : ℂ}
    (hz : z ∈ 𝔇.Uov (a, b)) :
    (𝔇.coverCochain s (a, b)).toFun z
      = -holoFn (cocycle_mem 𝔇 (𝔇.coverCocycleGerm s) a b)
        ((chartAt (H := ℂ) (𝔇.center a)).symm z)

coverCochain_mem_Z1cov

δ¹cov x = 0 — the cover cochain x is a cocycle. Pointwise on UovTriple, the three holoFn(x'_{··}) values obey the cocycle relation holoFn_cocycle_add (x' ∈ cocycles1).

theorem coverCochain_mem_Z1cov (s : 𝔇.overlapData.Cshr) :
    𝔇.delta1CovModel (𝔇.coverCochain s) = 0

leray_identity

The lift identity s = δ⁰ η + ρ x on each Wov (a,b). Pointwise at z = φ_a x (x ∈ V_a ∩ V_b): (δ⁰η + ρx)_{ab}(z) = (η_b(x) − η_a(x)) + (−(u_b(x) − u_a(x))) = ((u_b − G_b) − (u_a − G_a)) − (u_b − u_a) = G_a(x) − G_b(x) = holoFn σ_{ab}(x) = s_{ab}(z).

theorem leray_identity (s : 𝔇.overlapData.Cshr) (hs : 𝔇.delta1Model s = 0) :
    s = 𝔇.delta0Model (𝔇.etaCochain s hs) + 𝔇.overlapData.rhoRaw (𝔇.coverCochain s)

holomorphicCoboundaries

The structural δ-complex on 𝔇.overlapData, with the leray field. δ0/δ1/δ1cov/hδδ/hcomm are the model differentials of §A; leray (Forster 14.6) is discharged by the global Bott–Tu form route of §A2-*:

Given a shrinking cocycle s : Cshr (δ¹s = 0):

  • σ := shrinkGerm s reads each s_{ab} back to an 𝒪_0 germ on V_a ⊓ V_b, a germ cocycle.

  • ω̂ := glueForm s = ∑_{a,c} (ρ_a · holoFn σ_{ac}) • ∂̄ρ_c (shrinking PoU shrinkPoU) is a GLOBAL smooth (0,1)-form, built directly (NO cross-chart ∂̄g_a gluing).

  • x := coverCochain s is the per-disk ∂̄-solve cocycle dolbeaultToCechCocycle ω̂ (the no-cutoff ball solve), holomorphic on the FULL overlaps Uov; δ¹cov x = 0 (coverCochain_mem_Z1cov).

  • η := etaCochain s has η_a = diskVal a ω̂ − G_a (G_a := ∑_c ρ_c · holoFn σ_{ac}, the local split), holomorphic on V_a since both diskVal a ω̂ and G_a have intrinsic ∂̄ = ω̂ there (dbar_globalPrim/dbar_diskValue_eq_g).

  • s = δ⁰η + ρx (leray_identity): the diskVal terms cancel, leaving G_a − G_b = holoFn σ_{ab} (globalPrim_diff, cocycle telescoping ∑ρ = 1).

This is the ball geometry's genuine unblock over the Montel cover: the global form has a smooth full-ball chart read, so the per-disk solve produces a cover cocycle on the FULL overlap.

noncomputable def holomorphicCoboundaries : HolomorphicCoboundaries 𝔇.overlapData where

overlap_subset_source

The per-overlap holomorphy domain for the forward map: the ball overlap U a ⊓ U b, read in chart center a. U a ⊓ U b ⊆ (chartAt (center a)).source.

theorem overlap_subset_source (a b : 𝔇.ι) :
    ((𝔇.U a ⊓ 𝔇.U b : Opens X) : Set X) ⊆ (chartAt (H := ℂ) (𝔇.center a)).source

closure_Wov_subset_chartImage_overlap

closure (Wov (a,b)) ⊆ chartAt (center a) '' (U a ⊓ U b) — the relatively-compact nesting that makes the analytic representative bounded on Wov. This is closure_Wov_subset_Uov read against the defining Uov = chartAt '' (U a ⊓ U b).

theorem closure_Wov_subset_chartImage_overlap (a b : 𝔇.ι) :
    closure (𝔇.Wov (a, b)) ⊆
      (chartAt (H := ℂ) (𝔇.center a)) '' ((𝔇.U a ⊓ 𝔇.U b : Opens X) : Set X)

overlapAtom

The per-overlap atom (inline germSectionToBddHol on the shrinking Wov). A germ section g ∈ OmegaDGerm 0 (U a ⊓ U b), read through chart center a and restricted to Wov (a,b), is a BddHol (Wov (a,b)). Value: holoFn hg ∘ (chartAt (center a)).symm.

noncomputable def overlapAtom (a b : 𝔇.ι) {g : MGerm (𝔇.U a ⊓ 𝔇.U b)}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a ⊓ 𝔇.U b)) :
    BddHol (𝔇.Wov (a, b))

overlapAtom_toFun_of_mem

@[simp] theorem overlapAtom_toFun_of_mem (a b : 𝔇.ι) {g : MGerm (𝔇.U a ⊓ 𝔇.U b)}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a ⊓ 𝔇.U b)) {z : ℂ} (hz : z ∈ 𝔇.Wov (a, b)) :
    (𝔇.overlapAtom a b hg).toFun z = holoFn hg ((chartAt (H := ℂ) (𝔇.center a)).symm z)

chartSymm_mem_overlap

For z ∈ Wov (a,b), the chart-a preimage (chartAt (center a)).symm z lies in the overlap U a ⊓ U b — so holoFn (germ-invariant, additive, …) applies there.

theorem chartSymm_mem_overlap (a b : 𝔇.ι) {z : ℂ} (hz : z ∈ 𝔇.Wov (a, b)) :
    (chartAt (H := ℂ) (𝔇.center a)).symm z ∈ ((𝔇.U a ⊓ 𝔇.U b : Opens X) : Set X)

overlapAtom_add

theorem overlapAtom_add (a b : 𝔇.ι) {g₁ g₂ : MGerm (𝔇.U a ⊓ 𝔇.U b)}
    (hg₁ : g₁ ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a ⊓ 𝔇.U b))
    (hg₂ : g₂ ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a ⊓ 𝔇.U b)) :
    𝔇.overlapAtom a b (Submodule.add_mem _ hg₁ hg₂)
      = 𝔇.overlapAtom a b hg₁ + 𝔇.overlapAtom a b hg₂

overlapAtom_smul

theorem overlapAtom_smul (a b : 𝔇.ι) (c : ℂ) {g : MGerm (𝔇.U a ⊓ 𝔇.U b)}
    (hg : g ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a ⊓ 𝔇.U b)) :
    𝔇.overlapAtom a b (Submodule.smul_mem _ c hg) = c • 𝔇.overlapAtom a b hg

cechToCshr

The forward germ→BddHol cochain map ↥(cocycles1 0) →ₗ[ℂ] Cshr. Componentwise the per-overlap atom: a Čech germ cocycle g's (a,b)-component (an OmegaDGerm 0 (U a ⊓ U b) section, cocycle_mem) becomes a BddHol (Wov (a,b)) via its analytic representative restricted to the relatively-compact Wov (a,b). ℂ-linear (each component is, overlapAtomCLM).

noncomputable def cechToCshr :
    ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)) →ₗ[ℂ] 𝔇.overlapData.Cshr where

cechToCshr_apply_toFun

theorem cechToCshr_apply_toFun (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)))
    (p : 𝔇.overlapData.J) {z : ℂ} (hz : z ∈ 𝔇.Wov p) :
    (𝔇.cechToCshr g p).toFun z
      = holoFn (cocycle_mem 𝔇 g p.1 p.2) ((chartAt (H := ℂ) (𝔇.center p.1)).symm z)

chartSymm_coverTransition_eq

The transition point identity for a triple-overlap chart point: for x ∈ U a ⊓ U b ⊓ U c, (chart_b).symm (τ_{ab} (chart_a x)) = x. (τ_{ab} (chart_a x) = chart_b x by coverTransition_apply, then (chart_b).symm (chart_b x) = x.)

theorem chartSymm_coverTransition_eq (a b c : 𝔇.ι) {x : X}
    (hx : x ∈ (𝔇.U a ⊓ 𝔇.U b ⊓ 𝔇.U c : Opens X)) :
    (chartAt (H := ℂ) (𝔇.center b)).symm
        (𝔇.coverTransition a b ((chartAt (H := ℂ) (𝔇.center a)) x)) = x

cechToCshr_mem_Z1shr

The forward map lands in Z1shr (δ¹ vanishes). Pointwise on WovTriple t, the three terms reduce — via the transition point identity and the cocycle relation at the holoFn level (holoFn_cocycle_add) — to 0.

theorem cechToCshr_mem_Z1shr (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    𝔇.cechToCshr g ∈ (𝔇.holomorphicCoboundaries).Z1shr

cechToZ1shr

The forward map corestricted to Z1shr ↥(cocycles1 0) →ₗ[ℂ] Z1shr.

noncomputable def cechToZ1shr :
    ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)) →ₗ[ℂ] (𝔇.holomorphicCoboundaries).Z1shr

cechToZ1shr_coe

@[simp] theorem cechToZ1shr_coe (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    ((𝔇.cechToZ1shr g : (𝔇.holomorphicCoboundaries).Z1shr) : 𝔇.overlapData.Cshr)
      = 𝔇.cechToCshr g

U_subset_source

U a ⊆ (chartAt (center a)).source.

theorem U_subset_source (a : 𝔇.ι) :
    ((𝔇.U a : Opens X) : Set X) ⊆ (chartAt (H := ℂ) (𝔇.center a)).source

closure_Wov_diag_subset_chartImage_U

closure (Wov (a,a)) ⊆ chartAt (center a) '' (U a) — the diagonal relatively-compact nesting.

theorem closure_Wov_diag_subset_chartImage_U (a : 𝔇.ι) :
    closure (𝔇.Wov (a, a)) ⊆ (chartAt (H := ℂ) (𝔇.center a)) '' ((𝔇.U a : Opens X) : Set X)

diagAtom

The diagonal atom. A germ section η ∈ OmegaDGerm 0 (U a), read through chart center a and restricted to the diagonal shrinking Wov (a,a), is a BddHol (Wov (a,a)). Value: holoFn hη ∘ (chartAt (center a)).symm.

noncomputable def diagAtom (a : 𝔇.ι) {η : MGerm (𝔇.U a)}
    (hη : η ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a)) :
    BddHol (𝔇.Wov (a, a))

diagAtom_toFun_of_mem

@[simp] theorem diagAtom_toFun_of_mem (a : 𝔇.ι) {η : MGerm (𝔇.U a)}
    (hη : η ∈ OmegaDGerm (0 : Divisor X) (𝔇.U a)) {z : ℂ} (hz : z ∈ 𝔇.Wov (a, a)) :
    (𝔇.diagAtom a hη).toFun z = holoFn hη ((chartAt (H := ℂ) (𝔇.center a)).symm z)

chartSymm_coverTransition_eq_chartSymm

The b-side transition point (chart_b).symm (τ_{ab} z) equals the a-side preimage (chart_a).symm z for z ∈ Wov (a,b) (both = x).

theorem chartSymm_coverTransition_eq_chartSymm (a b : 𝔇.ι) {z : ℂ} (hz : z ∈ 𝔇.Wov (a, b)) :
    (chartAt (H := ℂ) (𝔇.center b)).symm (𝔇.coverTransition a b z)
      = (chartAt (H := ℂ) (𝔇.center a)).symm z

cechToCshr_coboundary_eq_delta0

The forward map sends a germ coboundary to δ⁰ of a diagonal C0Holo cochain. If g is the germ coboundary cechDelta0 η₀ of a germ 0-cochain η₀ ∈ sections0 0, then cechToCshr g = δ0 (fun a => diagAtom a (η₀ a)) — so cechToCshr g ∈ range δ.

Pointwise on Wov (a,b): (cechToCshr g)_{ab}(z) = holoFn(g_{ab}) x = holoFn(η₀ b) x − holoFn(η₀ a) x (holoFn_restrict + holoFn_sub, x = (chart_a).symm z), and (δ0 f)\_\{ab\}(z) = f\_b(τ z) − f\_a(z) = holoFn(η₀ b)((chart\_b).symm (τ z)) − holoFn(η₀ a) x = holoFn(η₀ b) x − holoFn(η₀ a) x (the transition point identity).

theorem cechToCshr_coboundary_eq_delta0 (η₀ : 𝔇.toFiniteCover.Cochain0)
    (hη₀ : η₀ ∈ 𝔇.toFiniteCover.sections0 (0 : Divisor X))
    (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)))
    (hgeq : (g : 𝔇.toFiniteCover.Cochain1) = 𝔇.toFiniteCover.cechDelta0 η₀) :
    𝔇.cechToCshr g
      = (𝔇.holomorphicCoboundaries).δ0 (fun a => 𝔇.diagAtom a (hη₀ a))

cechToSupH1

The composite ↥(cocycles1 0) → Z1shr → supH1 (the forward map followed by the supH1 quotient).

noncomputable def cechToSupH1 :
    ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)) →ₗ[ℂ] (𝔇.holomorphicCoboundaries).supH1

cechToSupH1_apply

theorem cechToSupH1_apply (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    𝔇.cechToSupH1 g = Submodule.Quotient.mk (𝔇.cechToZ1shr g)

coboundaries_le_ker_cechToSupH1

The forward map kills germ coboundaries (well-definedness of the descent): the submodule of cocycles that are germ coboundaries is contained in ker cechToSupH1. An element is a germ coboundary cechDelta0 η₀, so its forward image is δ0 (diagAtom ...) ∈ range δ (cechToCshr_coboundary_eq_delta0), hence 0 in supH1.

theorem coboundaries_le_ker_cechToSupH1 :
    (𝔇.toFiniteCover.coboundaries1 (0 : Divisor X)).submoduleOf
        (𝔇.toFiniteCover.cocycles1 (0 : Divisor X)) ≤ LinearMap.ker 𝔇.cechToSupH1

comparisonMap

The descended comparison map cechH1 𝔇 0 →ₗ[ℂ] supH1 (the forward germ→BddHol cochain map, descended to the cohomology quotients via coboundaries_le_ker_cechToSupH1).

noncomputable def comparisonMap :
    𝔇.toFiniteCover.cechH1 (0 : Divisor X) →ₗ[ℂ] (𝔇.holomorphicCoboundaries).supH1

comparisonMap_mk

theorem comparisonMap_mk (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X))) :
    𝔇.comparisonMap (Submodule.Quotient.mk g) = 𝔇.cechToSupH1 g

Wov_diag_eq_chartImage_shrinkOpens

Wov (a,a) = chartAt (center a) '' (V a) (the diagonal shrinking IS the chart-image of V a).

theorem Wov_diag_eq_chartImage_shrinkOpens (a : 𝔇.ι) :
    𝔇.Wov (a, a) = (chartAt (H := ℂ) (𝔇.center a)) '' ((𝔇.shrinkOpens a : Opens X) : Set X)

chartImage_shrinkOpens_subset_Wov_diag

chart_a '' (V a) ⊆ Wov (a,a) (in fact equal).

theorem chartImage_shrinkOpens_subset_Wov_diag (a : 𝔇.ι) :
    (chartAt (H := ℂ) (𝔇.center a)) '' ((𝔇.shrinkOpens a : Opens X) : Set X) ⊆ 𝔇.Wov (a, a)

diagRestrict

The diagonal C0Holo element f a, restricted to the exact chart-image chart_a '' (V a) (which equals Wov (a,a)). Avoids a propositional set-equality cast in diagPullbackGerm.

noncomputable def diagRestrict (f : 𝔇.C0Holo) (a : 𝔇.ι) :
    BddHol ((chartAt (H := ℂ) (𝔇.center a)) '' ((𝔇.shrinkOpens a : Opens X) : Set X))

diagRestrict_toFun_of_mem

theorem diagRestrict_toFun_of_mem (f : 𝔇.C0Holo) (a : 𝔇.ι) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) (𝔇.center a)) '' ((𝔇.shrinkOpens a : Opens X) : Set X)) :
    (𝔇.diagRestrict f a).toFun z = (f a).toFun z

diagPullbackGerm

The germ section ζ_a := [f_a ∘ chart_a] on V a from a diagonal C0Holo element f (bddHolToOmegaDGerm on the exact chart-image chart_a '' (V a)).

noncomputable def diagPullbackGerm (f : 𝔇.C0Holo) (a : 𝔇.ι) :
    ↥(OmegaDGerm (0 : Divisor X) (𝔇.shrinkOpens a))

diagPullbackGerm_holoFn

theorem diagPullbackGerm_holoFn (f : 𝔇.C0Holo) (a : 𝔇.ι) {y : X}
    (hy : y ∈ (𝔇.shrinkOpens a : Opens X)) :
    holoFn (𝔇.diagPullbackGerm f a).2 y
      = (f a).toFun ((chartAt (H := ℂ) (𝔇.center a)) y)

diagPullbackGerm_mem

The germ section diagPullbackGerm f a is 𝒪_0 on V a.

theorem diagPullbackGerm_mem (f : 𝔇.C0Holo) (a : 𝔇.ι) :
    (𝔇.diagPullbackGerm f a).1 ∈ OmegaDGerm (0 : Divisor X) (𝔇.shrinkOpens a)

chart_mem_Wov_of_shrinkInter

For v ∈ V a ⊓ V b, the chart-a value chartAt (center a) v ∈ Wov (a,b).

theorem chart_mem_Wov_of_shrinkInter (a b : 𝔇.ι) {v : X}
    (hv : v ∈ (𝔇.shrinkOpens a ⊓ 𝔇.shrinkOpens b : Opens X)) :
    (chartAt (H := ℂ) (𝔇.center a)) v ∈ 𝔇.Wov (a, b)

refineC1_eq_delta0_shrink

The key germ identity for injectivity. If δ0 f = cechToCshr g, then on each shrinking overlap V a ⊓ V b the germ g_{ab} (restricted) equals [ζ_b] − [ζ_a] (the diagonal pullback germs), i.e. refineC1 g = δ⁰_𝔙 (diagPullbackGerm f). Pointwise via holoFn/diagPullbackGerm_holoFn and the transition point identity.

theorem refineC1_eq_delta0_shrink (g : ↥(𝔇.toFiniteCover.cocycles1 (0 : Divisor X)))
    (f : 𝔇.C0Holo) (hf : (𝔇.holomorphicCoboundaries).δ0 f = 𝔇.cechToCshr g) :
    (𝔇.isRefinement_shrinkCover).refineC1 (g : 𝔇.toFiniteCover.Cochain1)
      = 𝔇.shrinkCover.cechDelta0 (fun a => (𝔇.diagPullbackGerm f a).1)

comparisonMap_injective

Injectivity of the comparison map (Forster 12.4 sheaf-gluing). comparisonMap (mk g) = 0 gives δ0 f = cechToCshr g for some f : C0Holo; then refineC1 g = δ⁰_𝔙 (diagPullbackGerm f) (refineC1_eq_delta0_shrink) so refineC1 g is a 𝔙-coboundary, and Forster 12.4 (refinementDescend_unconditional) gives g ∈ coboundaries1 𝔇, i.e. mk g = 0.

theorem comparisonMap_injective : Function.Injective 𝔇.comparisonMap

finiteDimensional_cechH1_of_holomorphicModel_inj

The finiteness reduction via a linear INJECTION (lighter than the full iso of finiteDimensional_cechH1_of_holomorphicModel). Given a HolomorphicCoboundaries model c for the chart-disk cover with its supH1 finite (via leray), a linear injection cechH1 𝔇 0 ↪ c.supH1 suffices to conclude cechH1 𝔇 0 finite (FiniteDimensional.of_injective).

theorem finiteDimensional_cechH1_of_holomorphicModel_inj
    (c : HolomorphicCoboundaries 𝔇.overlapData)
    (f : 𝔇.toFiniteCover.cechH1 (0 : Divisor X) →ₗ[ℂ] c.supH1) (hf : Function.Injective f) :
    FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 (0 : Divisor X))

finiteDimensional_cechH1_chartDisk_complete

H¹ finiteness on a chart-disk cover (Forster 14.9) — the COMPLETE statement. FiniteDimensional ℂ (cechH1 𝔇 0) for a ChartDiskCover 𝔇.

The δ-complex + comparison that ChartDiskFiniteness.lean leaves open are BUILT here: the model 𝔇.holomorphicCoboundaries (δ-data of §A; the leray field discharged in §A2-*) and the injection 𝔇.comparisonMap (forward germ→BddHol cochain map of §B).

This theorem is SORRY-FREE and axiom-clean (propext, Classical.choice, Quot.sound): the entire δ-complex, the leray lift (Forster 14.6, global Bott–Tu form route — see holomorphicCoboundaries), the comparison comparisonMap and its injectivity (Forster 12.4 sheaf-gluing), and this assembly are all proven.

theorem finiteDimensional_cechH1_chartDisk_complete [Nonempty X] :
    FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 (0 : Divisor X))