pairT/resMap: the residue pairing on the germ model (serre-duality-tails)

Unit: serre-duality-tails (docs/design/serre-duality-tails.md §3 D2, §5.2, §6 P2–P4).

Adaptation (mirrors SerrePairing/Pairing.lean's own note): MForm X is a quotient of MFormData X exposing only the LIFTED reading maps (ord/resAt/laurentCoeffAt), no raw coeffAt. So the pairing is built at the MFormData level first (pairAtData, honestly using θ.coeffAt p), then descended to MForm X via Quotient.liftOn (congruence: MFormData.Eqv, i.e. 𝓝[≠]-agreement of coeffAt at every center — exactly what the residue functional needs). All PUBLIC lemmas are stated at the MForm/laurentCoeffAt level.

• readAt: chart-read of a manifold germ as a punctured planar germ at the chart center.
• pairAtData/pairAt/pairTailAt/pairT: Miranda's Res_ω on T[D].
• pairT_trunc/pairT_mulInto/pairT_alpha: the compatibilities Miranda's diagram needs (pairT_alpha is the only citation of the residue theorem; the ℳ(X)-module laws MForm.ord_smul_mero/divisor_smul_mero/mul_smul are ALREADY built unconditionally by canonical-forms, so no separate D5/D6 "ord kit"/"congruence" layer is needed here).
• pairAt_tailGerm_order_ne_zero/pairT_ne_zero: Miranda Thm 3.3's injectivity half.
• resMap/resMap_injective: the induced map Ω(-D) →ₗ Dual(H1Tail D).

readAt: chart-read of a manifold germ as a punctured planar germ

noncomputable def RS.TailDuality.readAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) : MeroGermOn X (chartAt ℂ p).source →ₗ[ℂ] (nhdsWithin (↑(chartAt ℂ p) p) {↑(chartAt ℂ p) p}ᶜ).Germ ℂ

Chart-read of a manifold germ as a punctured planar germ at the chart center.

Equations

• RS.TailDuality.readAt p = { toFun := fun (ψ : RS.MeroGermOn X (chartAt ℂ p).source) => (↑ψ).liftOn (fun (f : X → ℂ) => ↑(f ∘ ↑(chartAt ℂ p).symm)) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.TailDuality.readAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) {f : X → ℂ} (hf : MeromorphicOnX f (chartAt ℂ p).source) : (readAt p) (MeroGermOn.mk f hf) = ↑(f ∘ ↑(chartAt ℂ p).symm)

theorem RS.TailDuality.meromorphicGerm_readAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (readAt p) ψ ∈ meromorphicGermsAt (↑(chartAt ℂ p) p)

theorem RS.TailDuality.readAt_mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (ψ ψ' : MeroGermOn X (chartAt ℂ p).source) : (readAt p) (ψ * ψ') = (readAt p) ψ * (readAt p) ψ'

theorem RS.TailDuality.readAt_tailGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (p : X) (m : ℤ) : (readAt p) (Cech.tailGerm p m) = ↑fun (z : ℂ) => (z - ↑(chartAt ℂ p) p) ^ m

pairAtData/pairAt: the per-point residue pairing

noncomputable def RS.TailDuality.pairAtData {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (p : X) : MeroGermOn X (chartAt ℂ p).source →ₗ[ℂ] ℂ

The per-point residue pairing at the MFormData (raw) level, built directly through resAt on representatives (well-definedness: resAt_congr + the codiscrete→𝓝[≠] chart transport, the same bridge readAt uses).

Equations

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

theorem RS.TailDuality.pairAtData_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (p : X) {f : X → ℂ} (hf : MeromorphicOnX f (chartAt ℂ p).source) : (pairAtData θ p) (MeroGermOn.mk f hf) = resAt (fun (z : ℂ) => f (↑(chartAt ℂ p).symm z) * θ.coeffAt p z) (↑(chartAt ℂ p) p)

theorem RS.TailDuality.pairAtData_congr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ θ' : MFormData X} (p : X) (h : θ.coeffAt p =ᶠ[nhdsWithin (↑(chartAt ℂ p) p) {↑(chartAt ℂ p) p}ᶜ] θ'.coeffAt p) : pairAtData θ p = pairAtData θ' p

noncomputable def RS.TailDuality.pairAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (p : X) : MeroGermOn X (chartAt ℂ p).source →ₗ[ℂ] ℂ

The residue pairing, Res_ω (Miranda VI.3), on classes.

Equations

• RS.TailDuality.pairAt θ p = Quotient.liftOn θ (fun (x : RS.MFormData X) => RS.TailDuality.pairAtData x p) ⋯

theorem RS.TailDuality.pairAt_apply_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MFormData X) (p : X) : pairAt (MForm.mk θ) p = pairAtData θ p

theorem RS.TailDuality.pairAt_tailGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (p : X) (m : ℤ) : (pairAt θ p) (Cech.tailGerm p m) = θ.laurentCoeffAt p (-1 - m)

theorem RS.TailDuality.pairAt_eq_zero_of_mem_ordGe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ : MForm X} {D : Divisor X} {p : X} (hθ : θ ∈ MForm.OmegaSpace (-D)) {ψ : MeroGermOn X (chartAt ℂ p).source} (hψ : ψ ∈ Cech.ordGe p (-D p)) : (pairAt θ p) ψ = 0

Linearity of pairAt in θ (unconditional; feeds resMap's map_add'/map_smul')

theorem RS.TailDuality.pairAt_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MForm X) (p : X) : pairAt (θ + η) p = pairAt θ p + pairAt η p

theorem RS.TailDuality.pairAt_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (θ : MForm X) (p : X) : pairAt (c • θ) p = c • pairAt θ p

theorem RS.TailDuality.pairAt_sub {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MForm X) (p : X) : pairAt (θ - η) p = pairAt θ p - pairAt η p

pairAt_tailGerm_order_ne_zero: the shared core of injectivity and Lemma 3.6

theorem RS.TailDuality.pairAt_tailGerm_order_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {θ : MForm X} {p : X} (hne : θ.ord p ≠ ⊤) : (pairAt θ p) (Cech.tailGerm p (-1 - (θ.ord p).untop₀)) ≠ 0

pairT: assembling pairAt over the tail T D

noncomputable def RS.TailDuality.pairTailAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) {D : Divisor X} (hθ : θ ∈ MForm.OmegaSpace (-D)) (p : X) : LaurentTail.TailAt p D →ₗ[ℂ] ℂ

pairAt θ p descended to the tail fibre TailAt p D, for θ ∈ Ω(-D).

Equations

• RS.TailDuality.pairTailAt θ hθ p = (RS.Cech.ordGe p (-D p)).liftQ (RS.TailDuality.pairAt θ p) ⋯

theorem RS.TailDuality.pairTailAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) {D : Divisor X} (hθ : θ ∈ MForm.OmegaSpace (-D)) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (pairTailAt θ hθ p) ((LaurentTail.TailAt.mk p D) ψ) = (pairAt θ p) ψ

noncomputable def RS.TailDuality.pairT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] (θ : MForm X) {D : Divisor X} (hθ : θ ∈ MForm.OmegaSpace (-D)) : LaurentTail.T D →ₗ[ℂ] ℂ

Miranda's Res_ω on T[D] (§3 D2).

Equations

• RS.TailDuality.pairT θ hθ = (DFinsupp.lsum ℕ) (RS.TailDuality.pairTailAt θ hθ)

@[simp]

theorem RS.TailDuality.pairT_singleT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] (θ : MForm X) {D : Divisor X} (hθ : θ ∈ MForm.OmegaSpace (-D)) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (pairT θ hθ) (singleT p D ψ) = (pairAt θ p) ψ

theorem RS.TailDuality.pairT_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] (D : Divisor X) : pairT 0 ⋯ = 0

Monotonicity of Ω(-D) in D, and the multiplication mover

theorem RS.TailDuality.omegaSpace_anti {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) {θ : MForm X} (hθ₂ : θ ∈ MForm.OmegaSpace (-D₂)) : θ ∈ MForm.OmegaSpace (-D₁)

theorem RS.TailDuality.smul_mem_omegaSpace {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {f : Mero X} {θ : MForm X} {E F : Divisor X} (hf : ∀ (p : X), ↑(F p) ≤ MeroGermOn.ord f p) (hθ : θ ∈ MForm.OmegaSpace (-E)) : f • θ ∈ MForm.OmegaSpace (-(E + F))

theorem RS.TailDuality.pairT_trunc {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (θ : MForm X) (hθ₂ : θ ∈ MForm.OmegaSpace (-D₂)) : pairT θ hθ₂ ∘ₗ truncT h = pairT θ ⋯

pairT_mulInto: Miranda's Res_ω∘μ_f = Res_{fω}

theorem RS.TailDuality.mulInto_singleT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (f : Mero X) {D E : Divisor X} (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) (p : X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (mulInto f hf) (singleT p D ψ) = singleT p E ((MeroGermOn.restrict ⋯) f * ψ)

theorem RS.TailDuality.pairAt_mulInto {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (f : Mero X) (p : X) (θ : MForm X) (ψ : MeroGermOn X (chartAt ℂ p).source) : (pairAt θ p) ((MeroGermOn.restrict ⋯) f * ψ) = (pairAt (f • θ) p) ψ

Miranda's Res_ω∘μ_f = Res_{fω}, at the raw germ level.

theorem RS.TailDuality.pairT_mulInto {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] {D E : Divisor X} (f : Mero X) (hf : ∀ (p : X), ↑(D p - E p) ≤ MeroGermOn.ord f p) (θ : MForm X) (hθ : θ ∈ MForm.OmegaSpace (-E)) (hfθ : f • θ ∈ MForm.OmegaSpace (-D)) : pairT θ hθ ∘ₗ mulInto f hf = pairT (f • θ) hfθ

pairT_alpha: the residue theorem's ONLY citation

theorem RS.TailDuality.pairAt_one {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (p : X) : (pairAt θ p) 1 = θ.resAt p

theorem RS.TailDuality.alpha_eq_sum_singleT {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [CompactSpace X] [ConnectedSpace X] [T1Space X] (D : Divisor X) (f : Mero X) : LaurentTail.alpha D f = ∑ p ∈ LaurentTail.alphaFinset D f, singleT p D ((MeroGermOn.restrict ⋯) f)

theorem RS.TailDuality.pairT_alpha {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [CompactSpace X] [ConnectedSpace X] [T1Space X] {D : Divisor X} (θ : MForm X) (hθ : θ ∈ MForm.OmegaSpace (-D)) (f : Mero X) : (pairT θ hθ) ((LaurentTail.alphaL D) f) = 0

pairT linearity in θ (feeds resMap) and injectivity

theorem RS.TailDuality.pairT_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] {D : Divisor X} (θ₁ θ₂ : MForm X) (hθ₁ : θ₁ ∈ MForm.OmegaSpace (-D)) (hθ₂ : θ₂ ∈ MForm.OmegaSpace (-D)) (hθ12 : θ₁ + θ₂ ∈ MForm.OmegaSpace (-D)) : pairT (θ₁ + θ₂) hθ12 = pairT θ₁ hθ₁ + pairT θ₂ hθ₂

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

theorem RS.TailDuality.pairT_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] {D : Divisor X} (c : ℂ) (θ : MForm X) (hθ : θ ∈ MForm.OmegaSpace (-D)) (hcθ : c • θ ∈ MForm.OmegaSpace (-D)) : pairT (c • θ) hcθ = c • pairT θ hθ

theorem RS.TailDuality.pairT_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [T1Space X] [ConnectedSpace X] {D : Divisor X} {θ : MForm X} (hθ0 : θ ≠ 0) (hθ : θ ∈ MForm.OmegaSpace (-D)) : pairT θ hθ ≠ 0

resMap: the induced map Ω(-D) →ₗ Dual(H1Tail D)

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

The residue pairing, descended to H1Tail D (Miranda's Res : L⁽¹⁾(-D) → H¹(D)^*).

Equations

• RS.TailDuality.resMap D = { toFun := fun (θ : ↥(RS.MForm.OmegaSpace (-D))) => (RS.LaurentTail.alphaL D).range.liftQ (RS.TailDuality.pairT ↑θ ⋯) ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.TailDuality.resMap_mk {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [CompactSpace X] [ConnectedSpace X] [T1Space X] (D : Divisor X) (θ : ↥(MForm.OmegaSpace (-D))) (τ : LaurentTail.T D) : ((resMap D) θ) ((LaurentTail.H1Tail.mk D) τ) = (pairT ↑θ ⋯) τ

theorem RS.TailDuality.resMap_injective {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [DecidableEq X] [CompactSpace X] [T1Space X] [ConnectedSpace X] (D : Divisor X) : Function.Injective ⇑(resMap D)