A machine-checked solution to the Jacobians challenge

19.11. Finiteness.CechModelBase🔗

Jacobians.Finiteness.CechModelBase — source

DiskOverlapData

Sup-norm cochain geometry. The finite pair-index J of a Leray chart-disk cover, with, for each overlap p, the chart-image cover-open Uov p ⊆ ℂ and a relatively-compact convex shrinking Kov p ⋐ Uov p. This is exactly the geometric input the disk-Montel atom needs (open U, compact convex K ⊆ U). The cover 1-cochains live in Π_p BddHol (Uov p), the shrinking 1-cochains in Π_p (Kov p →ᵇ ℂ).

structure DiskOverlapData where

compactSpace

Each shrinking compact carries a CompactSpace (so Kov p →ᵇ ℂ is a Banach space).

noncomputable instance compactSpace (p : d.J) : CompactSpace (d.Kov p)

Ccov

COVER 1-cochains: bounded-holomorphic on each overlap chart-image.

abbrev Ccov : Type

Cshr

SHRINKING 1-cochains: bounded-continuous on each compact shrunk overlap (where the Montel atom lands).

abbrev Cshr : Type

rhoRaw

The raw cochain restriction Π_p BddHol (Uov p) →L[ℂ] Π_p (Kov p →ᵇ ℂ), componentwise BddHol.restrictCLM.

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

rhoRaw_apply

@[simp] theorem rhoRaw_apply (f : d.Ccov) (p : d.J) :
    d.rhoRaw f p = BddHol.restrictCLM (d.hKU p) (f p)

rhoRaw_compact

The Montel payoff. The cochain restriction ρ (cover → shrinking) is a compact operator: componentwise it is BddHol.restrictCLM, compact by the disk-Montel atom (BddHol.isCompactOperator_restrictCLM_of_compact, valid for any compact shrunk overlap — no convexity), and a finite product of compacts is compact (isCompactOperator_pi).

theorem rhoRaw_compact : IsCompactOperator d.rhoRaw

Coboundaries

Sup-norm coboundary data completing DiskOverlapData to a Čech δ-complex. We need the shrinking-side coboundaries δ⁰ : C0 → C¹(shrinking) and δ¹ : C¹(shrinking) → C²(shrinking) with δ¹∘δ⁰ = 0, a coboundary δ¹ on the COVER side (whose kernel is Z¹(cover)), and the commuting square saying restriction ρ carries cover-cocycles to shrinking-cocycles. These are the analytic inputs that make Z¹/B¹ the sup-norm H¹.

structure Coboundaries (d : DiskOverlapData) 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). Its range is B¹, and Z¹/range δ is the sup-norm H¹.

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

Compactness on the cocycle subspace. ρ : Z¹(cover) →L Z¹(shrinking) is a compact operator: rhoRaw is compact (DiskOverlapData.rhoRaw_compact), ρ includes into it via the closed cocycle subspace, and isCompactOperator_of_subtypeL_comp transports compactness back.

theorem ρ_compact : IsCompactOperator c.ρ

supH1

The sup-norm H¹ of the cover/shrinking pair: Z¹(shrinking) ⧸ B¹, where B¹ = range δ. This is the object the abstract reduction makes finite-dimensional; it is compared to the genuine germ-class cechH1 by cechH1_model.

abbrev supH1 : Type

finiteDimensional_supH1

Finiteness of the sup-norm H¹. Given the Leray surjectivity of (η,ξ) ↦ δη + ρξ, the abstract reduction finiteDimensional_h1_of_leray_compact (with ρ compact by ρ_compact) gives supH1 finite-dimensional.

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 any chart-disk Leray model c, the combined map (η, ξ) ↦ δη + ρξ (shrinking-coboundary ⊕ cover-restriction) is surjective onto Z¹(shrinking).

This unpacks the model's leray field (the disk-acyclicity witness): given a shrinking cocycle t ∈ Z¹(shrinking) (so δ¹ t = 0), c.leray produces η : C⁰ and a cover cocycle x (δ¹_cov x = 0) with t = δ⁰η + ρ_raw x; corestricting to the cocycle subspaces (c.δ, c.ρ), the pair (η, ⟨x, _⟩) maps to t. The genuine analytic content (H¹(disk, 𝒪) = 0 + Čech refinement) is carried by the leray field and discharged where the model is built; here it is pure bookkeeping.

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

trivialCoboundaries

The trivial acyclic Coboundaries. For any DiskOverlapData d, the Coboundaries d with C⁰ = Cshr, δ⁰ = id, δ¹ = 0, δ¹_cov = 0. Structural fields hold trivially; the genuine analytic leray field is DISCHARGED (every shrinking cocycle s is δ⁰ s + ρ 0 = s). Its sup-norm H¹ is 0 (supH1_trivialCoboundaries_subsingleton) — the leray disk-acyclicity field wired at the acyclic extreme, the shape the completed hasGluedDbarDatum lands in.

noncomputable def trivialCoboundaries : Coboundaries d where

supH1_trivialCoboundaries_subsingleton

The trivial model is acyclic. (trivialCoboundaries d).supH1 is a subsingleton: its Z¹(shrinking) = ker δ¹ = Cshr (δ¹ = 0) and range δ = ⊤ (δ corestricts the surjective δ⁰ = id), so the quotient is trivial.

theorem supH1_trivialCoboundaries_subsingleton :
    Subsingleton (d.trivialCoboundaries).supH1

empty

A DiskOverlapData with empty overlap index (so Ccov/Cshr are subsingletons) — the carrier of the trivial model that witnesses the acyclic exists_cechModel.

def empty : DiskOverlapData where