A machine-checked solution to the Jacobians challenge

20.5. CanonicalForms.CanonicalFormIso🔗

Jacobians.CanonicalForms.CanonicalFormIso — source

lSysModule

The junk-free linear-system module L(D) (= H⁰(X, 𝒪_D)): the linear system with the toFun-germ junk quotiented out, lDim D = finrank ℂ (lSysModule D). (A local copy of the abbreviation in SerreDualityPairing, so this §17.4 layer stays independent of the downstream exists_serreDualityData.)

abbrev lSysModule (D : Divisor X) : Type _

toFun_eq_zero_of_formCoeff_zero

A covector in the (1-dim) cotangent fibre that kills the spanning tangent vector symmL 1 of the trivialization at x is the zero covector — because every tangent vector is a scalar multiple of symmL 1 (mirror of the argument in FormCoeff.exists_localRep_self_ne_zero).

theorem toFun_eq_zero_of_formCoeff_zero (α : MeromorphicOneForm X) {x y : X}
    (hy : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).baseSet)
    (h : α.toFun y ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1) = 0) :
    α.toFun y = 0

formOrderW_eq_top_iff

Intrinsic vanishing characterization. formOrderW α x = ⊤ (the form's germ vanishes at x) iff the *section* α.toFun vanishes on a punctured neighbourhood of x. No chart-coefficient change-of-variables — the chart coefficient is α.toFun paired with the spanning tangent vector.

theorem formOrderW_eq_top_iff (α : MeromorphicOneForm X) (x : X) :
    α.formOrderW x = ⊤ ↔ ∀ᶠ y in 𝓝[≠] x, α.toFun y = 0

formOrderW_ne_top_iff

formOrderW α x ≠ ⊤ (the form's germ is nonzero) iff the section α.toFun is eventually nonzero on a punctured neighbourhood of x.

theorem formOrderW_ne_top_iff (α : MeromorphicOneForm X) (x : X) :
    α.formOrderW x ≠ ⊤ ↔ ∀ᶠ y in 𝓝[≠] x, α.toFun y ≠ 0

formOrderW_ne_top_of_exists

Form identity theorem. If the germ of α is nonzero (formOrderW ≠ ⊤) at even one point, it is nonzero at *every* point. The set {x | formOrderW α x = ⊤} and its complement are both open (via the two intrinsic characterizations above), so on the connected X it is empty. Mirror of MeromorphicFunction.orderW_ne_top_of_exists.

theorem formOrderW_ne_top_of_exists (α : MeromorphicOneForm X)
    (h₀ : ∃ x₀, α.formOrderW x₀ ≠ ⊤) (x : X) : α.formOrderW x ≠ ⊤

CanonicalForm17Data

[ISOLATED ANALYTIC INPUT]. The canonical-form datum of Forster §17.4: a nonzero meromorphic 1-form ω₀ together with its canonical divisor K = div ω₀.

The two fields encode ω₀ ≠ 0 (nontrivial) and K = div ω₀ (order_eq, i.e. the divisor's coefficients are the form's orders). Both are TRUE for ω₀ = df of a nonconstant meromorphic function f (which exists by Riemann–Roch — exists_nonconstant_meromorphic); the finite support of K is the 1-form analog of MeromorphicFunction.div's local finiteness (Jacobians.Abel.orderAtPoint_isolated_at). The remaining §17.4 content built on this datum is purely algebraic.

structure CanonicalForm17Data (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] where

formOrderW_ω₀_ne_top

ω₀'s germ is nonzero at every point (the form identity theorem applied to nontrivial).

theorem formOrderW_ω₀_ne_top (x : X) : data.ω₀.formOrderW x ≠ ⊤

ω₀_eventually_ne_zero

ω₀.toFun is eventually nonzero on a punctured neighbourhood of every point (so the covector ratio α/ω₀ is well-defined as a meromorphic function).

theorem ω₀_eventually_ne_zero (x : X) : ∀ᶠ y in 𝓝[≠] x, data.ω₀.toFun y ≠ 0

covector_ratio_eq

Covector ratio is test-vector-independent. For covectors a b : TangentSpace 𝓘(ℂ) y →L[ℂ] ℂ, the trivialization e = trivializationAt _ _ x with y ∈ e.baseSet, and any v, the ratio a v / b v equals the ratio on the frame vector a (e.symmL 1) / b (e.symmL 1) (the cotangent fibre being 1-dim, every v is a scalar multiple of e.symmL 1, and the scalar cancels).

theorem covector_ratio_eq {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {x y : X} (a b : TangentSpace 𝓘(ℂ) (M := X) y →L[ℂ] ℂ)
    (hy : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).baseSet)
    (v : TangentSpace 𝓘(ℂ) (M := X) y) (hbv0 : b v ≠ 0) :
    a v / b v = a ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1)
      / b ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1)

apply_symmL_ne_zero_of_ne_zero

A nonzero covector on the (1-dim) cotangent fibre is nonzero on the frame vector symmL 1 (contrapositive of MeromorphicOneForm.toFun_eq_zero_of_formCoeff_zero).

theorem apply_symmL_ne_zero_of_ne_zero {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {x y : X}
    (a : TangentSpace 𝓘(ℂ) (M := X) y →L[ℂ] ℂ) (ha : a ≠ 0)
    (hy : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).baseSet) :
    a ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1) ≠ 0

meroFormDiv

The division α/ω₀ as a meromorphic function. Pointwise the intrinsic covector ratio (α/ω₀)(y) := α y v / ω₀ y v (test vector v = symmL 1 in y's own trivialization). It is chart-independent (covector_ratio_eq), with chart coefficient formCoeff α / formCoeff ω₀, hence meromorphic. This is the surjectivity witness of Forster §17.4: α = (α/ω₀)·ω₀.

noncomputable def meroFormDiv (α : MeromorphicOneForm X) : MeromorphicFunction X where

meroFormDiv_comp_chart_eq

The chart pullback of α/ω₀ agrees, on a punctured neighbourhood of chart x x, with the quotient formCoeff α x / formCoeff ω₀ x (the covector-ratio identity of the meromorphic field, extracted for reuse in the order computation).

theorem meroFormDiv_comp_chart_eq (α : MeromorphicOneForm X) (x : X) :
    (data.meroFormDiv α).toFun ∘ (chartAt ℂ x).symm
      =ᶠ[𝓝[≠] ((chartAt ℂ x) x)] formCoeff α.toFun x / formCoeff data.ω₀.toFun x

meroFormDiv_orderW

Order subtractivity of α/ω₀ (Forster §17.4 bookkeeping): orderW (α/ω₀) x = formOrderW α x − formOrderW ω₀ x = formOrderW α x − (K x). From meroFormDiv\_comp\_chart\_eq + meromorphicOrderAt\_div + order\_eq.

theorem meroFormDiv_orderW (α : MeromorphicOneForm X) (x : X) :
    (data.meroFormDiv α).orderW x = α.formOrderW x - (data.K x : WithTop ℤ)

covector_ext_symmL

Covector extensionality on the frame vector. Two covectors on the (1-dim) cotangent fibre at y are equal iff they agree on the spanning frame vector symmL 1 of any trivialization.

theorem covector_ext_symmL {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] {x y : X} (a b : TangentSpace 𝓘(ℂ) (M := X) y →L[ℂ] ℂ)
    (hy : y ∈ (trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).baseSet)
    (h : a ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1)
       = b ((trivializationAt ℂ (TangentSpace 𝓘(ℂ) (M := X)) x).symmL ℂ y 1)) :
    a = b

meroFormSMul_meroFormDiv_apply

The reconstruction identity (α/ω₀)·ω₀ = α where ω₀ ≠ 0. At a point y with ω₀.toFun y ≠ 0, the covector α.toFun y is the scalar (α/ω₀)(y) times ω₀.toFun y (covectors are proportional on the 1-dim fibre), so meroFormSMul (α/ω₀) ω₀ agrees with α there.

theorem meroFormSMul_meroFormDiv_apply (α : MeromorphicOneForm X) {y : X}
    (hy : data.ω₀.toFun y ≠ 0) :
    (meroFormSMul (data.meroFormDiv α) data.ω₀).toFun y = α.toFun y

formOrderW_meroFormSMul_meroFormDiv_sub_top

(α/ω₀)·ω₀ and α have the same class in omegaDModule D: their difference is germ-zero everywhere (they agree on a punctured neighbourhood of every point, where ω₀ ≠ 0).

theorem formOrderW_meroFormSMul_meroFormDiv_sub_top (α : MeromorphicOneForm X) (x : X) :
    (meroFormSMul (data.meroFormDiv α) data.ω₀ - α).formOrderW x = ⊤

formOrderW_meroFormSMul_ω₀

Order law for meroFormSMul · ω₀ (Forster §17.4): formOrderW (f·ω₀) x = orderW f x + (K x) (order additivity formOrderW_meroFormSMul + K = div ω₀).

theorem formOrderW_meroFormSMul_ω₀ (f : MeromorphicFunction X) (x : X) :
    (meroFormSMul f data.ω₀).formOrderW x = f.orderW x + (data.K x : WithTop ℤ)

meroFormSMul_ω₀_mem_omegaD

L(D+K)·ω₀ ⊆ Ω_D (Forster §17.4 well-definedness): if f ∈ L(D+K) then f·ω₀ ∈ Ω_D. Orders add: formOrderW (f·ω₀) = orderW f + K ≥ −(D+K) + K = −D.

theorem meroFormSMul_ω₀_mem_omegaD {D : Divisor X} {f : MeromorphicFunction X}
    (hf : f ∈ linearSystem (X := X) (D + data.K)) :
    meroFormSMul f data.ω₀ ∈ omegaD (X := X) D

omega17Map

The §17.4 map on representatives L(D+K) → omegaDModule D, f ↦ [f·ω₀] (multiply by ω₀, land in Ω_D by meroFormSMul_ω₀_mem_omegaD, project to the junk-free quotient). ℂ-linear.

noncomputable def omega17Map (D : Divisor X) :
    ↥(linearSystem (X := X) (D + data.K)) →ₗ[ℂ] omegaDModule (X := X) D where

omega17Map_mk

@[simp] theorem omega17Map_mk (D : Divisor X) (f : ↥(linearSystem (X := X) (D + data.K))) :
    data.omega17Map D f =
      Submodule.Quotient.mk ⟨meroFormSMul f.1 data.ω₀, data.meroFormSMul_ω₀_mem_omegaD f.2⟩

meroFormSMul_ω₀_formGermZero_iff

f·ω₀ is germ-zero iff f is germ-zero (multiplication by ω₀ ≠ 0 preserves and reflects the germ-junk): formOrderW (f·ω₀) x = orderW f x + K x, and K x ≠ ⊤, so = ⊤ ↔ orderW f x = ⊤.

theorem meroFormSMul_ω₀_formGermZero_iff (f : MeromorphicFunction X) :
    meroFormSMul f data.ω₀ ∈ formGermZeroSubmodule (X := X) ↔ f ∈ germZeroSubmodule (X := X)

ker_omega17Map

The §17.4 map has kernel exactly the germ-junk. ker (omega17Map D) = germZeroSubmodule.submoduleOf. ([f·ω₀] = 0 ↔ f·ω₀ germ-zero ↔ f germ-zero, by meroFormSMul_ω₀_formGermZero_iff.)

theorem ker_omega17Map (D : Divisor X) :
    LinearMap.ker (data.omega17Map D)
      = (germZeroSubmodule (X := X)).submoduleOf (linearSystem (X := X) (D + data.K))

meroFormDiv_mem_linearSystem

α/ω₀ ∈ L(D+K) for α ∈ Ω_D (the surjectivity preimage of §17.4): orders subtract, orderW (α/ω₀) x = formOrderW α x − K x ≥ −D − K = −(D+K).

theorem meroFormDiv_mem_linearSystem {D : Divisor X} {α : MeromorphicOneForm X}
    (hα : α ∈ omegaD (X := X) D) :
    data.meroFormDiv α ∈ linearSystem (X := X) (D + data.K)

omega17Map_surjective

Forster §17.4 surjectivity. omega17Map D is surjective: every class [α] ∈ omegaDModule D is the image of [α/ω₀] (with α/ω₀ ∈ L(D+K)), since (α/ω₀)·ω₀ and α have the same class.

theorem omega17Map_surjective (D : Divisor X) : Function.Surjective (data.omega17Map D)

omega17

The §17.4 map descended to lSysModule (D+K) (the junk-free domain), via liftQ using germZero.submoduleOf ≤ ker (omega17Map D) (in fact equality, ker_omega17Map).

noncomputable def omega17 (D : Divisor X) :
    lSysModule (X := X) (D + data.K) →ₗ[ℂ] omegaDModule (X := X) D

omega17_mk

@[simp] theorem omega17_mk (D : Divisor X) (f : ↥(linearSystem (X := X) (D + data.K))) :
    data.omega17 D (Submodule.Quotient.mk f) = data.omega17Map D f

omega17_injective

omega17 D is injective (Forster §17.4 injectivity): its kernel is ⊥ because ker (omega17Map D) = germZeroSubmodule.submoduleOf (the submodule we quotient by).

theorem omega17_injective (D : Divisor X) : Function.Injective (data.omega17 D)

omega17_surjective

omega17 D is surjective (Forster §17.4 surjectivity), lifted from omega17Map_surjective.

theorem omega17_surjective (D : Divisor X) : Function.Surjective (data.omega17 D)

omega17Equiv

Forster §17.4 — ω₀· : 𝒪_{D+K} ≅ Ω_D. The multiplication-by-ω₀ isomorphism lSysModule (D + K) ≃ₗ[ℂ] omegaDModule D for every divisor D. Injective (mult by ω₀ ≠ 0, kernel = germ-junk) and surjective (the division α/ω₀).

noncomputable def omega17Equiv (D : Divisor X) :
    lSysModule (X := X) (D + data.K) ≃ₗ[ℂ] omegaDModule (X := X) D

lDim_add_K_eq_omegaDim

Forster §17.4 as a dimension equality: lDim (D + K) = omegaDim D (the iso 𝒪_{D+K} ≅ Ω_D preserves finrank).

theorem lDim_add_K_eq_omegaDim (D : Divisor X) :
    lDim (X := X) (D + data.K) = omegaDim (X := X) D

lDim_K_eq_omegaDim_zero

lDim K = omegaDim 0 (Forster §17.4 at D = 0, the iso 𝒪_K ≅ Ω_0). A direct corollary of lDim_add_K_eq_omegaDim at D = 0 (0 + K = K).

theorem lDim_K_eq_omegaDim_zero : lDim (X := X) data.K = omegaDim (X := X) 0

hKgenus

hKgenus — lDim K = genus X (Forster §17.4 at D = 0). Chains the unconditional lDim K = omegaDim 0 with omegaDim 0 = genus X (the Ω_D system's omegaDim_zero_eq_genus_of_le). The two hypotheses are exactly the isolated removable-singularity inputs: finiteness of Ω_0 and the reverse bound omegaDim 0 ≤ genus X (an order-≥ 0 meromorphic 1-form is holomorphic modulo germ-junk). This is the SerreDualityData.hKgenus field.

theorem hKgenus [FiniteDimensional ℂ (omegaDModule (X := X) 0)]
    (hle : omegaDim (X := X) 0 ≤ genus X) :
    lDim (X := X) data.K = genus X