pair: the Serre pairing (Miranda's Res_ω), purely algebraic (serre-duality-cech, §2 D2)

Unit: serre-duality-cech (docs/design/serre-duality-cech.md §2 D2, §4.2).

Adaptation to the quotient revision of Jacobian/CanonicalForms/. The design's pair was written against a raw MForm structure exposing ω.coeffAt x z directly; MForm is now a quotient of MFormData (Jacobian/CanonicalForms/Quotient.lean) with no coeffAt field on classes, only the already lifted reading maps MForm.ord/resAt/laurentCoeffAt. Since MForm.laurentCoeffAt Θ x k is already exactly Miranda's c_{-1-k} read at x (chart-invariant, proof-irrelevant in the choice of representative — Jacobian/CanonicalForms/Quotient.lean's laurentCoeffAt_mk), we define pair directly as the finite sum of Laurent coefficients against the tail (the design's pair_eq_finsum_sum, i.e. Miranda's own boxed formula PDF 187), rather than via resAt of an explicit representative product and resAt_tail_mul. This is the SAME mathematical content (for any representative θ of Θ, resAt_tail_mul applied to θ.coeffAt x recovers exactly this formula — see pair_single's proof, which is the one place the "residue of a tail-multiplied form" reading is exercised) with strictly less proof debt: the τ-linearity of pair is packaged for free by Finsupp.lsum (no manual "extend to the union of two supports" finsum bookkeeping, as the original design anticipated needing finsum_add_distrib for).

The θ-linearity (pair_add_left/pair_smul_left) needs a small Compat fact not exported by canonical-forms — MForm.laurentCoeffAt is additive/ℂ-linear in the class argument — proved here via representatives + residue-calculus's laurentCoeffAt_fun_add/_const_mul/_zero_fun (coordination note filed to docs/requests/canonical-forms.md).

Compat: MForm.laurentCoeffAt is ℂ-linear in the class argument

theorem RS.MForm.laurentCoeffAt_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (Θ H : MForm X) (x : X) (k : ℤ) : (Θ + H).laurentCoeffAt x k = Θ.laurentCoeffAt x k + H.laurentCoeffAt x k

Compat (docs/requests/canonical-forms.md): additivity of laurentCoeffAt in the class argument, via representatives + residue-calculus's laurentCoeffAt_fun_add.

theorem RS.MForm.laurentCoeffAt_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (Θ : MForm X) (x : X) (k : ℤ) : (c • Θ).laurentCoeffAt x k = c * Θ.laurentCoeffAt x k

Compat (docs/requests/canonical-forms.md): ℂ-homogeneity of laurentCoeffAt in the class argument, via representatives + residue-calculus's laurentCoeffAt_const_mul.

@[simp]

theorem RS.MForm.laurentCoeffAt_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (k : ℤ) : laurentCoeffAt 0 x k = 0

pairAt: the per-point linear functional

noncomputable def RS.SerrePairing.pairAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (x : X) : (ℤ →₀ ℂ) →ₗ[ℂ] ℂ

The per-point contribution to the pairing: a finite tail of Laurent exponents at x, read against θ's Laurent coefficients there (Miranda's Res_x(r_x θ) in coefficient form). Linear in the tail-at-x argument by construction (Finsupp.lsum).

Equations

• RS.SerrePairing.pairAt θ x = (Finsupp.lsum ℂ) fun (k : ℤ) => θ.laurentCoeffAt x (-1 - k) • LinearMap.id

theorem RS.SerrePairing.pairAt_single {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (x : X) (n : ℤ) (c : ℂ) : (pairAt θ x) (Finsupp.single n c) = c * θ.laurentCoeffAt x (-1 - n)

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

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

pairTail/pairL: the full tail-linear pairing, and pair

noncomputable def RS.SerrePairing.pairTail {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) : Tail X →ₗ[ℂ] ℂ

pair θ, packaged as a genuine linear map Tail X →ₗ[ℂ] ℂ (Finsupp-summed over x).

Equations

• RS.SerrePairing.pairTail θ = (Finsupp.lsum ℂ) (RS.SerrePairing.pairAt θ)

theorem RS.SerrePairing.pairTail_add_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MForm X) : pairTail (θ + η) = pairTail θ + pairTail η

theorem RS.SerrePairing.pairTail_smul_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (θ : MForm X) : pairTail (c • θ) = c • pairTail θ

noncomputable def RS.SerrePairing.pair {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (τ : Tail X) : ℂ

The Serre pairing (Miranda's Res_ω, purely algebraic): a meromorphic 1-form θ and an ambient tail τ, paired by summing (over τ's finite support) θ's Laurent coefficients against τ's exponents.

Equations

• RS.SerrePairing.pair θ τ = (RS.SerrePairing.pairTail θ) τ

noncomputable def RS.SerrePairing.pairL {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : MForm X →ₗ[ℂ] Tail X →ₗ[ℂ] ℂ

Packaged as a genuine bilinear map (matches the design's pairL export).

Equations

• RS.SerrePairing.pairL = { toFun := RS.SerrePairing.pairTail, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.SerrePairing.pairL_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (τ : Tail X) : (pairL θ) τ = pair θ τ

theorem RS.SerrePairing.pair_add_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ η : MForm X) (τ : Tail X) : pair (θ + η) τ = pair θ τ + pair η τ

theorem RS.SerrePairing.pair_smul_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (c : ℂ) (θ : MForm X) (τ : Tail X) : pair (c • θ) τ = c * pair θ τ

theorem RS.SerrePairing.pair_zero_left {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (τ : Tail X) : pair 0 τ = 0

theorem RS.SerrePairing.pair_add_right {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (τ σ : Tail X) : pair θ (τ + σ) = pair θ τ + pair θ σ

theorem RS.SerrePairing.pair_smul_right {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (c : ℂ) (τ : Tail X) : pair θ (c • τ) = c * pair θ τ

theorem RS.SerrePairing.pair_zero_right {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) : pair θ 0 = 0

theorem RS.SerrePairing.pair_single {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (θ : MForm X) (p : X) (n : ℤ) (c : ℂ) : pair θ (Tail.single p n c) = c * θ.laurentCoeffAt p (-1 - n)

The atom the injectivity witness (Duality.lean) uses directly.