Documentation

LeanPool.JacobianDiffgeo.SerrePairing.Duality

The injectivity core and the generic dimension inequality (serre-duality-cech, §2 D4–D5) #

Unit: serre-duality-cech (docs/design/serre-duality-cech.md §2 D4–D5, §4.3).

Adaptation to the quotient revision. MForm.OmegaSpace/mem_omegaSpace_iff (Jacobian/ CanonicalForms/LinearSystems.lean) dropped the design's Θ = 0 ∨ -D ≤ Θ.divisor disjunction in favor of a single order-wise condition ∀ x, (-(D x) : WithTop ℤ) ≤ Θ.ord x (uniform since Θ = 0 has ord = ⊤ everywhere, ≥ anything for free) — the proof below uses this directly.

Hypothesis deviation (a simplification, not a correction). The design's §4.3 listed [T1Space X] [T2Space X] [CompactSpace X] [ConnectedSpace X] for this file; MForm.OmegaSpace is now instance-free and Module.finrank needs no topology, so both theorems here need only [T1Space X] [ConnectedSpace X] (for MForm.ord_ne_top/Nonempty X) — dropped per CONVENTIONS.md's "drop hypotheses lemmas don't need, when free to do so".

source
theorem RS.MForm.laurentCoeffAt_ord_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Θ : MForm X} {x : X} (h : Θ.ord x ≠ ⊤) :
Θ.laurentCoeffAt x (Θ.ord x).untop₀ ≠ 0

Compat: the leading Laurent coefficient of a meromorphic 1-form at a finite-order point is nonzero (lifted from residue-calculus's laurentCoeffAt_order_ne_zero through a representative; the residue-calculus atom the whole injectivity core rests on).

source
theorem RS.SerrePairing.exists_tail_pair_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {D : Divisor X} {Θ : MForm X} (hΘ : Θ ∈ MForm.OmegaSpace (-D)) (hΘ0 : Θ ≠ 0) :
∃ (τ : Tail X), τ.BoundedBy D ∧ pair Θ τ ≠ 0

D4 (Miranda Thm 3.3's injectivity half / Forster 17.6): a nonzero Θ ∈ Ω(-D) pairs nontrivially against some D-bounded tail — the single-term tail at the leading exponent of Θ at any point, cheap and local.

D5: the generic dimension inequality #

source
theorem RS.SerrePairing.pair_congr_of_toH_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D : Divisor X} {H : Type u_2} [AddCommGroup H] [Module ℂ H] (toH : ↥(TailSpace D) →ₗ[ℂ] H) (hwd : ∀ Θ ∈ MForm.OmegaSpace (-D), ∀ (τ : ↥(TailSpace D)), toH τ = 0 → pair Θ ↑τ = 0) {Θ : MForm X} (hΘ : Θ ∈ MForm.OmegaSpace (-D)) {τ σ : ↥(TailSpace D)} (h : toH τ = toH σ) :
pair Θ ↑τ = pair Θ ↑σ

pair Θ is invariant on the fibres of toH (a repackaging of hwd: since pair Θ vanishes on ker toH, it agrees on any two tails with the same toH-image). The engine behind resDual below — the design's risk-3 fallback (docs/design/serre-duality-cech.md §7): instead of Submodule.liftQ/LinearMap.quotKerEquivOfSurjective (which stacks a further quotient on top of the already-reducible abbrev Tail X, and was found to elaborate very slowly / time out), we work directly with a section Function.surjInv of toH and this congruence lemma.

A genuine mathlib-instance gap found and worked around: ↥(TailSpace D) has no findable AddCommGroup/Sub/Neg instance at this pin — confirmed by direct experiment that AddSubgroupClass (Submodule ℂ (Tail X)) (Tail X) fails to synthesize (Tail X's doubly-nested Finsupp carrier X →₀ (ℤ →₀ ℂ) defeats it), even though Tail X itself (unwrapped) has a perfectly good AddCommGroup/Sub, and the SEMIRING-level Submodule.add_mem/smul_mem (not neg_mem/sub_mem, which need Ring/AddCommGroup) resolve fine. So the proof below builds "τ - σ" as τ + (-1 : ℂ) • σ (+/• on ↥(TailSpace D), both confirmed working), never invoking Sub/Neg on the submodule-subtype itself.

source
noncomputable def RS.SerrePairing.resDual {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D : Divisor X} {H : Type u_2} [AddCommGroup H] [Module ℂ H] (toH : ↥(TailSpace D) →ₗ[ℂ] H) (hwd : ∀ Θ ∈ MForm.OmegaSpace (-D), ∀ (τ : ↥(TailSpace D)), toH τ = 0 → pair Θ ↑τ = 0) (hsurj : Function.Surjective ⇑toH) (Θ : ↥(MForm.OmegaSpace (-D))) :
Module.Dual ℂ H

The functional on H induced by a class Θ ∈ Ω(-D), via a chosen section Function.surjInv of toH (internal plumbing for finrank_omegaSpace_le).

Equations
Instances For
    source
    theorem RS.SerrePairing.resDual_apply_toH {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D : Divisor X} {H : Type u_2} [AddCommGroup H] [Module ℂ H] (toH : ↥(TailSpace D) →ₗ[ℂ] H) (hwd : ∀ Θ ∈ MForm.OmegaSpace (-D), ∀ (τ : ↥(TailSpace D)), toH τ = 0 → pair Θ ↑τ = 0) (hsurj : Function.Surjective ⇑toH) (Θ : ↥(MForm.OmegaSpace (-D))) (τ : ↥(TailSpace D)) :
    (resDual toH hwd hsurj Θ) (toH τ) = pair ↑Θ ↑τ
    source
    theorem RS.SerrePairing.finrank_omegaSpace_le {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [T1Space X] [ConnectedSpace X] {D : Divisor X} {H : Type u_2} [AddCommGroup H] [Module ℂ H] [FiniteDimensional ℂ H] (toH : ↥(TailSpace D) →ₗ[ℂ] H) (hsurj : Function.Surjective ⇑toH) (hwd : ∀ Θ ∈ MForm.OmegaSpace (-D), ∀ (τ : ↥(TailSpace D)), toH τ = 0 → pair Θ ↑τ = 0) :
    Module.finrank ℂ ↥(MForm.OmegaSpace (-D)) ≤ Module.finrank ℂ H

    D5 (the interface #26 discharges, generic in the target H): given a finite-dimensional H and a surjective linear map toH from D-bounded tails such that pair Θ vanishes on ker toH for every Θ ∈ Ω(-D), the pairing descends to an injective map into Dual H, hence i(-D) ≤ finrank H. Pure linear algebra once the two hypotheses are supplied — proved here in full, no dependency on laurent-tails or residue-theorem's own content.