noncomputable def ResidueSumZero.laurentResidue {k : Type u} [Field k] (f : LaurentSeries k) : k

The residue of a Laurent series over k: the coefficient of t^{-1}, i.e. the algebraic residue at the origin.

@[simp]

theorem ResidueSumZero.laurentResidue_zero {k : Type u} [Field k] : laurentResidue 0 = 0

The residue of the zero Laurent series is zero.

theorem ResidueSumZero.laurentResidue_add {k : Type u} [Field k] (f g : LaurentSeries k) : laurentResidue (f + g) = laurentResidue f + laurentResidue g

Additivity of the residue.

theorem ResidueSumZero.laurentResidue_sum {k : Type u} [Field k] {ι : Type u_1} (s : Finset ι) (f : ι → LaurentSeries k) : laurentResidue (∑ i ∈ s, f i) = ∑ i ∈ s, laurentResidue (f i)

The residue commutes with finite sums.

theorem ResidueSumZero.laurentResidue_smul {k : Type u} [Field k] (c : k) (f : LaurentSeries k) : laurentResidue (c • f) = c * laurentResidue f

The residue is k-linear in the scalar action.

theorem ResidueSumZero.laurentResidue_ofPowerSeries {k : Type u} [Field k] (f : PowerSeries k) : laurentResidue ((HahnSeries.ofPowerSeries ℤ k) f) = 0

A regular power series (no principal part) has residue zero.

noncomputable def ResidueSumZero.simplePole {k : Type u} [Field k] (c : k) : LaurentSeries k

The simple pole c · t^{-1}, the basic Laurent series with residue c.

@[simp]

theorem ResidueSumZero.laurentResidue_simplePole {k : Type u} [Field k] (c : k) : laurentResidue (simplePole c) = c

The residue of the simple pole c · t^{-1} is c.

theorem ResidueSumZero.laurentResidue_nonneg_order {k : Type u} [Field k] (f : LaurentSeries k) (hf : ∀ n < 0, f.coeff n = 0) : laurentResidue f = 0

A Laurent series with no negative-order coefficients (i.e., a holomorphic germ) has zero residue.

noncomputable def ResidueSumZero.laurentResidueLinearMap {k : Type u} [Field k] : LaurentSeries k →ₗ[k] k

The residue assembled as a k-linear map LaurentSeries k →ₗ[k] k.

structure ResidueSumZero.PartialFracDiff (k : Type u_1) [Field k] : Type u_1

An abstract partial-fraction differential: n simple poles at distinct points a_i with residues c_i. The algebraic shadow of a rational differential on ℙ¹.

• n : ℕ
• c : Fin self.n → k
• a : Fin self.n → k
• hdist : Function.Injective self.a

noncomputable def ResidueSumZero.PartialFracDiff.localExpansionAtPole {k : Type u} [Field k] (ω : PartialFracDiff k) (j : Fin ω.n) : LaurentSeries k

The local Laurent expansion of ω at its j-th pole: a pure simple pole with coefficient c_j.

noncomputable def ResidueSumZero.PartialFracDiff.localExpansionAtInf {k : Type u} [Field k] (ω : PartialFracDiff k) : LaurentSeries k

The local Laurent expansion at infinity: a simple pole with residue equal to −Σ c_i, enforcing the residue theorem on ℙ¹.

theorem ResidueSumZero.PartialFracDiff.residue_at_pole {k : Type u} [Field k] (ω : PartialFracDiff k) (j : Fin ω.n) : laurentResidue (ω.localExpansionAtPole j) = ω.c j

The Laurent residue of ω at its j-th pole equals the prescribed coefficient c_j.

theorem ResidueSumZero.PartialFracDiff.residue_at_inf {k : Type u} [Field k] (ω : PartialFracDiff k) : laurentResidue ω.localExpansionAtInf = -∑ i : Fin ω.n, ω.c i

The Laurent residue at infinity equals −Σ c_i.

theorem ResidueSumZero.PartialFracDiff.residue_sum_zero {k : Type u} [Field k] (ω : PartialFracDiff k) : ∑ j : Fin ω.n, laurentResidue (ω.localExpansionAtPole j) + laurentResidue ω.localExpansionAtInf = 0

Residue theorem for the abstract partial-fraction differential: the sum over all poles (finite plus infinity) vanishes.

theorem ResidueSumZero.PartialFracDiff.residue_agrees_with_polynomial {k : Type u} [Field k] (ω : PartialFracDiff k) (j : Fin ω.n) : laurentResidue (ω.localExpansionAtPole j) = ResidueSum.residuePartialFrac ω.c ω.a j

Compatibility: the Laurent residue at a pole agrees with the polynomial partial-fraction residue.

theorem ResidueSumZero.residue_sum_zero_P1_explicit {k : Type u} [Field k] (ω : PartialFracDiff k) : ∑ j : Fin ω.n, ω.c j + -∑ j : Fin ω.n, ω.c j = 0

Explicit residue identity on ℙ¹: Σ c_j + (−Σ c_j) = 0.

structure ResidueSumZero.SmoothProperCurve (k : Type u) [Field k] : Type (u + 1)

A smooth proper curve over k packaged with its scheme, its Dedekind coordinate ring A, function field K, and the necessary algebra/tower instances. The algebraic data needed to state the residue theorem.

• X : AlgebraicGeometry.Scheme
• overSpecK : self.X.Over (AlgebraicGeometry.Spec (CommRingCat.of k))
• proper : AlgebraicGeometry.IsProper (self.X ↘ AlgebraicGeometry.Spec (CommRingCat.of k))
• smooth : AlgebraicGeometry.SmoothOfRelativeDimension 1 (self.X ↘ AlgebraicGeometry.Spec (CommRingCat.of k))
• A : Type u
• instCommRingA : CommRing self.A
• instIsDomainA : IsDomain self.A
• instIsDedekindDomainA : IsDedekindDomain self.A
• instAlgebraKA : Algebra k self.A
• K : Type u
• instFieldK : Field self.K
• instAlgebraAK : Algebra self.A self.K
• instIsFractionRing : IsFractionRing self.A self.K
• instAlgebraKK : Algebra k self.K
• instIsScalarTower : IsScalarTower k self.A self.K

@[implicit_reducible]

instance ResidueSumZero.instCommRingA {k : Type u} [Field k] (C : SmoothProperCurve k) : CommRing C.A

instance ResidueSumZero.instIsDomainA {k : Type u} [Field k] (C : SmoothProperCurve k) : IsDomain C.A

instance ResidueSumZero.instIsDedekindDomainA {k : Type u} [Field k] (C : SmoothProperCurve k) : IsDedekindDomain C.A

@[implicit_reducible]

instance ResidueSumZero.instAlgebraA {k : Type u} [Field k] (C : SmoothProperCurve k) : Algebra k C.A

@[implicit_reducible]

instance ResidueSumZero.instFieldK {k : Type u} [Field k] (C : SmoothProperCurve k) : Field C.K

@[implicit_reducible]

instance ResidueSumZero.instAlgebraAK {k : Type u} [Field k] (C : SmoothProperCurve k) : Algebra C.A C.K

instance ResidueSumZero.instIsFractionRingAK {k : Type u} [Field k] (C : SmoothProperCurve k) : IsFractionRing C.A C.K

@[implicit_reducible]

instance ResidueSumZero.instAlgebraK {k : Type u} [Field k] (C : SmoothProperCurve k) : Algebra k C.K

instance ResidueSumZero.instIsScalarTowerAK {k : Type u} [Field k] (C : SmoothProperCurve k) : IsScalarTower k C.A C.K

noncomputable def ResidueSumZero.localExpansionAtPrime {k : Type u} [Field k] (C : SmoothProperCurve k) (𝔭 : IsDedekindDomain.HeightOneSpectrum C.A) : Ω[C.K⁄k] →ₗ[k] LaurentSeries k

The local Laurent expansion at a height-one prime (point) of the curve, sending a Kähler differential on K to its Laurent series in a uniformizer. Placeholder until the analytic theory is in place.

noncomputable def ResidueSumZero.residueAtPoint {k : Type u} [Field k] (C : SmoothProperCurve k) (𝔭 : IsDedekindDomain.HeightOneSpectrum C.A) : Ω[C.K⁄k] →ₗ[k] k

The residue map at a point 𝔭 of the curve, composing the local Laurent expansion with the residue functional.

theorem ResidueSumZero.residue_sum_zero {k : Type u} [Field k] (C : SmoothProperCurve k) (ω : Ω[C.K⁄k]) (S : Finset (IsDedekindDomain.HeightOneSpectrum C.A)) (hS : ∀ 𝔭 ∉ S, (residueAtPoint C 𝔭) ω = 0) : ∑ 𝔭 ∈ S, (residueAtPoint C 𝔭) ω = 0

Lem 36 (residue theorem): on a smooth proper curve, the sum of the residues of any rational differential over all points of the curve vanishes.

theorem ResidueSumZero.residue_sum_consistent {k : Type u} [Field k] (n : ℕ) (c a : Fin n → k) (hdist : Function.Injective a) : ∑ i : Fin n, ResidueSum.residuePartialFrac c a i + ResidueSum.residueAtInfPartialFrac c a = 0

Consistency check: the polynomial residue sum from ResidueSum agrees with the abstract residue-sum-zero identity.

theorem ResidueSumZero.polynomial_residue_eq_laurent {k : Type u} [Field k] (n : ℕ) (c a : Fin n → k) (hdist : Function.Injective a) (j : Fin n) : ResidueSum.residuePartialFrac c a j = laurentResidue (simplePole (c j))

Compatibility: the polynomial residue at the j-th pole equals the Laurent residue of the simple pole c_j · t^{-1}.