19.10. Finiteness.CechModelArtificial🔗

Jacobians.Finiteness.CechModelArtificial — source

onePointBcfEquiv

A bounded-continuous function on the one-point space ↥({(0:ℂ)} : Set ℂ) is determined by its single value, giving (↥{0} →ᵇ ℂ) ≃ₗ[ℂ] ℂ.

noncomputable def onePointBcfEquiv : (↥({(0:ℂ)} : Set ℂ) →ᵇ ℂ) ≃ₗ[ℂ] ℂ

bddHolConst

The constant-c element of BddHol (Metric.ball 0 1): the function equal to c on the ball and 0 outside, which is analytic on the ball (it agrees with the constant c there) and bounded.

noncomputable def bddHolConst (c : ℂ) : BddHol (Metric.ball (0 : ℂ) 1)

bddHolConst_toFun_mem

@[simp] theorem bddHolConst_toFun_mem (c : ℂ) {z : ℂ} (hz : z ∈ Metric.ball (0 : ℂ) 1) :
    (bddHolConst c).toFun z = c

artificialData

The single-point chart-disk overlap data on Fin k: every overlap is the unit disk Metric.ball 0 1, every shrinking is the single point {0}.

def artificialData (k : ℕ) : DiskOverlapData where

artificialData_rhoRaw_surjective

rhoRaw of the artificial model is SURJECTIVE: each component BddHol.restrictCLM : BddHol (ball 0 1) → (↥{0} →ᵇ ℂ) is surjected by a constant bounded-holomorphic function, since the one-point bcf is determined by its value at 0.

theorem artificialData_rhoRaw_surjective (k : ℕ) :
    Function.Surjective (artificialData k).rhoRaw

artificialCoboundaries

The trivial-δ Coboundaries on the artificial model: C0 = C2 = C2cov = PUnit, every coboundary map is 0. The leray field reduces (since δ0 = δ1 = δ1cov = 0) to the surjectivity of rhoRaw, which holds because the one-point shrinking is realized by constant bounded-holomorphic functions.

noncomputable def artificialCoboundaries (k : ℕ) : Coboundaries (artificialData k) where

artificialCshrEquiv

The shrinking cochains of the artificial model are (Fin k → ℂ), via the one-point bcf equiv on each factor.

noncomputable def artificialCshrEquiv (k : ℕ) :
    (Fin k → ℂ) ≃ₗ[ℂ] (artificialData k).Cshr

artificialCoboundaries_Z1shr_eq_top

Z¹(shrinking) of the artificial model is ⊤ (δ¹ = 0).

theorem artificialCoboundaries_Z1shr_eq_top (k : ℕ) :
    (artificialCoboundaries k).Z1shr = ⊤

artificialCoboundaries_range_δ_eq_bot

The coboundary δ of the artificial model is 0 (δ0 = 0), so range δ = ⊥.

theorem artificialCoboundaries_range_δ_eq_bot (k : ℕ) :
    LinearMap.range (artificialCoboundaries k).δ.toLinearMap = ⊥

artificialSupH1Equiv

supH1 of the artificial model is ℂ-linearly isomorphic to the shrinking cochains Cshr: B¹ = range δ = ⊥ (so Cshr ⧸ B¹ ≅ ↥Z¹) and Z¹ = ⊤ (so ↥Z¹ ≅ Cshr).

noncomputable def artificialSupH1Equiv (k : ℕ) :
    (artificialCoboundaries k).supH1 ≃ₗ[ℂ] (artificialData k).Cshr

exists_cechModel_of_finiteDimensional

The artificial (single-point) model witnesses the bundled exists_cechModel shape. For any finite-dimensional germ-class H¹, there is a DiskOverlapData + Coboundaries whose sup-norm H¹ is ℂ-linearly isomorphic to 𝔘.cechH1 D.

Soundness: the model is artificial (it does NOT read the cover geometry); it uses a ONE-POINT shrinking Kov = {0}, which keeps the shrinking cochains finite-dimensional, so the leray field (forcing the compact rhoRaw to surject) is consistent and provable. The comparison composes 𝔘.cechH1 D ≅ (Fin k → ℂ) ≅ Cshr ≅ supH1 with k = finrank ℂ (𝔘.cechH1 D).

theorem exists_cechModel_of_finiteDimensional
    (𝔘 : FiniteCover X) (D : Divisor X) [FiniteDimensional ℂ (𝔘.cechH1 D)] :
    ∃ (d : Jacobians.Dolbeault.DiskOverlapData) (c : Jacobians.Dolbeault.Coboundaries d),
      Nonempty (𝔘.cechH1 D ≃ₗ[ℂ] c.supH1)