Tail X: free ambient Laurent-tail data, and TailSpace D (serre-duality-cech, §2 D1)

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

Miranda VI.3's ambient Laurent-tail space, before any D-bound: at finitely many points of X, an arbitrary finite tail of Laurent coefficients (any integer exponents, read in each point's own chartAt — no compatibility/transition data needed, since the pairing (Pairing.lean) never crosses charts). Tail X imposes no exponent condition at all (finite support only, entirely free via Finsupp); Tail.BoundedBy/TailSpace D is the only place any bound enters, parameterized by a divisor D (Miranda's T[D](X), top degree < -(D p)).

Deviation from the design (adaptation, not a correction): docs/design/serre-duality-cech.md declared Tail X as a def plus manually-registered AddCommGroup ℂ/Module ℂ instances. The sibling unit laurent-tails independently discovered that a plain def wrapping a Finsupp/ DFinsupp breaks DFunLike/AddCommGroup/Module instance search (Jacobian/LaurentTail/TailSpace.lean's own module docstring, confirmed by their spike scratch_ltails.lean); using abbrev here sidesteps the issue entirely (reducible unfolding lets every Finsupp instance transport for free), so no manual instances are needed at all.

@[reducible, inline]

noncomputable abbrev RS.SerrePairing.Tail (X : Type u_2) : Type u_2

Miranda VI.3's ambient Laurent-tail space: at finitely many points of X, an arbitrary finite tail of Laurent coefficients (any integer exponents), read in each point's own chartAt.

Equations

• RS.SerrePairing.Tail X = (X →₀ ℤ →₀ ℂ)

def RS.SerrePairing.Tail.BoundedBy {X : Type u_1} [TopologicalSpace X] (τ : Tail X) (D : Divisor X) : Prop

Miranda's T[D](X)-membership condition: the exponent at each point in τ's support is bounded by D (exponent range < -(D x), matching her convention exactly — for D = 0 this is "only negative exponents", her own base case).

Equations

• τ.BoundedBy D = ∀ x ∈ τ.support, ∀ k ∈ (τ x).support, k < -D x

def RS.SerrePairing.TailSpace {X : Type u_1} [TopologicalSpace X] (D : Divisor X) : Submodule ℂ (Tail X)

D-bounded ambient tails form a submodule (Miranda's T[D](X)).

Equations

• RS.SerrePairing.TailSpace D = { carrier := {τ : RS.SerrePairing.Tail X | τ.BoundedBy D}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem RS.SerrePairing.mem_tailSpace_iff {X : Type u_1} [TopologicalSpace X] {τ : Tail X} {D : Divisor X} : τ ∈ TailSpace D ↔ τ.BoundedBy D

noncomputable def RS.SerrePairing.Tail.single {X : Type u_1} (p : X) (n : ℤ) (c : ℂ) : Tail X

A single-point, single-exponent test tail.

Equations

• RS.SerrePairing.Tail.single p n c = Finsupp.single p (Finsupp.single n c)

theorem RS.SerrePairing.Tail.single_apply {X : Type u_1} (p : X) (n : ℤ) (c : ℂ) (x : X) : (single p n c) x = if x = p then Finsupp.single n c else 0

theorem RS.SerrePairing.Tail.single_boundedBy {X : Type u_1} [TopologicalSpace X] {p : X} {n : ℤ} {c : ℂ} {D : Divisor X} (h : c ≠ 0 → n < -D p) : (single p n c).BoundedBy D