19.32. Finiteness.SkyscraperProductWitness🔗

Jacobians.Finiteness.SkyscraperProductWitness — source

coeffGermLin_surjective_of_ne_zero

coeffGermLin is surjective once it is nonzero. Given γ₀ ∈ 𝒪_{D+P}(W) with coeffGermLin γ₀ = c ≠ 0, every a : ℂ is coeffGermLin ((a/c) • γ₀).

theorem coeffGermLin_surjective_of_ne_zero {W : Opens X} {D : Divisor X} {P : X} (hP : P ∈ W)
    {γ₀ : OmegaDGerm (D + Finsupp.single P 1) W} (hc : coeffGermLin hP (D := D) γ₀ ≠ 0) :
    Function.Surjective (coeffGermLin hP (D := D))

coeffGermLin_ne_zero_of_ordU_eq

A section of order *exactly* −(D P)−1 at P has nonzero coefficient. For g ∈ 𝒪_{D+P}(W) with ordU g ⟨P,hP⟩ = −(D P)−1 (the minimal allowed order, a genuine pole of that exact order), the order-(−D(P)−1) coefficient is nonzero (coeffWFn_eq_zero_iff: it vanishes iff the order is *strictly* larger).

theorem coeffGermLin_ne_zero_of_ordU_eq {W : Opens X} {D : Divisor X} {P : X} (hP : P ∈ W)
    {g : W → ℂ} (hg : g ∈ OmegaD (D + Finsupp.single P 1) W)
    (hord : ordU g ⟨P, hP⟩ = ((-(D P) - 1 : ℤ) : WithTop ℤ)) :
    coeffGermLin hP (D := D) ⟨toGerm W g, ⟨g, hg, rfl⟩⟩ ≠ 0

coeffGermLin_surjective_of_exists_witness

Per-cover-set realizability from a witness of exact order. If for every D and P ∈ W there is a section of 𝒪_{D+P}(W) of order *exactly* −(D P)−1 at P, then coeffGermLin is surjective at W (the local Mittag–Leffler condition). The product witness supplies such a section on a chart-disk.

theorem coeffGermLin_surjective_of_exists_witness {W : Opens X} {D : Divisor X} {P : X}
    (hP : P ∈ W)
    (hwit : ∃ g : W → ℂ, ∃ _hg : g ∈ OmegaD (D + Finsupp.single P 1) W,
      ordU g ⟨P, hP⟩ = ((-(D P) - 1 : ℤ) : WithTop ℤ)) :
    Function.Surjective (coeffGermLin hP (D := D))

ordU_comp_chart_eq

Order transfer through the center chart. The intrinsic order on ↥U (ordU) of the chart-pullback witness g = F ∘ φ (with φ = chartAt c and U ⊆ φ.source) at a point x ∈ U equals the *planar* order of F at φ x.

ordU g ⟨x⟩ is read in the *ambient* chart at x (CechH0.ordU_eq_orderAt_Gext), where Gext g agrees with F ∘ φ; the chart-transition φ ∘ (chartAt x).symm is an analytic biholomorphism (transition_analyticAt_of_mem + transition_deriv_ne_zero), so meromorphicOrderAt_comp_of_deriv_ne_zero collapses the composition to meromorphicOrderAt F (φ x).

theorem ordU_comp_chart_eq {c : X} {U : Opens X}
    (hU : (U : Set X) ⊆ (chartAt (H := ℂ) c).source) (F : ℂ → ℂ) {x : X} (hx : x ∈ U) :
    ordU (fun w : U => F ((chartAt (H := ℂ) c) w.1)) ⟨x, hx⟩ =
      meromorphicOrderAt F ((chartAt (H := ℂ) c) x)

isMeromorphic_comp_chart

Meromorphy of the chart-pullback witness on ↥U. If F is meromorphic on all of ℂ and U ⊆ φ.source (φ = chartAt c), then g = F ∘ φ is meromorphic on the open submanifold ↥U: in each point's own chart it agrees with F ∘ (φ ∘ chart.symm) (an analytic-precomposition of the meromorphic F).

theorem isMeromorphic_comp_chart {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {c : X} {U : Opens X}
    (hU : (U : Set X) ⊆ (chartAt (H := ℂ) c).source) {F : ℂ → ℂ} (hF : ∀ z : ℂ, MeromorphicAt F z) :
    IsMeromorphic (U : Type _) (fun w : U => F ((chartAt (H := ℂ) c) w.1))

exists_orderExact_witness_chartDisk

Existence of an exact-order witness on each chart-disk cover-set — the local-analytic core of the χ-side (Forster §16, Mittag–Leffler).

For each chart-disk cover-set U j ∋ P and divisor D, there is a section g ∈ 𝒪_{D+P}(U j) of order *exactly* −(D P)−1 at P.

The witness is the factorized rational g = (∏ᶠ u, (· − u)^{dz u}) ∘ φ read through the *center* chart φ = chartAt (center j) (U j ⊆ φ.source), with exponent dz w = −(D+P)(φ.symm w) on φ.target (zero off it) — so dz (φ x) = −(D+P)(x) for every x ∈ U j. The Mathlib FactorizedRational API supplies the planar facts (meromorphicNFOn_univ — meromorphic everywhere; meromorphicOrderAt_eq — order dz z at z), and ordU_comp_chart_eq / isMeromorphic_comp_chart transfer them through the chart to ↥(U j). Hence ordU g ⟨x⟩ = −(D+P)(x) for every x ∈ U j: this meets the 𝒪_{D+P} bound with equality everywhere, and at P gives the exact order −(D+P)(P) = −(D P)−1.

theorem exists_orderExact_witness_chartDisk (D : Divisor X)
    (j : (chartDiskCover (X := X)).ι) (P : X) (hP : P ∈ (chartDiskCover (X := X)).U j) :
    ∃ g : (chartDiskCover (X := X)).U j → ℂ,
      ∃ _ : g ∈ OmegaD (D + Finsupp.single P 1) ((chartDiskCover (X := X)).U j),
      ordU g ⟨P, hP⟩ = ((-(D P) - 1 : ℤ) : WithTop ℤ)

locallyRealizable_chartDiskCover

Local realizability of the canonical chart-disk cover (the product witness / local Mittag–Leffler). At every chart-disk cover-set U j ∋ P, the order-(−D(P)−1) principal-part coefficient coeffGermLin is surjective onto ℂ, for every divisor D — the single analytic input the cone skyscraper construction consumes. Proven from the exact-order witness (exists_orderExact_witness_chartDisk) via coeffGermLin_surjective_of_exists_witness.

theorem locallyRealizable_chartDiskCover :
    (chartDiskCover (X := X)).toFiniteCover.LocallyRealizable

exists_realizableLerayCover

A realizable Leray cover exists — the canonical chart-disk cover is both Leray (simply connected sets, chartDiskCover_simplyConnected) and locally realizable (locallyRealizable_chartDiskCover). This unlocks the ladder→headline wiring with the cone skyscraper construction.

theorem exists_realizableLerayCover :
    ∃ 𝔘 : FiniteCover X, 𝔘.IsLeray ∧ 𝔘.LocallyRealizable