A machine-checked solution to the Jacobians challenge

14.5. Cech.CechH0🔗

Jacobians.Cech.CechH0 — source

ordU_val_eq_orderW

Order bridge. The order of F restricted to the open submanifold ↥U (in ↥U's chart) equals the global order orderW F at the corresponding point.

theorem ordU_val_eq_orderW [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {U : Opens X} (F : MeromorphicFunction X) (u : U) :
    ordU (F.toFun ∘ Subtype.val) u = F.orderW u.1

isMeromorphic_val

F : X → ℂ meromorphic on X restricts to a meromorphic function on the open submanifold ↥U.

theorem isMeromorphic_val [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {U : Opens X} (F : MeromorphicFunction X) :
    IsMeromorphic (U : Type _) (F.toFun ∘ Subtype.val)

eventually_comp_chart_iff

Chart-transport of an eventually-property across 𝓝[≠], for *any* ℂ-charted space Y (the repo's eventually_comp_chart_iff carries spurious CompactSpace/ConnectedSpace; the open submanifold ↥U has neither). Proof copied verbatim — uses only the chart's local-homeo structure.

theorem eventually_comp_chart_iff' {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    (g : Y → ℂ) (y : Y) (P : ℂ → Prop) :
    (∀ᶠ w in 𝓝[≠] ((chartAt (H := ℂ) y) y), P ((g ∘ (chartAt (H := ℂ) y).symm) w))
      ↔ ∀ᶠ z in 𝓝[≠] y, P (g z)

ordU_eq_top_iff

ordU g u = ⊤ iff g vanishes throughout a punctured neighbourhood of u on ↥U.

theorem ordU_eq_top_iff [ChartedSpace ℂ X]
    {U : Opens X} (g : U → ℂ) (u : U) :
    ordU g u = ⊤ ↔ ∀ᶠ z in 𝓝[≠] u, g z = 0

toGerm_eq_zero_iff

The germ-class of g is 0 iff g vanishes near every point (punctured) — i.e. g is germ-zero junk. This is the codiscrete ⟺ ∀ 𝓝[≠] bridge (here on T = univ, so it needs no meromorphy).

theorem toGerm_eq_zero_iff {U : Opens X} (g : U → ℂ) :
    toGerm U g = 0 ↔ ∀ u : U, ∀ᶠ z in 𝓝[≠] u, g z = 0

toGerm_eq_iff

Two germ-classes are equal iff their representatives agree off a discrete set near every point. The two-function form of toGerm_eq_zero_iff (same codiscrete ⟺ ∀ 𝓝[≠] bridge).

theorem toGerm_eq_iff {U : Opens X} (a b : U → ℂ) :
    toGerm U a = toGerm U b ↔ ∀ u : U, a =ᶠ[𝓝[≠] u] b

Gext

Extend a section on the open submanifold ↥U by 0 to a function on the whole space X.

noncomputable def Gext {U : Opens X} (g : U → ℂ) : X → ℂ

Gext_apply_mem

theorem Gext_apply_mem {U : Opens X} (g : U → ℂ) {x : X} (hx : x ∈ U) :
    Gext g x = g ⟨x, hx⟩

Gext_chart_bridge

The base point and chart-pullback agree between ↥U's chart at ⟨y⟩ and X's chart at y for y ∈ U: both are subtypeRestrs of the *same* ambient chart chartAt ℂ y (Opens.chartAt_eq), and Gext g agrees with g near y (the point and its neighbours lie in U). The Gext analogue of incl_chart_aux.

theorem Gext_chart_bridge [ChartedSpace ℂ X]
    {U : Opens X} (g : U → ℂ) {y : X} (hy : y ∈ U) :
    (chartAt (H := ℂ) (⟨y, hy⟩ : U)) ⟨y, hy⟩ = (chartAt (H := ℂ) y) y ∧
    (g ∘ (chartAt (H := ℂ) (⟨y, hy⟩ : U)).symm) =ᶠ[𝓝 ((chartAt (H := ℂ) y) y)]
      (Gext g ∘ (chartAt (H := ℂ) y).symm)

Gext_meromorphicAt

Gext g is meromorphic at y ∈ U (in X's chart), given g meromorphic on ↥U.

theorem Gext_meromorphicAt [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {U : Opens X} {g : U → ℂ} (hg : IsMeromorphic (U : Type _) g)
    {y : X} (hy : y ∈ U) :
    MeromorphicAt (Gext g ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y)

ordU_eq_orderAt_Gext

The intrinsic order on ↥U (ordU g) equals the order of Gext g read in X's chart.

theorem ordU_eq_orderAt_Gext [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {U : Opens X} (g : U → ℂ) {y : X} (hy : y ∈ U) :
    ordU g ⟨y, hy⟩ =
      meromorphicOrderAt (Gext g ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y)

nfX

The "normal form at y" predicate intrinsic to X: h read in X's chart at y has meromorphic normal form at the chart centre.

def nfX [ChartedSpace ℂ X] (h : X → ℂ) (y : X) : Prop

eventually_nhdsNE_of_subtype

Transport a punctured-neighbourhood property from the open submanifold ↥V to the ambient X: since ↥V ↪ X is an open embedding and V ∈ 𝓝 x, a 𝓝[≠] ⟨x⟩-statement on ↥V becomes the corresponding 𝓝[≠] x-statement on X. (Subtype.val maps 𝓝[≠] ⟨x⟩ to 𝓝[V\{x}] x = 𝓝[≠] x.)

theorem eventually_nhdsNE_of_subtype {V : Opens X} {x : X} (hx : x ∈ V) (P : X → Prop)
    (h : ∀ᶠ w in 𝓝[≠] (⟨x, hx⟩ : V), P w.1) :
    ∀ᶠ z in 𝓝[≠] x, P z

Gext_overlap_eventuallyEq

Overlap agreement. If two representatives' germs match after restriction to the overlap (the Čech matching condition, via rawRestrictG), their extensions-by-zero Gext agree off a discrete set near every overlap point. This is what makes the per-point normal forms glue *honestly*.

theorem Gext_overlap_eventuallyEq [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {U V : Opens X} (gU : U → ℂ) (gV : V → ℂ)
    (hmatch : rawRestrictG (inf_le_right : U ⊓ V ≤ V) (toGerm V gV)
      = rawRestrictG (inf_le_left : U ⊓ V ≤ U) (toGerm U gU))
    {x : X} (hxU : x ∈ U) (hxV : x ∈ V) :
    Gext gU =ᶠ[𝓝[≠] x] Gext gV

eventuallyEq_comp_chart

Transport an =ᶠ[𝓝[≠]] from X to X's chart at x (precompose with chartAt x's inverse).

theorem eventuallyEq_comp_chart [ChartedSpace ℂ X]
    {a b : X → ℂ} {x : X} (h : a =ᶠ[𝓝[≠] x] b) :
    (a ∘ (chartAt (H := ℂ) x).symm) =ᶠ[𝓝[≠] ((chartAt (H := ℂ) x) x)]
      (b ∘ (chartAt (H := ℂ) x).symm)

toMeromorphicNFAt_chart_val_congr

The normal-form *value* at the chart centre depends only on the germ: if a and b agree off a discrete set near x (and a is meromorphic in the chart), their per-point normal forms (read in X's chart at x) take equal value at the chart centre. The MeromorphicNFAt local-identity theorem upgrades the punctured-neighbourhood agreement to a full-neighbourhood one.

theorem toMeromorphicNFAt_chart_val_congr [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {a b : X → ℂ} {x : X} (h : a =ᶠ[𝓝[≠] x] b)
    (hma : MeromorphicAt (a ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)) :
    toMeromorphicNFAt (a ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)
        ((chartAt (H := ℂ) x) x)
      = toMeromorphicNFAt (b ∘ (chartAt (H := ℂ) x).symm) ((chartAt (H := ℂ) x) x)
        ((chartAt (H := ℂ) x) x)

transition_analyticAt

The chart transition chartAt y ∘ (chartAt z).symm is analytic at chartAt z z (for z in the source of chartAt y): chart and inverse-chart are C^ω (contMDiffOn_chart), and C^ω = analytic (ContDiffAt.analyticAt) since the model 𝓘(ℂ) is the identity.

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

eventually_subtype_of_nhdsNE

The reverse of eventually_nhdsNE_of_subtype: pull a punctured-neighbourhood property on X back to the open submanifold ↥V (precompose with Subtype.val, which is continuous and injective so tends 𝓝[≠] u → 𝓝[≠] u.1).

theorem eventually_subtype_of_nhdsNE {V : Opens X} {u : V} (P : X → Prop)
    (h : ∀ᶠ z in 𝓝[≠] u.1, P z) : ∀ᶠ w : V in 𝓝[≠] u, P w.1

analyticAt_chart_change

Chart-invariance of analyticity. 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. Composes with the analytic transition map (transition_analyticAt).

theorem analyticAt_chart_change [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {h : X → ℂ} {y z : X} (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)

cechRestrict

Restrict a global meromorphic function to the cover's germ-class 0-cochains: F ↦ (i ↦ [F|_{U i}]). ℂ-linear (depends only on the cover, not on D).

noncomputable def cechRestrict [ChartedSpace ℂ X] :
    MeromorphicFunction X →ₗ[ℂ] 𝔘.Cochain0 where

cechRestrict_apply

@[simp] theorem cechRestrict_apply [ChartedSpace ℂ X]
    (F : MeromorphicFunction X) (i : 𝔘.ι) :
    𝔘.cechRestrict F i = toGerm (𝔘.U i) (F.toFun ∘ Subtype.val)

cechRestrict_mem_globalSections

The restriction of F ∈ L(D) is a global matching 𝒪_D-section: each component is an 𝒪_D-germ (the order bridge ordU = orderW ≥ −D), and the components match on overlaps automatically (both restrict the *same* F).

theorem cechRestrict_mem_globalSections [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {F : MeromorphicFunction X}
    (hF : F ∈ linearSystem D) : 𝔘.cechRestrict F ∈ 𝔘.globalSections D

cechRestrictL

The forward map Φ : L(D) →ₗ globalSections D (domain/codomain restriction of cechRestrict).

noncomputable def cechRestrictL [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] :
    linearSystem (X := X) D →ₗ[ℂ] ↥(𝔘.globalSections D)

cechRestrictL_coe

@[simp] theorem cechRestrictL_coe [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (F : linearSystem (X := X) D) :
    (𝔘.cechRestrictL D F : 𝔘.Cochain0) = 𝔘.cechRestrict (F : MeromorphicFunction X)

cechRestrict_eq_zero_iff

The restriction of F is the zero cochain iff F is germ-zero junk everywhere (orderW ≡ ⊤). Uses the order bridge (ordU = orderW), the germ-zero bridge, and that the U i cover X.

theorem cechRestrict_eq_zero_iff [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (F : MeromorphicFunction X) :
    𝔘.cechRestrict F = 0 ↔ ∀ x, F.orderW x = ⊤

ker_cechRestrictL

The kernel of the descended forward map is exactly the germ-zero junk: Φ descends to an *injective* map L(D) ⧸ germZero ↪ H⁰.

theorem ker_cechRestrictL [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    :
    LinearMap.ker (𝔘.cechRestrictL D) = (germZeroSubmodule).submoduleOf (linearSystem D)

gluedFun

The per-point glued function: at x, the meromorphic *normal-form* value of the local member G (idx x) read in X's chart at x.

noncomputable def gluedFun [ChartedSpace ℂ X] (G : 𝔘.ι → X → ℂ) (idx : X → 𝔘.ι) : X → ℂ

nfX_Gext_codiscrete

NF-codiscreteness on X. Near every y ∈ U i, the extension Gext g is in normal form (nfX, intrinsic to X's per-point charts) off a discrete set: Gext g is meromorphic at y, so analytic at codiscretely-many nearby chart points, and analyticity is chart-invariant (analyticAt_chart_change), giving nfX at the point's own chart.

theorem nfX_Gext_codiscrete [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    {i : 𝔘.ι} {g : 𝔘.U i → ℂ} (hg : IsMeromorphic (𝔘.U i : Type _) g)
    {y : X} (hy : y ∈ 𝔘.U i) :
    ∀ᶠ z in 𝓝[≠] y, nfX (Gext g) z

gluedFun_eventuallyEq

Central gluing property. The glued function agrees off a discrete set near every point with the local family member G i whose patch U i contains that point. Hence (downstream) gluedFun is meromorphic, satisfies the order bound, and restricts to the prescribed germ on each U i.

Needs: every point lies in U (idx ·) (hidx); each G i meromorphic on U i (hmer); the family agrees off a discrete set on overlaps (hoverlap); and G i is normal-form-codiscrete near U i (hnf). The proof: on the 𝓝[≠] y set where z ∈ U i and G i is nfX at z, idx-independence (toMeromorphicNFAt_chart_val_congr + hoverlap) rewrites gluedFun z to the normal form of G i, which (being already normal form) equals G i z (toMeromorphicNFAt_eq_self).

theorem gluedFun_eventuallyEq [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (G : 𝔘.ι → X → ℂ) (idx : X → 𝔘.ι)
    (hidx : ∀ x, x ∈ 𝔘.U (idx x))
    (hmer : ∀ i, ∀ y, y ∈ 𝔘.U i →
      MeromorphicAt (G i ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) y))
    (hoverlap : ∀ i j, ∀ x, x ∈ 𝔘.U i → x ∈ 𝔘.U j → G i =ᶠ[𝓝[≠] x] G j)
    (hnf : ∀ i, ∀ y, y ∈ 𝔘.U i → ∀ᶠ z in 𝓝[≠] y, nfX (G i) z)
    {y : X} {i : 𝔘.ι} (hy : y ∈ 𝔘.U i) :
    𝔘.gluedFun G idx =ᶠ[𝓝[≠] y] G i

cechRestrictL_surjective

Gluing. Every global matching 𝒪_D-section over the cover glues to a single global meromorphic function in L(D).

CONSTRUCTION (rigidified normal-form gluing; the naive pointwise patch x ↦ g_{idx x} x is *not* meromorphic at cover-boundary points because the per-overlap disagreement set is only codiscrete *within* the overlap). Extract honest representatives g i ∈ OmegaD D (U i) with [g i] = f i (choice on OmegaDGerm = map toGerm). Extend each by 0 to Gext i : X → ℂ. Define

F.toFun x := toMeromorphicNFAt (Gext (idx x) ∘ (chartAt ℂ x).symm) (chartAt ℂ x x) (chartAt ℂ x x)

(the per-point normal-form value; idx x any index with x ∈ U i).

  • idx-independent: the nf value at x depends only on the germ at x; the matching gives Gext i =ᶠ[𝓝[≠] x] Gext j on overlaps, so (read in the shared chart chartAt ℂ x) the nf values agree by NF-uniqueness (MeromorphicNFAt.eventuallyEq_nhdsNE_iff_eventuallyEq_nhds).

  • F =ᶠ[𝓝[≠] y] Gext i for y ∈ U i: the normal form repairs only a *codiscrete* set (analyticAt_mem_codiscreteWithin; toMeromorphicNFAt = id on nf-points, eq_nhdsNE_toMeromorphicNFAt), so F and Gext i agree off a discrete set ⟹ F meromorphic at y and (order bridge ordU = orderW) orderW F ≥ −D ⟹ F ∈ L(D); and [F|_{U i}] = [g i] = f i.

theorem cechRestrictL_surjective [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    : Function.Surjective (𝔘.cechRestrictL D)

globalSectionsEquivQuot

H⁰(𝔘, 𝒪_D) ≅ L(D) ⧸ germZero as ℂ-modules (first isomorphism theorem + ker = germZero).

noncomputable def globalSectionsEquivQuot [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    (linearSystem (X := X) D ⧸ (germZeroSubmodule (X := X)).submoduleOf (linearSystem D))
      ≃ₗ[ℂ] ↥(𝔘.globalSections D)

h0Dim_eq_lDim

The bridge leaf h⁰(𝔘, 𝒪_D) = l(D) — Čech global sections agree with the linear system.

theorem h0Dim_eq_lDim [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) : 𝔘.h0Dim D = lDim D