19.21. Finiteness.ChartDiskFiniteness🔗

Jacobians.Finiteness.ChartDiskFiniteness — source

e

The chart-i coordinate of the center of U i (the ball center).

noncomputable def e (i : 𝔇.ι) : ℂ

U_subset_chartAt_source

U i is contained in the chart-i source (the chartAt form of subset_chart_source; the chartAt/extChartAt sources agree by extChartAt_source).

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

image_U_eq_ball

The chart-i image of the cover set U i is exactly the open ball ball (e i) (radius i). Directly from ChartDiskCover.isDisk: U i = φ_i⁻¹(ball) ∩ φ_i.source, so φ_i '' (U i) is the part of ball hit by φ_i.source, which (since the ball lies in φ_i.target by closedBall_subset_target) is all of ball. Stated with extChartAt (matching ChartDiskCover's fields).

theorem image_U_eq_ball (i : 𝔇.ι) :
    (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)) '' ((𝔇.U i : Opens X) : Set X)
      = Metric.ball (𝔇.e i) (𝔇.radius i)

Uov

The chart-i image of the overlap U i ∩ U j (using chartAt, the OpenPartialHomeomorph form — defeq to extChartAt for the identity model, so it agrees with image_U_eq_ball).

noncomputable def Uov (p : 𝔇.ι × 𝔇.ι) : Set ℂ

isOpen_Uov

Uov p is open in ℂ (chart image of an open set ⊆ chart source).

theorem isOpen_Uov (p : 𝔇.ι × 𝔇.ι) : IsOpen (𝔇.Uov p)

coverTransition

The cover chart transition τ_{ij} = φ_j ∘ φ_i⁻¹ (chart-i coordinates → chart-j coordinates).

noncomputable def coverTransition (i j : 𝔇.ι) : ℂ → ℂ

coverTransition_apply

The transition τ_{ij} maps φ_i x to φ_j x for x in the overlap (chart cancellation).

theorem coverTransition_apply (i j : 𝔇.ι) {x : X} (hx : x ∈ (𝔇.U i ⊓ 𝔇.U j : Opens X)) :
    𝔇.coverTransition i j ((chartAt (H := ℂ) (𝔇.center i)) x) =
      (chartAt (H := ℂ) (𝔇.center j)) x

BallSplitData

Bott–Tu smooth-split data for a holomorphic cover cocycle on the ball cover (chart-read).

s a b is the chart-a-read of the cocycle component over U_a ∩ U_b (a function ℂ → ℂ, holomorphic on the overlap image Uov (a,b)). g a is the chart-a-read smooth split (ℂ → ℂ, smooth on the whole ball ball (e a) (radius a)). The split identity says g telescopes the cocycle on overlaps: g_b(τ_{ab} z) − g_a(z) = s_{ab}(z) for z in the overlap image. This is exactly the output of a PoU smooth split (Bott–Tu); we take it as a hypothesis so the section is the pure analysis.

structure BallSplitData where

differentiableAt_of_dbar_eq_zero_chartDisk

Local Wirtinger criterion ∂̄g x = 0 ⟹ ℂ-differentiable, for g only ℝ-differentiable at x. Local copy (the CechFinitenessBallSolve branch is excluded by an import collision with GoodCover; this avoids it).

theorem differentiableAt_of_dbar_eq_zero_chartDisk {g : ℂ → ℂ} {x : ℂ}
    (hg : DifferentiableAt ℝ g x) (hdb : DbarDisk.dbar g x = 0) : DifferentiableAt ℂ g x

iUnion_U_eq_univ

The cover sets cover X as sets: ⋃ i, U i = univ (from FiniteCover.covers).

theorem iUnion_U_eq_univ : (⋃ i, ((𝔇.U i : Opens X) : Set X)) = Set.univ

exists_coveringShrinking

A covering relatively-compact open shrinking V_i ⋐ U_i of the cover sets: V_i open, the V_i cover X, and closure V_i ⊆ U_i (compact, since X is compact). From the shrinking lemma exists_iUnion_eq_closure_subset on the normal space X.

theorem exists_coveringShrinking :
    ∃ V : 𝔇.ι → Set X, (⋃ i, V i = Set.univ) ∧ (∀ i, IsOpen (V i)) ∧
      ∀ i, closure (V i) ⊆ ((𝔇.U i : Opens X) : Set X)

shrinkSet

The chosen covering shrinking.

noncomputable def shrinkSet (i : 𝔇.ι) : Set X

shrinkSet_isOpen

theorem shrinkSet_isOpen (i : 𝔇.ι) : IsOpen (𝔇.shrinkSet i)

closure_shrinkSet_subset_U

theorem closure_shrinkSet_subset_U (i : 𝔇.ι) :
    closure (𝔇.shrinkSet i) ⊆ ((𝔇.U i : Opens X) : Set X)

iUnion_shrinkSet_eq_univ

theorem iUnion_shrinkSet_eq_univ : (⋃ i, 𝔇.shrinkSet i) = Set.univ

Wov

The shrinking overlap image Wov (i,j) := φ_i '' (V_i ∩ V_j).

noncomputable def Wov (p : 𝔇.ι × 𝔇.ι) : Set ℂ

isOpen_Wov

theorem isOpen_Wov (p : 𝔇.ι × 𝔇.ι) : IsOpen (𝔇.Wov p)

closure_shrinkInter_compact

closure (V_i ∩ V_j) (in the COMPACT X) is compact.

theorem closure_shrinkInter_compact (p : 𝔇.ι × 𝔇.ι) :
    IsCompact (closure (𝔇.shrinkSet p.1 ∩ 𝔇.shrinkSet p.2))

closure_shrinkInter_subset_source

theorem closure_shrinkInter_subset_source (p : 𝔇.ι × 𝔇.ι) :
    closure (𝔇.shrinkSet p.1 ∩ 𝔇.shrinkSet p.2) ⊆ (chartAt (H := ℂ) (𝔇.center p.1)).source

closure_Wov_subset_Uov

Wov is relatively compact in Uov (the key structural fact). φ_i is a homeomorphism on the compact closure (V_i ∩ V_j) ⊆ φ_i.source, so it maps closure to closure: closure (Wov (i,j)) = φ_i '' (closure (V_i ∩ V_j)) ⊆ φ_i '' (U_i ∩ U_j) = Uov (i,j).

theorem closure_Wov_subset_Uov (p : 𝔇.ι × 𝔇.ι) : closure (𝔇.Wov p) ⊆ 𝔇.Uov p

isCompact_closure_Wov

closure (Wov p) is compact: it is closed and contained in the compact chart-image φ_i '' (closure (V_i ∩ V_j)).

theorem isCompact_closure_Wov (p : 𝔇.ι × 𝔇.ι) : IsCompact (closure (𝔇.Wov p))

overlapData

The HolomorphicDiskOverlapData of a chart-disk cover. Cover side Uov (ball overlaps), shrinking side Wov (covering-shrinking overlaps, relatively compact in Uov). Its restriction ρ is a COMPACT operator for free (HolomorphicDiskOverlapData.rhoRaw_compact, Montel) — the FA-engine input that needed only the relatively-compact shrinking, now supplied.

noncomputable def overlapData (𝔇 : ChartDiskCover X) : HolomorphicDiskOverlapData where

finiteDimensional_cechH1_iff_dolbeault

The two finiteness statements are equivalent (via GoodCover.comparison_linearEquiv'). FiniteDimensional ℂ (cechH1 𝔇 0) ↔ FiniteDimensional ℝ (DolbeaultH01 X): the proven Dolbeault comparison DolbeaultH01 X ≃ₗ[ℝ] cechH1 𝔇 0 transports ℝ-finiteness, and ℂ-finiteness of the ℂ-module cechH1 𝔇 0 is equivalent to its ℝ-finiteness (ℂ is finite over ℝ). So either half of the goal yields the other for free.

theorem finiteDimensional_cechH1_iff_dolbeault
    [ConnectedSpace X] [Nonempty X] :
    FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 (0 : Divisor X))
      ↔ FiniteDimensional ℝ (DolbeaultH01 X)

finiteDimensional_cechH1_of_holomorphicModel

The finiteness reduction (heart plugged in). Given a HolomorphicDiskOverlapData d for the chart-disk cover together with a HolomorphicCoboundaries d c (the δ-complex with the leray field — whose analytic core is exactly forster146_lift, the genuinely-unblocked content) and a comparison cechH1 𝔇 0 ≃ₗ[ℂ] c.supH1, the Čech H¹ is finite-dimensional.

This is the assembly via the proven HolomorphicCoboundaries.finiteDimensional_supH1 (= Forster 14.8/14.7: compact ρ + leray surjectivity ⟹ finite supH1) transported across the comparison. The two inputs are the structural plumbing (G-shrink builds d's shrinking, G-bridge builds the comparison); the analytic content (the leray field) is discharged by the heart.

theorem finiteDimensional_cechH1_of_holomorphicModel
    (d : HolomorphicDiskOverlapData) (c : HolomorphicCoboundaries d)
    (e : 𝔇.toFiniteCover.cechH1 (0 : Divisor X) ≃ₗ[ℂ] c.supH1) :
    FiniteDimensional ℂ (𝔇.toFiniteCover.cechH1 (0 : Divisor X))