Weierstrass gaps

At a place P, a positive integer n is a pole number if some function has a pole of order exactly n at P and is regular at every other place. Otherwise n is a gap. At a rational place of a function field with integrally closed constants and positive genus g, there are exactly g gaps: the first is 1, and every gap is at most 2g - 1. This is the Weierstrass gap theorem, Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Theorem 1.6.8.

The proof counts the jumps in the filtration

L(0) ⊆ L(P) ⊆ L(2P) ⊆ ....

At a rational place each step changes the dimension by at most one, and it changes the dimension exactly when the index is a pole number. Riemann--Roch computes ℓ((2g - 1)P) = g, so precisely g of the first 2g - 1 steps do not change the dimension.

Main definitions

• TauCeti.Place.IsPoleNumber: a natural number n witnessed by a nonzero function of order -n at the place and nonnegative order elsewhere.
• TauCeti.Place.IsGap: an integer which is not a pole number.
• TauCeti.Place.gapNumbersUpTo: the gaps in a prescribed finite interval.
• TauCeti.Place.weierstrassGaps: the finite set of gaps at a place.

Main results

• TauCeti.Place.isPoleNumber_iff_dim_lt: pole numbers are exactly the strict jumps in the one-place Riemann--Roch filtration.
• TauCeti.Place.card_gapNumbersUpTo_add_dim: among 1, ..., n, the number of gaps plus ℓ(nP) is n + 1.
• TauCeti.Place.card_weierstrassGaps: the Weierstrass gap theorem: a rational place of a function field with integrally closed constants and genus g has exactly g gaps.
• TauCeti.Place.one_mem_weierstrassGaps: the first gap is 1.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Theorem 1.6.8.
• G. Li, vaca22/riemann-roch-function-fields, a separate Lean formalization of Weierstrass gaps along the same function-field route.

def TauCeti.Place.IsPoleNumber {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) : Prop

A natural number n is a pole number at P if some nonzero function has order -n at P and is regular at every other place (Stichtenoth, Definition preceding Theorem 1.6.8).

Although the classical terminology is principally used for positive n, this definition also includes 0: the constant function 1 witnesses that zero is a pole number.

Equations

• P.IsPoleNumber n = ∃ (x : F), x ≠ 0 ∧ P.ord x = -↑n ∧ ∀ (Q : TauCeti.Place k F), Q ≠ P → 0 ≤ Q.ord x

theorem TauCeti.Place.isPoleNumber_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) : P.IsPoleNumber n ↔ ∃ (x : F), x ≠ 0 ∧ P.ord x = -↑n ∧ ∀ (Q : Place k F), Q ≠ P → 0 ≤ Q.ord x

A pole number is witnessed by a nonzero function of order -n at P and nonnegative order at every other place.

def TauCeti.Place.IsGap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) : Prop

A natural number is a gap at P if it is not a pole number at P.

Equations

• P.IsGap n = ¬P.IsPoleNumber n

@[simp]

theorem TauCeti.Place.isGap_iff_not_isPoleNumber {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) : P.IsGap n ↔ ¬P.IsPoleNumber n

Being a gap at P is being a non-pole number at P.

@[simp]

theorem TauCeti.Place.isPoleNumber_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : P.IsPoleNumber 0

Zero is a pole number at every place, witnessed by the constant function 1.

theorem TauCeti.Place.not_isGap_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : ¬P.IsGap 0

Zero is never a gap at a place.

theorem TauCeti.Place.IsPoleNumber.add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {P : Place k F} {m n : ℕ} (hm : P.IsPoleNumber m) (hn : P.IsPoleNumber n) : P.IsPoleNumber (m + n)

Pole numbers are closed under addition: multiply their witnessing functions.

theorem TauCeti.Place.isPoleNumber_iff_dim_lt {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (P : Place k F) {n : ℕ} (hn : 0 < n) : P.IsPoleNumber n ↔ Divisor.dim (↑(n - 1) • AlgebraicGeometry.WeilDivisor.ofPoint P) < Divisor.dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint P)

A positive integer is a pole number exactly when the corresponding one-place Riemann--Roch filtration has a strict dimension jump.

theorem TauCeti.Place.isGap_iff_dim_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (P : Place k F) {n : ℕ} (hn : 0 < n) : P.IsGap n ↔ Divisor.dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint P) = Divisor.dim (↑(n - 1) • AlgebraicGeometry.WeilDivisor.ofPoint P)

A positive integer is a gap exactly when the corresponding consecutive Riemann--Roch dimensions are equal.

theorem TauCeti.Place.dim_succ_zsmul_ofPoint_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {P : Place k F} (hP : P.degree = 1) (n : ℕ) : Divisor.dim (↑(n + 1) • AlgebraicGeometry.WeilDivisor.ofPoint P) ≤ Divisor.dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint P) + 1

At a rational place, adjoining one more allowed pole raises the Riemann--Roch dimension by at most one.

noncomputable def TauCeti.Place.gapNumbersUpTo {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) : Finset ℕ

The gaps at P among the positive integers at most n.

Equations

• P.gapNumbersUpTo n = Finset.filter P.IsGap (Finset.Icc 1 n)

@[simp]

theorem TauCeti.Place.mem_gapNumbersUpTo_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (m n : ℕ) : m ∈ P.gapNumbersUpTo n ↔ 1 ≤ m ∧ m ≤ n ∧ P.IsGap m

Membership in gapNumbersUpTo: the gaps in 1, ..., n.

theorem TauCeti.Place.card_gapNumbersUpTo_add_dim {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {P : Place k F} (hP : P.degree = 1) (n : ℕ) : (P.gapNumbersUpTo n).card + Divisor.dim (↑n • AlgebraicGeometry.WeilDivisor.ofPoint P) = n + 1

Among the integers 1, ..., n at a rational place, the number of gaps plus ℓ(nP) is n + 1. This is the counting identity underlying the Weierstrass gap theorem.

noncomputable def TauCeti.Place.weierstrassGaps {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) : Finset ℕ

The gaps at P in the interval 1, ..., 2g - 1. For a function field whose constants are integrally closed this interval captures every gap, so it is the full set of Weierstrass gaps; see mem_weierstrassGaps_iff_isGap.

Equations

• P.weierstrassGaps = P.gapNumbersUpTo (2 * TauCeti.genus k F - 1)

@[simp]

theorem TauCeti.Place.mem_weierstrassGaps_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℕ) : n ∈ P.weierstrassGaps ↔ 1 ≤ n ∧ n ≤ 2 * genus k F - 1 ∧ P.IsGap n

Membership in the finite set of Weierstrass gaps, before using the theorem that its upper bound captures every gap.

theorem TauCeti.Place.not_isGap_of_two_mul_genus_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) {n : ℕ} (hn : 2 * genus k F ≤ n) : ¬P.IsGap n

No integer at least 2g is a gap: Riemann--Roch produces a function whose only pole is at P, with the prescribed order.

theorem TauCeti.Place.mem_weierstrassGaps_iff_isGap {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (P : Place k F) (n : ℕ) : n ∈ P.weierstrassGaps ↔ P.IsGap n

The displayed finite set captures every gap at a place of a function field with integrally closed constants.

theorem TauCeti.Place.card_weierstrassGaps {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {P : Place k F} (hP : P.degree = 1) : P.weierstrassGaps.card = genus k F

Weierstrass gap theorem (Stichtenoth, Theorem 1.6.8): at a rational place of a function field with integrally closed constants and genus g, there are exactly g gaps.

theorem TauCeti.Place.one_mem_weierstrassGaps {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {P : Place k F} (hP : P.degree = 1) (hg : 0 < genus k F) : 1 ∈ P.weierstrassGaps

At a rational place of a positive-genus function field with integrally closed constants, 1 is a gap.