nuPairDual/Miranda Lemma 3.4: the counting step (serre-duality-tails)

Unit: serre-duality-tails (docs/design/serre-duality-tails.md §6 P5, addendum re-basing).

• instFiniteDimensional_H1Tail: H1Tail D is finite-dimensional for EVERY D, via H1Tail.toH1_injective (unconditional, landed) + Finiteness.finiteDimensional_H1 (an injection into a finite-dimensional space) — the orchestrator addendum's re-basing, NOT via the (Serre-circular, out-of-scope) surjectivity of tailToH1.
• h1T/h1T_le_h1: the tail-level h¹, bounded above by the Čech h¹ via the same injection (this ONE inequality is all Lemma 3.4's internal arithmetic needs from the Čech side — no tail-level six-term ledger is required here).
• nuPairDual/two_l_le_h1T_of_injective: the pair-map dimension count.
• exists_mul_functional_eq: MIRANDA LEMMA 3.4.

Finite-dimensionality of H1Tail D, via injection into Cech.H1 D

instance RS.TailDuality.instFiniteDimensional_H1Tail {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : FiniteDimensional ℂ (LaurentTail.H1Tail D)

noncomputable def RS.TailDuality.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) : ℕ

The tail-level h¹.

Equations

• RS.TailDuality.h1T D = Module.finrank ℂ (RS.LaurentTail.H1Tail D)

theorem RS.TailDuality.h1T_le_h1 {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (D : Divisor X) : h1T D ≤ Finiteness.h1 D

h1T D ≤ h1 D (Čech), via the injection H1Tail.toH1 — the ONE fact Lemma 3.4's arithmetic borrows from the Čech side (no tail-level six-term ledger needed).

nuPairDual: the pair map into Dual (H1Tail (A - C))

noncomputable def RS.TailDuality.nuPairDual {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (A C : Divisor X) (φ₁ φ₂ : LaurentTail.T A →ₗ[ℂ] ℂ) (hα₁ : ∀ (g : Mero X), φ₁ ((LaurentTail.alphaL A) g) = 0) (hα₂ : ∀ (g : Mero X), φ₂ ((LaurentTail.alphaL A) g) = 0) : ↥(LinSys C) × ↥(LinSys C) →ₗ[ℂ] Module.Dual ℂ (LaurentTail.H1Tail (A - C))

Miranda's pair map (f₁,f₂) ↦ φ₁∘t∘μ_{f₁} − φ₂∘t∘μ_{f₂}, packaged as a linear map into the dual of H1Tail (A - C) (well-defined: kills range (alphaL (A-C)) by nuL_alpha + the vanishing hypotheses).

Equations

• One or more equations did not get rendered due to their size.

theorem RS.TailDuality.nuPairDual_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (A C : Divisor X) (φ₁ φ₂ : LaurentTail.T A →ₗ[ℂ] ℂ) (hα₁ : ∀ (g : Mero X), φ₁ ((LaurentTail.alphaL A) g) = 0) (hα₂ : ∀ (g : Mero X), φ₂ ((LaurentTail.alphaL A) g) = 0) (f₁ f₂ : ↥(LinSys C)) (τ : LaurentTail.T (A - C)) : ((nuPairDual A C φ₁ φ₂ hα₁ hα₂) (f₁, f₂)) ((LaurentTail.H1Tail.mk (A - C)) τ) = φ₁ (((nuL A C) f₁) τ) - φ₂ (((nuL A C) f₂) τ)

theorem RS.TailDuality.two_l_le_h1T_of_injective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (A C : Divisor X) (φ₁ φ₂ : LaurentTail.T A →ₗ[ℂ] ℂ) (hα₁ : ∀ (g : Mero X), φ₁ ((LaurentTail.alphaL A) g) = 0) (hα₂ : ∀ (g : Mero X), φ₂ ((LaurentTail.alphaL A) g) = 0) (hinj : Function.Injective ⇑(nuPairDual A C φ₁ φ₂ hα₁ hα₂)) : 2 * ↑(l C) ≤ ↑(h1T (A - C))

exists_mul_functional_eq: MIRANDA LEMMA 3.4

theorem RS.TailDuality.exists_mul_functional_eq {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] [ConnectedSpace X] [T1Space X] [DecidableEq X] (A : Divisor X) (φ₁ φ₂ : LaurentTail.T A →ₗ[ℂ] ℂ) (hα₁ : ∀ (g : Mero X), φ₁ ((LaurentTail.alphaL A) g) = 0) (hα₂ : ∀ (g : Mero X), φ₂ ((LaurentTail.alphaL A) g) = 0) (h₁ : φ₁ ≠ 0) (h₂ : φ₂ ≠ 0) : ∃ (C : Divisor X), 0 ≤ C ∧ ∃ (f₁ : ↥(LinSys C)) (f₂ : ↥(LinSys C)), ↑f₁ ≠ 0 ∧ ↑f₂ ≠ 0 ∧ φ₁ ∘ₗ (nuL A C) f₁ = φ₂ ∘ₗ (nuL A C) f₂

MIRANDA LEMMA 3.4: for nonzero functionals on T A vanishing on range (alphaL A), there are C ≥ 0 and nonzero f₁ f₂ ∈ L(C) with φ₁∘t∘μ_{f₁} = φ₂∘t∘μ_{f₂} on T (A - C).