Laurent tail spaces TailAt p D / T D (laurent-tails, design §2 D1/D2/D4, §4.1)

Unit: laurent-tails (docs/design/laurent-tails.md).

• TailAt p D: the tail space at a point p — germs at the chart source of p, modulo those of order ≥ -(D p) (D1). A direct quotient, no colimit: every germ has some finite order, so the "growing window" colimit Miranda's definition literally describes collapses to a single quotient (verified by the spike, scratch_ltails.lean).
• windowAtToTailAt: Cech's finite WindowAt p (D p) d' embeds into TailAt p D for every finite d' (the two defining submodules are literally equal, not just comparable).
• T D := Π₀ p : X, TailAt p D (D2): a DFinsupp (dependent on p via chartAt ℂ p/D p). abbrev, not def — matching Cech.C0/C1/Window/H1's own convention (a plain def breaks DFunLike/AddCommGroup/Module ℂ instance search here, confirmed by the spike).
• T.mk/windowToT (D4): the finite skyscraper Window D D' embeds in T D, the bridge that will let a future bridge derive the tail-level six-term sequence from Cech's own.

Deviation from the design doc: mulTailAt/mulTail/mulTailEquiv (§2 D5) are not built here. serre-duality-tails (docs/requests/laurent-tails.md, item 4) explicitly de-scopes them: their own mulInto (built directly on T D/TailAt p D from this file) supersedes mulTail, so this is a genuine scope relief, not a shortfall.

TailAt p D (D1)

@[reducible, inline]

noncomputable abbrev RS.LaurentTail.TailAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (D : Divisor X) : Type u_1

The tail space at p: germs at the chart source of p, modulo those of order ≥ -(D p). No colimit over d' is needed: every germ has some finite order, so it already lies in some Cech.ordGe p (-d'). abbrev, not def — matching T D's own convention (D2): a plain def here is opaque enough to break Submodule.liftQ's instance/type matching against TailAt p D downstream (Comparison.lean's tailAtToH1, confirmed by that build); abbrev lets the ambient Submodule.Quotient AddCommGroup/Module ℂ instances be found directly, so the two instances previously declared here by hand are no longer needed.

Equations

• RS.LaurentTail.TailAt p D = (RS.MeroGermOn X (chartAt ℂ p).source ⧸ RS.Cech.ordGe p (-D p))

noncomputable def RS.LaurentTail.TailAt.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (D : Divisor X) : MeroGermOn X (chartAt ℂ p).source →ₗ[ℂ] TailAt p D

The quotient map onto TailAt p D.

Equations

• RS.LaurentTail.TailAt.mk p D = (RS.Cech.ordGe p (-D p)).mkQ

@[simp]

theorem RS.LaurentTail.TailAt.mk_eq_zero_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {p : X} {D : Divisor X} (ψ : MeroGermOn X (chartAt ℂ p).source) : (mk p D) ψ = 0 ↔ -↑(D p) ≤ ψ.ord p

theorem RS.LaurentTail.TailAt.mk_surjective {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (D : Divisor X) : Function.Surjective ⇑(mk p D)

windowAtToTailAt (D1 continued)

noncomputable def RS.LaurentTail.windowAtToTailAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (D : Divisor X) (d' : ℤ) : Cech.WindowAt p (D p) d' →ₗ[ℂ] TailAt p D

Cech's finite Laurent window at p (between orders -d' and -(D p)) embeds into the full tail space: WindowAt p (D p) d''s defining submodule, viewed inside ordGe p (-d'), is exactly the restriction of ordGe p (-(D p)) there.

Equations

• RS.LaurentTail.windowAtToTailAt p D d' = (Submodule.comap (RS.Cech.ordGe p (-d')).subtype (RS.Cech.ordGe p (-D p))).mapQ (RS.Cech.ordGe p (-D p)) (RS.Cech.ordGe p (-d')).subtype ⋯

theorem RS.LaurentTail.windowAtToTailAt_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (D : Divisor X) (d' : ℤ) (ψ : ↥(Cech.ordGe p (-d'))) : (windowAtToTailAt p D d') ((Cech.WindowAt.mk p (D p) d') ψ) = (TailAt.mk p D) ↑ψ

theorem RS.LaurentTail.exists_windowAt_repr {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (p : X) (D : Divisor X) (z : TailAt p D) : ∃ (d' : ℤ) (ψ : ↥(Cech.ordGe p (-d'))), (windowAtToTailAt p D d') ((Cech.WindowAt.mk p (D p) d') ψ) = z

Every tail class is represented by some finite window (the union-of-ordGe fact): every germ has an honest WithTop ℤ-order, hence lies in ordGe p (-d') for d' large enough.

T D (D2)

@[reducible, inline]

noncomputable abbrev RS.LaurentTail.T {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : Type u_1

Miranda's T[D]: finitely-supported tail data (D2). abbrev, not def — a plain def breaks DFunLike/AddCommGroup/Module ℂ instance search for the assembled DFinsupp (confirmed by the spike, scratch_ltails.lean).

Equations

• RS.LaurentTail.T D = Π₀ (p : X), RS.LaurentTail.TailAt p D

@[instance_reducible]

noncomputable instance RS.LaurentTail.instAddCommGroupT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : AddCommGroup (T D)

Equations

• RS.LaurentTail.instAddCommGroupT D = { toAddGroup := DFinsupp.instAddGroup, add_comm := ⋯ }

@[instance_reducible]

noncomputable instance RS.LaurentTail.instModuleT {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : Divisor X) : Module ℂ (T D)

Equations

• RS.LaurentTail.instModuleT D = { toDistribMulAction := DFinsupp.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def RS.LaurentTail.T.mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] (D : Divisor X) (S : Finset X) (x : (p : ↑↑S) → TailAt (↑p) D) : T D

A single finitely-supported tail element, built from a Finset witness (mirrors Cech.Window.diffSupp's own pattern).

Equations

• RS.LaurentTail.T.mk D S x = DFinsupp.mk S x

theorem RS.LaurentTail.T.mk_apply_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] {D : Divisor X} {S : Finset X} {x : (p : ↑↑S) → TailAt (↑p) D} {p : X} (hp : p ∈ S) : (mk D S x) p = x ⟨p, hp⟩

theorem RS.LaurentTail.T.mk_apply_not_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [DecidableEq X] {D : Divisor X} {S : Finset X} {x : (p : ↑↑S) → TailAt (↑p) D} {p : X} (hp : p ∉ S) : (mk D S x) p = 0

windowToT (D4): the finite skyscraper embeds in the tail space

noncomputable def RS.LaurentTail.windowToT {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [DecidableEq X] [CompactSpace X] (D D' : Divisor X) (_h : D ≤ D') : Cech.Window D D' →ₗ[ℂ] T D

The finite skyscraper Window D D' embeds in the full tail space T D — the bridge that lets a future bridge file derive the tail-level six-term sequence from Cech's own (instead of re-proving it).

Equations

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

theorem RS.LaurentTail.windowToT_apply {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [DecidableEq X] [CompactSpace X] (D D' : Divisor X) (h : D ≤ D') (w : Cech.Window D D') (q : ↥(Cech.diffSupp D D')) : ((windowToT D D' h) w) ↑q = (windowAtToTailAt (↑q) D (D' ↑q)) (w q)