19.17. Finiteness.CechModelHolomorphicDelta🔗

Jacobians.Finiteness.CechModelHolomorphicDelta — source

montel_coverCenter_eq_coverCenter

The cover centres of the holomorphic model and the continuous model coincide definitionally (montel_coverCenter = coverCenter). We expose this rfl as a simp lemma so the coverTransition (defined via coverCenter) unfolds cleanly against the Wov/Uov sets (defined via montel_coverCenter).

theorem montel_coverCenter_eq_coverCenter {X : Type*} [TopologicalSpace X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a : Fin ((chartCover : Finset X).card)) :
    montel_coverCenter (X := X) a = coverCenter (X := X) a

innerChartOpen_subset_chartAt_source_aux

A point of innerChartOpen (montel_coverCenter a) lies in the chart source.

theorem innerChartOpen_subset_chartAt_source_aux {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a : Fin ((chartCover : Finset X).card)) :
    innerChartOpen (X := X) (montel_coverCenter (X := X) a) ⊆
      (chartAt (H := ℂ) (montel_coverCenter (X := X) a)).source

analyticOn_coverTransition_Wov

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

theorem analyticOn_coverTransition_Wov {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (a b : Fin ((chartCover : Finset X).card)) :
    AnalyticOn ℂ (coverTransition (X := X) a b)
      ((chartCoverHolomorphicDiskOverlapData (X := X)).Wov (a, b))

mapsTo_coverTransition_Wov

The cover transition τ_{ab} maps the OPEN shrinking Wov (a,b) (chart-a coordinates) into coverSetImage b (chart-b image of chartOpen b), where the b-component of a 0-cochain is bounded-holomorphic. A point φ_a x with x ∈ innerChartOpen a ∩ innerChartOpen b maps to φ_b x with x ∈ innerChartOpen b ⊆ chartOpen b, so φ_b x ∈ φ_b '' (chartOpen b) = coverSetImage b.

theorem mapsTo_coverTransition_Wov {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b : Fin ((chartCover : Finset X).card)) :
    Set.MapsTo (coverTransition (X := X) a b)
      ((chartCoverHolomorphicDiskOverlapData (X := X)).Wov (a, b))
      (coverSetImage (X := X) b)

Wov_subset_coverSetImage_fst

The shrinking Wov (a,b) lies in coverSetImage a (chart-a image of innerChartOpen a ∩ innerChartOpen b ⊆ chartOpen a), so the a-component restricts directly.

theorem Wov_subset_coverSetImage_fst {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b : Fin ((chartCover : Finset X).card)) :
    (chartCoverHolomorphicDiskOverlapData (X := X)).Wov (a, b) ⊆ coverSetImage (X := X) a

delta0ModelHolo

The cross-chart Čech δ⁰ of the holomorphic-shrinking model: Cochain0Model →L[ℂ] d.Cshr. 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: the off-diagonal via BddHol.precompHolCLM, the diagonal via BddHol.restrictOpenCLM.

The 0-cochain spaces Cochain0Model = ∀ a, BddHol (coverSetImage a) are branch-independent (CechModelDelta); coverSetImage a = (chartAt (coverCenter a)) '' (chartOpen a) is definitionally Uov (a,a), the diagonal cover open, so the diagonal restriction reads f a : BddHol (coverSetImage a) = BddHol (Uov (a,a)) and the transport lands f b in Uov (b,b) = coverSetImage b.

noncomputable def delta0ModelHolo :
    Cochain0Model (X := X) →L[ℂ] (chartCoverHolomorphicDiskOverlapData (X := X)).Cshr

delta0ModelHolo_apply

The component identity for δ⁰ at overlap p = (a,b).

theorem delta0ModelHolo_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : Cochain0Model (X := X)) (p : (chartCoverHolomorphicDiskOverlapData (X := X)).J) :
    delta0ModelHolo 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_coverSetImage_fst p.1 p.2) (f p.1)

delta0ModelHolo_apply_apply

The Čech coboundary pointwise formula. On the OPEN shrinking Wov (a,b), the δ⁰ value at a point z is f b evaluated at the transported point τ_{ab} z minus f a at z — the explicit cross-chart Čech δ⁰ formula (δ⁰f)_{ab}(z) = f_b(τ_{ab} z) − f_a(z).

theorem delta0ModelHolo_apply_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (f : Cochain0Model (X := X)) (p : (chartCoverHolomorphicDiskOverlapData (X := X)).J)
    {z : ℂ} (hz : z ∈ (chartCoverHolomorphicDiskOverlapData (X := X)).Wov p) :
    (delta0ModelHolo 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 inner overlap innerChartOpen a ∩ innerChartOpen b ∩ innerChartOpen c — the shrinking-side 2-cochain domain (relatively compact in coverTripleImage).

noncomputable def WovTriple (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) : Set ℂ

isOpen_WovTriple

theorem isOpen_WovTriple {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) :
    IsOpen (WovTriple (X := X) t)

C2Holo

Sup-norm 2-cochains, holomorphic shrinking side C2Holo — bounded-holomorphic on each open triple WovTriple t (target of the shrinking-side δ¹).

abbrev C2Holo : Type

analyticOn_coverTransition_WovTriple

The cover transition τ_{ab} is analytic on the OPEN triple WovTriple (a,b,c).

theorem analyticOn_coverTransition_WovTriple {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    AnalyticOn ℂ (coverTransition (X := X) a b) (WovTriple (X := X) (a, b, c))

mapsTo_coverTransition_WovTriple_shrink

The cover transition τ_{ab} maps the OPEN triple WovTriple (a,b,c) (chart-a coordinates) into the shrinking Wov (b,c) (chart-b image of innerChartOpen b ∩ innerChartOpen c). The (b,c) transport is routed through Wov (b,c) — matching the Cshr shrinking-component domain BddHol (Wov (b,c)) — rather than the larger Uov (b,c). A point φ_a x with x ∈ innerChartOpen a ∩ innerChartOpen b ∩ innerChartOpen c maps to φ_b x with x ∈ innerChartOpen b ∩ innerChartOpen c.

theorem mapsTo_coverTransition_WovTriple_shrink {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    Set.MapsTo (coverTransition (X := X) a b) (WovTriple (X := X) (a, b, c))
      ((chartCoverHolomorphicDiskOverlapData (X := X)).Wov (b, c))

WovTriple_subset_Wov_fst_snd

The OPEN triple WovTriple (a,b,c) lies in Wov (a,b) (chart-a image of innerChartOpen a ∩ innerChartOpen b ⊇ innerChartOpen a ∩ innerChartOpen b ∩ innerChartOpen c).

theorem WovTriple_subset_Wov_fst_snd {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    WovTriple (X := X) (a, b, c) ⊆ (chartCoverHolomorphicDiskOverlapData (X := X)).Wov (a, b)

WovTriple_subset_Wov_fst_trd

The OPEN triple WovTriple (a,b,c) lies in Wov (a,c).

theorem WovTriple_subset_Wov_fst_trd {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) :
    WovTriple (X := X) (a, b, c) ⊆ (chartCoverHolomorphicDiskOverlapData (X := X)).Wov (a, c)

delta1ModelHolo

The cross-chart Čech δ¹ on the HOLOMORPHIC shrinking side d.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), the genuine Čech coboundary with the (b,c)-component transported chart-b→chart-a through the holomorphic transition τ_{ab}. All three pieces stay BddHol on the open triple: the off-diagonal via BddHol.precompHolCLM (Wov (b,c) → WovTriple), the two diagonal restrictions via BddHol.restrictOpenCLM (Wov (a,c), Wov (a,b) → WovTriple).

noncomputable def delta1ModelHolo :
    (chartCoverHolomorphicDiskOverlapData (X := X)).Cshr →L[ℂ] C2Holo (X := X)

delta1ModelHolo_apply

The component identity for the shrinking-side δ¹ at the triple t = (a,b,c).

theorem delta1ModelHolo_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (s : (chartCoverHolomorphicDiskOverlapData (X := X)).Cshr)
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) :
    delta1ModelHolo 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))

delta1ModelHolo_apply_apply

The shrinking-side Čech coboundary pointwise formula. On the OPEN triple WovTriple, the δ¹ value at z is s_{bc} at the transported point τ_{ab} z minus s_{ac} at z plus s_{ab} at z — the explicit cross-chart Čech δ¹ formula (δ¹s)_{abc}(z) = s_{bc}(τ_{ab} z) − s_{ac}(z) + s_{ab}(z).

theorem delta1ModelHolo_apply_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (s : (chartCoverHolomorphicDiskOverlapData (X := X)).Cshr)
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) {z : ℂ} (hz : z ∈ WovTriple (X := X) t) :
    (delta1ModelHolo 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

delta1CovModelHolo

The cross-chart Čech δ¹ on the COVER side d.Ccov →L[ℂ] Cochain2CovModel. REUSED verbatim from CechModelDifferential.delta1CovModel: the holomorphic cover side d.Ccov = ∀ p, BddHol (Uov p) is definitionally the continuous cover side (same cover centres montel_coverCenter = coverCenter, same outer overlaps Uov), so the cover-side coboundary is identical.

noncomputable def delta1CovModelHolo :
    (chartCoverHolomorphicDiskOverlapData (X := X)).Ccov →L[ℂ] Cochain2CovModel (X := X)

coverTransition_cocycle_Wov

The chart-transition cocycle identity on the OPEN triple WovTriple: τ_{bc}(τ_{ab} z) = τ_{ac} z for z ∈ WovTriple (a,b,c). Geometrically φ_c ∘ φ_b⁻¹ ∘ φ_b ∘ φ_a⁻¹ = φ_c ∘ φ_a⁻¹ where the inner cancellations hold because the triple-overlap point x lies in all three chart sources. The algebraic heart of δ¹∘δ⁰ = 0.

theorem coverTransition_cocycle_Wov {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (a b c : Fin ((chartCover : Finset X).card)) {z : ℂ}
    (hz : z ∈ WovTriple (X := X) (a, b, c)) :
    coverTransition b c (coverTransition a b z) = coverTransition a c z

delta1_comp_delta0_holo

δ¹ ∘ δ⁰ = 0 (the Čech hδδ). The composite of the cross-chart δ⁰ and the shrinking-side δ¹ vanishes — the defining Čech-complex identity δ² = 0. Pointwise on the OPEN triple the six terms of (δ¹(δ⁰f))_{abc}(z) collapse to f_c(τ_{bc}(τ_{ab} z)) − f_c(τ_{ac} z), which is 0 by the cocycle identity coverTransition_cocycle_Wov (the two f_c-arguments coincide).

theorem delta1_comp_delta0_holo {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    :
    (delta1ModelHolo (X := X)).comp delta0ModelHolo = 0

WovTriple_subset_coverTripleImage

The OPEN triple WovTriple (a,b,c) lies in the cover triple-image coverTripleImage (a,b,c) (chart-a image of innerChartOpen a ∩ innerChartOpen b ∩ innerChartOpen c ⊆ chartOpen a ∩ chartOpen b ∩ chartOpen c), so a cover 2-cochain restricts to a holomorphic shrinking 2-cochain.

theorem WovTriple_subset_coverTripleImage {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X]
    (t : Fin ((chartCover : Finset X).card) ×
    Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card)) :
    WovTriple (X := X) t ⊆ coverTripleImage (X := X) t

rho2ModelHolo

The 2-cochain restriction ρ² : Cochain2CovModel →L C2Holo (cover → holomorphic shrinking), componentwise BddHol.restrictOpenCLM from the open cover triple-image to the open shrinking triple. Carries the cover-side δ¹ to the shrinking-side δ¹ (the commuting square).

noncomputable def rho2ModelHolo : Cochain2CovModel (X := X) →L[ℂ] C2Holo (X := X)

rho2ModelHolo_apply

@[simp] theorem rho2ModelHolo_apply {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X]
    (g : Cochain2CovModel (X := X))
    (t : Fin ((chartCover : Finset X).card) × Fin ((chartCover : Finset X).card) ×
      Fin ((chartCover : Finset X).card)) :
    rho2ModelHolo g t = BddHol.restrictOpenCLM (WovTriple_subset_coverTripleImage t) (g t)

delta1_comp_rhoRaw_eq_rho2_comp_delta1Cov_holo

The commuting square δ¹_shr ∘ ρ = ρ² ∘ δ¹_cov. Restricting a cover 1-cochain to the holomorphic shrinking and applying the shrinking δ¹ is the same as applying the cover δ¹ and restricting the resulting 2-cochain — the Čech naturality of δ¹ under cover-refinement. Pointwise both sides equal x_{bc}(τ_{ab} z) − x_{ac}(z) + x_{ab}(z) on the OPEN triple.

theorem delta1_comp_rhoRaw_eq_rho2_comp_delta1Cov_holo {X : Type*} [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    :
    (delta1ModelHolo (X := X)).comp (chartCoverHolomorphicDiskOverlapData (X := X)).rhoRaw
      = rho2ModelHolo.comp delta1CovModelHolo

hcomm_holo

hcomm for the holomorphic-shrinking chart cover. If a cover 1-cochain x is a cocycle (δ¹_cov x = 0), then its restriction ρ x (to the holomorphic shrinking) is a shrinking cocycle (δ¹_shr (ρ x) = 0). Immediate from the commuting square δ¹_shr∘ρ = ρ²∘δ¹_cov: δ¹_shr(ρ x) = ρ²(δ¹_cov x) = ρ²(0) = 0. This is the HolomorphicCoboundaries.hcomm field for the chart cover.

theorem hcomm_holo {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (x : (chartCoverHolomorphicDiskOverlapData (X := X)).Ccov) (hx : delta1CovModelHolo x = 0) :
    delta1ModelHolo ((chartCoverHolomorphicDiskOverlapData (X := X)).rhoRaw x) = 0