Documentation

LeanPool.JacobianDiffgeo.TailDuality.Duality

Miranda Lemma 3.6, the surjectivity endgame, and Serre duality (serre-duality-tails) #

Unit: serre-duality-tails (docs/design/serre-duality-tails.md §6 P6/P7, orchestrator addendum 2026-07-08 re-basing).

Update (chiT-ledger closure pass): DELIVERED, in Jacobian/TailDuality/ChiLedger.lean (not in this file, to keep this file's own scope unchanged) — chiT_eq_chiT_zero_add_degree/ chiT_single_add, via exactly the sketch recorded here: windowConnectT := H1Tail.mk D ∘ₗ windowToT D D' h (Cech's Window D D'/windowMap/windowToT, Jacobian/Cech/Window.lean, Jacobian/LaurentTail/TailSpace.lean) plus a NEW descent H1TailIncl of truncT, both exactness facts proved elementarily (no Čech H1/cochain machinery: H1Tail D being a literal coker of alphaL D, not a colimit, makes both a DFinsupp/Submodule bookkeeping argument). See that file's own docstring for the full account. riemann-roch (#28) now consumes chiT's own ledger directly.

Miranda Lemma 3.6 (the order downgrade) #

source
theorem RS.TailDuality.mem_omegaSpace_of_vanishing_ker_trunc {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) {θ : MForm X} (hθ : θ ∈ MForm.OmegaSpace (-D₁)) (hker : ∀ (τ : LaurentTail.T D₁), (truncT h) τ = 0 → (pairT θ hθ) τ = 0) :
θ ∈ MForm.OmegaSpace (-D₂)

MIRANDA LEMMA 3.6.

The surjectivity endgame (Miranda Thm 3.3, hard half) #

source
theorem RS.TailDuality.pairT_eq_of_eq {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] {D : Divisor X} {θ₁ θ₂ : MForm X} (hEq : θ₁ = θ₂) (h1 : θ₁ ∈ MForm.OmegaSpace (-D)) (h2 : θ₂ ∈ MForm.OmegaSpace (-D)) :
pairT θ₁ h1 = pairT θ₂ h2

pairT only depends on its MForm argument up to equality (proof-irrelevant in the membership proof) — avoids a dependent rw/▸ inside pairT's own proof argument, which rw cannot abstract into a well-typed motive.

source
theorem RS.TailDuality.exists_pairT_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) (φ : LaurentTail.T D →ₗ[ℂ] ℂ) (hα : ∀ (f : Mero X), φ ((LaurentTail.alphaL D) f) = 0) :
∃ (θ : MForm X) (hθ : θ ∈ MForm.OmegaSpace (-D)), pairT θ hθ = φ

MIRANDA THM 3.3, surjectivity half, functional form on T D.

source
theorem RS.TailDuality.resMap_surjective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) :
Function.Surjective ⇑(resMap D)
source
noncomputable def RS.TailDuality.resEquiv {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) :
↥(MForm.OmegaSpace (-D)) ≃ₗ[ℂ] Module.Dual ℂ (LaurentTail.H1Tail D)

MIRANDA THM 3.3: Res is a linear isomorphism Ω(-D) ≅ Dual(H1Tail D).

Equations
Instances For

    The export bank (orchestrator addendum: re-based against the tail h¹) #

    source
    theorem RS.TailDuality.i_neg_eq_h1T {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) :
    MForm.i (-D) = h1T D

    THE frozen obligation, re-based (serre-duality-cech D6's exact shape, at the TAIL h¹; RS.MForm.i is the exact name for the design's RS.i — see the file-end note).

    source
    theorem RS.TailDuality.l_sub_eq_h1T {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {ω₀ : MForm X} (h₀ : ω₀ ≠ 0) (D : Divisor X) :
    l (canonicalDivisorOf ω₀ - D) = h1T D

    Serre duality in the l(K-D) shape riemann-roch consumes.

    source
    theorem RS.TailDuality.h1T_zero_eq_l_K {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {ω₀ : MForm X} (h₀ : ω₀ ≠ 0) :
    h1T 0 = l (canonicalDivisorOf ω₀)
    source
    theorem RS.TailDuality.h1T_zero_eq_genus {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] :
    h1T 0 = genus X
    source
    theorem RS.TailDuality.h1T_canonical {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] {ω₀ : MForm X} (h₀ : ω₀ ≠ 0) :
    h1T (canonicalDivisorOf ω₀) = 1

    chiT (definition only — see the file docstring for the additivity gap) #

    source
    noncomputable def RS.TailDuality.chiT {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) :
    ℤ

    The tail-level χ. Additivity (chiT D = chiT 0 + deg D) is NOT delivered — see the file docstring.

    Equations
    Instances For