A machine-checked solution to the Jacobians challenge

19.28. Finiteness.SkyscraperArrow🔗

Jacobians.Finiteness.SkyscraperArrow — source

ordU_congr

ordU is 𝓝[≠]-germ-invariant on the open submanifold ↥U: two functions agreeing off a discrete set near u have equal order at u (chart-transport via eventually_comp_chart_iff' + meromorphicOrderAt_congr).

theorem ordU_congr {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Opens X}
    {f g : U → ℂ} {u : U} (h : f =ᶠ[𝓝[≠] u] g) :
    ordU f u = ordU g u

OmegaD_add_single_eq_of_not_mem

On an open U not containing P, the order bounds for 𝒪_D and 𝒪_{D+P} coincide pointwise (single P 1 is supported at P ∉ U), so the section submodules agree: 𝒪_{D+P}(U) = 𝒪_D(U).

theorem OmegaD_add_single_eq_of_not_mem {U : Opens X} {D : Divisor X} {P : X} (hP : P ∉ U) :
    OmegaD (D + Finsupp.single P 1) U = OmegaD D U

OmegaDGerm_add_single_eq_of_not_mem

Germ version: on an open U not containing P, OmegaDGerm (D+P) U = OmegaDGerm D U.

theorem OmegaDGerm_add_single_eq_of_not_mem {U : Opens X} {D : Divisor X} {P : X} (hP : P ∉ U) :
    OmegaDGerm (D + Finsupp.single P 1) U = OmegaDGerm D U

mem_OmegaDGerm_of_overlap_match

Overlap membership transport (the case P ∈ V). If on the overlap U ⊓ V two matching germs (hmatch) come from γU ∈ OmegaDGerm D U and γV ∈ OmegaDGerm (D+P) V, then γV already lies in the *smaller* OmegaDGerm D V. Reason: the order of γV at P (read on V) equals the order of γU at P (read on U, via the overlap — orders are 𝓝[≠]-germ- and restriction-invariant), and γU ∈ 𝒪_D bounds that order by −(D P); mem_OmegaD_iff_ordU_at_P then upgrades γV's 𝒪_{D+P}- membership to 𝒪_D-membership. This is the genuine sheaf-theoretic content of exact₁₂.

theorem mem_OmegaDGerm_of_overlap_match {U V : Opens X} {D : Divisor X} {P : X}
    (hPU : P ∈ U) (hPV : P ∈ V) {γU : MGerm U} {γV : MGerm V}
    (hγU : γU ∈ OmegaDGerm D U) (hγV : γV ∈ OmegaDGerm (D + Finsupp.single P 1) V)
    (hmatch : rawRestrictG (inf_le_right : U ⊓ V ≤ V) γV
      = rawRestrictG (inf_le_left : U ⊓ V ≤ U) γU) :
    γV ∈ OmegaDGerm D V

restrictToCoverSet

Restrict a global 𝒪_D-section to its component germ on the cover-set U i, as an element of the subtype ↥(OmegaDGerm D (U i)). The underlying map is s ↦ s.1 i; the codomain-restriction membership s.1 i ∈ OmegaDGerm D (U i) is the sections0 half of globalSections = ker δ⁰ ⊓ sections0.

noncomputable def restrictToCoverSet (i : 𝔘.ι) :
    ↥(𝔘.globalSections D) →ₗ[ℂ] ↥(OmegaDGerm D (𝔘.U i))

restrictToCoverSet_coe

@[simp] theorem restrictToCoverSet_coe (i : 𝔘.ι) (s : ↥(𝔘.globalSections D)) :
    (𝔘.restrictToCoverSet D i s : MGerm (𝔘.U i)) = (s : 𝔘.Cochain0) i

globalSections_matching

The Čech matching condition extracted from s ∈ ker δ⁰: on each overlap U i ⊓ U j the component germs s i and s j restrict to the same germ.

theorem globalSections_matching {X : Type*} [TopologicalSpace X] (𝔘 : FiniteCover X)
    {s : 𝔘.Cochain0} (hs : s ∈ LinearMap.ker 𝔘.cechDelta0) (i j : 𝔘.ι) :
    rawRestrictG (inf_le_right : 𝔘.U i ⊓ 𝔘.U j ≤ 𝔘.U j) (s j)
      = rawRestrictG (inf_le_left : 𝔘.U i ⊓ 𝔘.U j ≤ 𝔘.U i) (s i)

component_mem_iff_all

The per-section core of exact₁₂. For a global 𝒪_{D+P}-section s and a cover-set U i ∋ P, the component on U i lies in 𝒪_D iff *every* component lies in 𝒪_D (equivalently, iff s is a global 𝒪_D-section). Forward is trivial (specialise to i); backward is the genuine sheaf content: at any U j, if P ∉ U j the D and D+P bounds coincide (OmegaDGerm_add_single_eq_…), and if P ∈ U j the order at P transports from U i across the overlap (mem_OmegaDGerm_of_overlap_match).

theorem component_mem_iff_all {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (s : ↥(𝔘.globalSections (D + Finsupp.single P 1))) :
    (s : 𝔘.Cochain0) i ∈ OmegaDGerm D (𝔘.U i)
      ↔ ∀ j, (s : 𝔘.Cochain0) j ∈ OmegaDGerm D (𝔘.U j)

h0ToSky

The skyscraper coefficient arrow f₂ : H⁰(𝒪_{D+P}) → ℂ_P at P, given a cover-set U i ∋ P: restrict the global section to its component germ on U i (in OmegaDGerm (D+P) (U i)), then read its order-(−D(P)−1) principal-part coefficient at P (coeffGermLin). The codomain Skyscraper D P is ℂ. Not surjective in general (its image is the H⁰-cokernel).

noncomputable def h0ToSky {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    ↥(𝔘.globalSections (D + Finsupp.single P 1)) →ₗ[ℂ] 𝔘.Skyscraper D P

h0ToSky_apply

@[simp] theorem h0ToSky_apply {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (s : ↥(𝔘.globalSections (D + Finsupp.single P 1))) :
    𝔘.h0ToSky D P hP s
      = coeffGermLin hP (𝔘.restrictToCoverSet (D + Finsupp.single P 1) i s)

h0ToSky_eq_zero_iff

h0ToSky s = 0 iff the component germ s i on U i lies in OmegaDGerm D (U i) (the order- (−D(P)−1) coefficient at P vanishes — the kernel characterization ker_coeffGermLin).

theorem h0ToSky_eq_zero_iff {i : 𝔘.ι} (hP : P ∈ 𝔘.U i)
    (s : ↥(𝔘.globalSections (D + Finsupp.single P 1))) :
    𝔘.h0ToSky D P hP s = 0 ↔ (s : 𝔘.Cochain0) i ∈ OmegaDGerm D (𝔘.U i)

exact_h0Incl_h0ToSky

Exactness at H⁰(𝒪_{D+P}) (exact₁₂ of the skyscraper LES): range f₁ = ker f₂, i.e. a global section lies in the image of 𝒪_D ↪ 𝒪_{D+P} iff its order-(−D(P)−1) principal-part coefficient at P vanishes. Combines the kernel characterization at the chosen cover-set (h0ToSky_eq_zero_iff ⟶ ker_coeffGermLin) with the sheaf-theoretic propagation (component_mem_iff_all: vanishing at U i forces 𝒪_D-membership at every cover-set).

theorem exact_h0Incl_h0ToSky {i : 𝔘.ι} (hP : P ∈ 𝔘.U i) :
    Function.Exact (𝔘.h0Incl D P) (𝔘.h0ToSky D P hP)

transition_analyticAt

The chart transition chartAt y ∘ (chartAt z).symm is analytic at chartAt z z (for z in the source of chartAt y), on a generic ℂ-charted ω-manifold Y. Compactness-free copy of CechH0.transition_analyticAt.

theorem transition_analyticAt' {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {y z : Y} (hz : z ∈ (chartAt (H := ℂ) y).source) :
    AnalyticAt ℂ ((chartAt (H := ℂ) y) ∘ (chartAt (H := ℂ) z).symm) ((chartAt (H := ℂ) z) z)

analyticAt_chart_change

Chart-invariance of analyticity on a generic ℂ-charted ω-manifold Y (compactness-free copy of CechH0.analyticAt_chart_change): if h read in the chart at y is analytic at the image of z (with z in that chart's source), then h read in its own chart at z is analytic.

theorem analyticAt_chart_change' {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    [IsManifold 𝓘(ℂ) ω Y] {h : Y → ℂ} {y z : Y} (hz : z ∈ (chartAt (H := ℂ) y).source)
    (ha : AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) z)) :
    AnalyticAt ℂ (h ∘ (chartAt (H := ℂ) z).symm) ((chartAt (H := ℂ) z) z)

witnessFn_analyticAt_of_ne

Away from P, the witness (chart − chart P)^k is analytic in ↥W's chart at Q (chart-change of the analytic (chart_P − c)^k via the analytic transition map; needs Q in the P-chart source and Q ≠ P).

theorem witnessFn_analyticAt_of_ne {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {W : Opens X} {P : X} (hP : P ∈ W) (k : ℤ) {Q : W} (hQne : Q ≠ ⟨P, hP⟩)
    (hQsrc : Q ∈ (chartAt (H := ℂ) (⟨P, hP⟩ : W)).source) :
    AnalyticAt ℂ (witnessFn (⟨P, hP⟩ : W) k ∘ (chartAt (H := ℂ) Q).symm)
      ((chartAt (H := ℂ) Q) Q)

ordU_witnessFn_eq_zero_of_ne

Away from P, the witness has order 0 (analytic and nonvanishing at Q).

theorem ordU_witnessFn_eq_zero_of_ne {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {W : Opens X} {P : X} (hP : P ∈ W) (k : ℤ) {Q : W} (hQne : Q ≠ ⟨P, hP⟩)
    (hQsrc : Q ∈ (chartAt (H := ℂ) (⟨P, hP⟩ : W)).source) :
    ordU (witnessFn (⟨P, hP⟩ : W) k) Q = 0

witnessFn_mem_OmegaD_add_single

Witness global membership on a chart-disk (discharges hwit). On a W contained in the source of ↥W's chart at P (hWsrc) where D is supported only at P (hDsupp), the witness section (chart − chart P)^k (with k = −(D P) − 1) lies in OmegaD (D + single P 1) W: at P its order is exactly k = −(D+P)(P) (ordU_witnessFn), and away from P it is analytic and nonvanishing (order 0 = −(D Q) = −(D+P)(Q), ordU_witnessFn_eq_zero_of_ne). This is exactly the geometric input the local-realization surjectivity (coeffGermLin_surjective/localRealizationGermEquiv) needs.

theorem witnessFn_mem_OmegaD_add_single
    (hWsrc : ∀ Q : W, Q ∈ (chartAt (H := ℂ) (⟨P, hP⟩ : W)).source)
    (hDsupp : ∀ Q : W, Q ≠ ⟨P, hP⟩ → D Q.1 = 0) :
    witnessFn (⟨P, hP⟩ : W) (-(D P) - 1) ∈ OmegaD (D + Finsupp.single P 1) W