19.16. Finiteness.CechModelHolomorphic🔗

Jacobians.Finiteness.CechModelHolomorphic — source

HolomorphicDiskOverlapData

Corrected overlap data for the holomorphic-shrinking branch: the cover side stays BddHol (Uov p), while the shrinking side is BddHol (Wov p) for an open relatively-compact shrinking Wov p ⋐ Uov p.

structure HolomorphicDiskOverlapData where

Ccov

Cover 1-cochains: bounded-holomorphic functions on the overlap opens.

abbrev Ccov : Type

Cshr

Corrected shrinking 1-cochains: bounded-holomorphic functions on the open shrinkings.

abbrev Cshr : Type

rhoRaw

The raw cover → corrected-shrinking restriction, componentwise BddHol.restrictOpenCLM.

noncomputable def rhoRaw : d.Ccov →L[ℂ] d.Cshr

rhoRaw_apply

theorem rhoRaw_apply (f : d.Ccov) (p : d.J) :
    d.rhoRaw f p = BddHol.restrictOpenCLM (subset_closure.trans (d.hWU p)) (f p)

rhoRaw_compact

The cochain restriction ρ (cover → holomorphic shrinking) is a compact operator: componentwise it is BddHol.restrictOpenCLM, compact for a relatively compact open shrinking Wov p ⋐ Uov p, and a finite product of compacts is compact.

theorem rhoRaw_compact : IsCompactOperator d.rhoRaw

montel_coverCenter

The chart center corresponding to the Fin-enumeration of chartCover.

noncomputable def montel_coverCenter (a : Fin ((chartCover : Finset X).card)) : X

montel_coverCenter_mem

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

montel_chartOpen_subset_chartAt_source

theorem montel_chartOpen_subset_chartAt_source {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X)
    (hx : x ∈ (chartCover : Finset X)) :
    chartOpen (X := X) x ⊆ (chartAt (H := ℂ) x).source

montel_innerChartOpen_subset_chartOpen

theorem montel_innerChartOpen_subset_chartOpen {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ChartedSpace ℂ X] (x : X) :
    innerChartOpen (X := X) x ⊆ chartOpen (X := X) x

chartCoverHolomorphicDiskOverlapData

The outer holomorphic shrinking geometry from Montel.Cover: Uov is the open chart image of the chartOpen overlap, while Wov is the open chart image of the smaller innerChartOpen overlap. The latter has compact closure inside Uov, giving the corrected branch a genuine relatively-compact open shrinking.

noncomputable def chartCoverHolomorphicDiskOverlapData : HolomorphicDiskOverlapData where

HolomorphicCoboundaries

Corrected coboundary data for the holomorphic-shrinking branch. It mirrors Coboundaries, but the shrinking cochains live in BddHol (Wov p) rather than →ᵇ on compacts.

structure HolomorphicCoboundaries (d : HolomorphicDiskOverlapData) where

Z1cov

Z¹(cover) = ker δ¹(cover), a closed subspace of the cover 1-cochains.

noncomputable def Z1cov : Submodule ℂ d.Ccov

Z1shr

Z¹(shrinking) = ker δ¹(shrinking), a closed subspace of the shrinking 1-cochains.

noncomputable def Z1shr : Submodule ℂ d.Cshr

isClosed_Z1shr

theorem isClosed_Z1shr : IsClosed (c.Z1shr : Set d.Cshr)

δ

The coboundary δ : C⁰ →L[ℂ] Z¹(shrinking) (i.e. δ⁰ corestricted to the cocycles, using δ¹∘δ⁰=0).

noncomputable def δ : c.C0 →L[ℂ] c.Z1shr

ρ

The restriction ρ : Z¹(cover) →L[ℂ] Z¹(shrinking) (the raw restriction rhoRaw restricted to the cocycle subspaces, using the commuting square hcomm).

noncomputable def ρ : c.Z1cov →L[ℂ] c.Z1shr

subtypeL_comp_ρ

subtypeL ∘ ρ = rhoRaw ∘ subtypeL — the defining commuting identity for ρ.

theorem subtypeL_comp_ρ :
    c.Z1shr.subtypeL.comp c.ρ = d.rhoRaw.comp c.Z1cov.subtypeL

ρ_compact

The restriction ρ : Z¹(cover) →L Z¹(shrinking) is compact.

theorem ρ_compact : IsCompactOperator c.ρ

supH1

The sup-norm H¹ of the corrected holomorphic branch: Z¹(shrinking) ⧸ B¹.

abbrev supH1 : Type

finiteDimensional_supH1

Finiteness of the corrected branch's sup-norm H¹, conditional on Leray surjectivity.

theorem finiteDimensional_supH1
    (hsurj : Function.Surjective (fun p : c.C0 × c.Z1cov => c.δ p.1 + c.ρ p.2)) :
    FiniteDimensional ℂ c.supH1

leray_surjective

Leray surjectivity for the corrected holomorphic branch.

theorem leray_surjective (d : HolomorphicDiskOverlapData) (c : HolomorphicCoboundaries d) :
    Function.Surjective (fun p : c.C0 × c.Z1cov => c.δ p.1 + c.ρ p.2)

trivialCoboundaries

The trivial acyclic corrected model.

noncomputable def trivialCoboundaries : HolomorphicCoboundaries d where

supH1_trivialCoboundaries_subsingleton

The corrected trivial model is acyclic.

theorem supH1_trivialCoboundaries_subsingleton :
    Subsingleton (d.trivialCoboundaries).supH1

empty

The empty overlap-index corrected model.

def empty : HolomorphicDiskOverlapData where