The divisor of a Weil differential, and the Riemann–Roch theorem

TauCeti.Divisor.IsRiemannRochDivisor records what it means for a divisor W to satisfy the Riemann–Roch identity ℓ(D) = deg D + 1 - g₀ + ℓ(W - D); for such a W the number g₀ is the genus, deg W = 2g - 2 and ℓ(W) = g, and any two such divisors are linearly equivalent. The Riemann–Roch theorem, proved here, is that such a W exists.

The witness is the divisor of a nonzero Weil differential. Enlarging a divisor shrinks the space Ω_F(D) of Weil differentials it bounds, so the divisors bounding a fixed ω form a downward closed family; the two facts that make it have a greatest element are that the family is stable under suprema (TauCeti.weilDifferentialFiltration_sup) and that its degrees are bounded above, because past the threshold of Riemann's theorem the index of specialty vanishes and with it Ω_F(D). A divisor of maximal degree in the family is then the greatest, since places have positive degree.

Writing W for that greatest divisor, multiplication by a function is an injective k-linear map F → Ω_F carrying L(W - D) onto Ω_F(D): a nonzero x has x · ω ∈ Ω_F(D) exactly when ω ∈ Ω_F(D - div x), which by maximality says D - div x ≤ W, that is x ∈ L(W - D); and it is onto because every Weil differential is a multiple of ω (Proposition 1.5.9, TauCeti.exists_repartitionDualMul_eq). So ℓ(W - D) = dim_k Ω_F(D) = i(D), which rearranges to the Riemann–Roch identity.

Main definitions

• TauCeti.weilDifferentialDivisor: the divisor (ω) of a nonzero Weil differential (Stichtenoth, Definition 1.5.11), the greatest divisor bounding it.
• TauCeti.canonicalClass: the canonical class in the divisor class group, represented by the divisor of any nonzero Weil differential.
• TauCeti.weilDifferentialOrder: the order v_P(ω) of a nonzero Weil differential at a place, the coefficient of P in (ω).
• TauCeti.riemannRochSpaceEquivWeilDifferentialFiltration: the duality isomorphism L(W - D) ≃ Ω_F(D), x ↦ x · ω (Stichtenoth, Theorem 1.5.14).

Main results

• TauCeti.exists_forall_degree_lt_of_mem_weilDifferentialFiltration: the divisors bounding a fixed nonzero Weil differential have bounded degree.
• TauCeti.exists_isGreatest_mem_weilDifferentialFiltration: the divisor of a nonzero Weil differential — among the divisors bounding it there is a greatest (Stichtenoth, Lemma 1.5.10).
• TauCeti.mem_weilDifferentialFiltration_iff_le_of_isGreatest and TauCeti.mem_weilDifferentialFiltration_iff_le_weilDifferentialDivisor: ω ∈ Ω_F(D) ↔ D ≤ (ω), the characteristic property of that divisor.
• TauCeti.weilDifferentialDivisor_repartitionDualMul: the transformation law (z · ω) = div z + (ω) (Stichtenoth, Proposition 1.5.13), which is what makes the class of (ω) — the canonical class — independent of ω.
• TauCeti.divisorClass_weilDifferentialDivisor: the divisor of every nonzero Weil differential represents TauCeti.canonicalClass.
• TauCeti.repartitionDualMul_mem_weilDifferentialFiltration_iff_mem_riemannRochSpace: the membership x · ω ∈ Ω_F(D) ↔ x ∈ L(W - D) that carries the theorem.
• TauCeti.map_riemannRochSpace_repartitionDualMulRight and TauCeti.dim_sub_eq_finrank_weilDifferentialFiltration: the duality theorem — x ↦ x · ω maps L(W - D) onto Ω_F(D), so ℓ(W - D) = dim_k Ω_F(D) (Stichtenoth, Theorem 1.5.14).
• TauCeti.isRiemannRochDivisor_of_isGreatest_mem_weilDifferentialFiltration and TauCeti.isRiemannRochDivisor_weilDifferentialDivisor: that divisor is a Riemann–Roch divisor for the genus (Stichtenoth, Theorem 1.5.15).
• TauCeti.dim_weilDifferentialDivisor and TauCeti.degree_weilDifferentialDivisor: ℓ((ω)) = g and deg (ω) = 2g - 2 (Stichtenoth, Corollary 1.5.16).
• TauCeti.degreeClass_canonicalClass: the canonical class has degree 2g - 2.
• TauCeti.exists_isRiemannRochDivisor: the Riemann–Roch theorem — a Riemann–Roch divisor exists.
• TauCeti.exists_isGreatest_of_divisorClass_eq_canonicalClass: every divisor of the canonical class is the divisor of a nonzero Weil differential.
• TauCeti.divisorClass_eq_canonicalClass_iff: the characterization of canonical divisors (Stichtenoth, Proposition 1.6.2) — a divisor represents the canonical class exactly when deg D = 2g - 2 and ℓ(D) ≥ g.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section I.5, in particular Lemma 1.5.10, Theorem 1.5.14 and Theorem 1.5.15, and Proposition 1.6.2.

The divisor of a nonzero Weil differential

theorem TauCeti.exists_forall_degree_lt_of_mem_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) : ∃ (c : ℤ), ∀ (D : Divisor k F), ω ∈ weilDifferentialFiltration D → Divisor.degree D < c

The divisors bounding a fixed nonzero Weil differential have bounded degree.

theorem TauCeti.exists_isGreatest_mem_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : ∃ (W : Divisor k F), IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W

The divisor of a nonzero Weil differential (Stichtenoth, Lemma 1.5.10): the divisors bounding ω have a greatest element.

theorem TauCeti.mem_weilDifferentialFiltration_iff_le_of_isGreatest {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {ω : Module.Dual k ↥(repartitionSpace k F)} {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) (D : Divisor k F) : ω ∈ weilDifferentialFiltration D ↔ D ≤ W

The characteristic property of the divisor of ω, in the form consumers use: ω is bounded by D exactly when D is at most the divisor of ω.

noncomputable def TauCeti.weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : Divisor k F

The divisor (ω) of a nonzero Weil differential (Stichtenoth, Definition 1.5.11): the greatest divisor bounding ω, which exists by TauCeti.exists_isGreatest_mem_weilDifferentialFiltration. The hypotheses are exactly what that existence needs, so the value is always the divisor it is meant to denote; its characteristic property is TauCeti.mem_weilDifferentialFiltration_iff_le_weilDifferentialDivisor.

Equations

• TauCeti.weilDifferentialDivisor hF hex hmem hω = ⋯.choose

theorem TauCeti.isGreatest_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} (weilDifferentialDivisor hF hex hmem hω)

The divisor of a nonzero Weil differential is indeed the greatest divisor bounding it.

@[simp]

theorem TauCeti.mem_weilDifferentialFiltration_iff_le_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (D : Divisor k F) : ω ∈ weilDifferentialFiltration D ↔ D ≤ weilDifferentialDivisor hF hex hmem hω

The characteristic property of (ω): a nonzero Weil differential is bounded by D exactly when D ≤ (ω).

noncomputable def TauCeti.weilDifferentialOrder {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (P : Place k F) : ℤ

The order v_P(ω) of a nonzero Weil differential at a place (Stichtenoth, Definition 1.5.11): the coefficient of P in the divisor (ω). A differential is regular, or holomorphic, exactly when all of its orders are nonnegative, that is when 0 ≤ (ω).

Equations

• TauCeti.weilDifferentialOrder hF hex hmem hω P = TauCeti.AlgebraicGeometry.WeilDivisor.coeff (TauCeti.weilDifferentialDivisor hF hex hmem hω) P

@[simp]

theorem TauCeti.coeff_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (P : Place k F) : AlgebraicGeometry.WeilDivisor.coeff (weilDifferentialDivisor hF hex hmem hω) P = weilDifferentialOrder hF hex hmem hω P

The divisor of a nonzero Weil differential has the orders v_P(ω) as its coefficients.

theorem TauCeti.mem_weilDifferentialFiltration_zero_iff_forall_order_nonneg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : ω ∈ weilDifferentialFiltration 0 ↔ ∀ (P : Place k F), 0 ≤ weilDifferentialOrder hF hex hmem hω P

A nonzero Weil differential is regular (or holomorphic), meaning that it is bounded by the zero divisor, exactly when its order is nonnegative at every place. This is deliberately not @[simp]: TauCeti.mem_weilDifferentialFiltration_iff_le_weilDifferentialDivisor already sends the left-hand side to the divisor inequality 0 ≤ (ω), which is the simp-normal form.

@[simp]

theorem TauCeti.weilDifferentialDivisor_repartitionDualMul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (z : Fˣ) : weilDifferentialDivisor hF hex ⋯ ⋯ = Divisor.principal hF z + weilDifferentialDivisor hF hex hmem hω

The transformation law (z · ω) = div z + (ω) (Stichtenoth, Proposition 1.5.13): the divisor of a Weil differential changes by a principal divisor when the differential is multiplied by a nonzero function, so the class of (ω) in the divisor class group — the canonical class — does not depend on ω.

theorem TauCeti.divisorClass_weilDifferentialDivisor_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω η : Module.Dual k ↥(repartitionSpace k F)} (hωmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) (hηmem : η ∈ weilDifferentialSpace k F) (hη : η ≠ 0) : (Place.orderSystem hF).divisorClass (weilDifferentialDivisor hF hex hωmem hω) = (Place.orderSystem hF).divisorClass (weilDifferentialDivisor hF hex hηmem hη)

The divisors of any two nonzero Weil differentials have the same divisor class.

noncomputable def TauCeti.canonicalClass {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : (Place.orderSystem hF).ClassGroup

The canonical class of an algebraic function field with exact constant field: the divisor class of a nonzero Weil differential. Such a differential exists by TauCeti.weilDifferentialSpace_ne_bot, and TauCeti.divisorClass_weilDifferentialDivisor shows that the class is independent of the chosen differential.

Equations

• TauCeti.canonicalClass hF hex = (TauCeti.Place.orderSystem hF).divisorClass (TauCeti.weilDifferentialDivisor hF hex ⋯ ⋯)

@[simp]

theorem TauCeti.divisorClass_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : (Place.orderSystem hF).divisorClass (weilDifferentialDivisor hF hex hmem hω) = canonicalClass hF hex

Every nonzero Weil differential represents the canonical class.

The Riemann–Roch theorem

theorem TauCeti.repartitionDualMul_mem_weilDifferentialFiltration_iff_mem_riemannRochSpace {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {ω : Module.Dual k ↥(repartitionSpace k F)} {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) (D : Divisor k F) (x : F) : ((repartitionDualMul hF) x) ω ∈ weilDifferentialFiltration D ↔ x ∈ riemannRochSpace (W - D)

Duality between L(W - D) and Ω_F(D), for W the divisor of ω: a function x multiplies ω into Ω_F(D) exactly when it lies in L(W - D).

theorem TauCeti.map_riemannRochSpace_repartitionDualMulRight {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) (D : Divisor k F) : Submodule.map (repartitionDualMulRight hF ω) (riemannRochSpace (W - D)) = weilDifferentialFiltration D

The image of L(W - D) under multiplication by ω is Ω_F(D), for W the divisor of a nonzero Weil differential ω.

noncomputable def TauCeti.riemannRochSpaceEquivWeilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) (D : Divisor k F) : ↥(riemannRochSpace (W - D)) ≃ₗ[k] ↥(weilDifferentialFiltration D)

The duality theorem (Stichtenoth, Theorem 1.5.14): for W the divisor of a nonzero Weil differential ω, multiplication by ω is a k-linear isomorphism L(W - D) ≃ Ω_F(D).

Equations

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

@[simp]

theorem TauCeti.riemannRochSpaceEquivWeilDifferentialFiltration_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) (D : Divisor k F) (x : ↥(riemannRochSpace (W - D))) : ↑((riemannRochSpaceEquivWeilDifferentialFiltration hF hex hω hW D) x) = ((repartitionDualMul hF) ↑x) ω

The duality equivalence sends x to the Weil differential x · ω.

theorem TauCeti.dim_sub_eq_finrank_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) (D : Divisor k F) : (W - D).dim = Module.finrank k ↥(weilDifferentialFiltration D)

The duality theorem, in dimensions: ℓ(W - D) = dim_k Ω_F(D).

theorem TauCeti.isRiemannRochDivisor_of_isGreatest_mem_weilDifferentialFiltration {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hω : ω ≠ 0) {W : Divisor k F} (hW : IsGreatest {D : Divisor k F | ω ∈ weilDifferentialFiltration D} W) : W.IsRiemannRochDivisor (genus k F)

The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15): the divisor of a nonzero Weil differential is a Riemann–Roch divisor for the genus.

theorem TauCeti.isRiemannRochDivisor_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : (weilDifferentialDivisor hF hex hmem hω).IsRiemannRochDivisor (genus k F)

The Riemann–Roch theorem (Stichtenoth, Theorem 1.5.15), for the divisor (ω) itself: the divisor of a nonzero Weil differential is a Riemann–Roch divisor for the genus.

theorem TauCeti.dim_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : (weilDifferentialDivisor hF hex hmem hω).dim = genus k F

ℓ((ω)) = g (Stichtenoth, Corollary 1.5.16): the divisor of a nonzero Weil differential has Riemann–Roch space of dimension the genus.

theorem TauCeti.degree_weilDifferentialDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {ω : Module.Dual k ↥(repartitionSpace k F)} (hmem : ω ∈ weilDifferentialSpace k F) (hω : ω ≠ 0) : Divisor.degree (weilDifferentialDivisor hF hex hmem hω) = 2 * ↑(genus k F) - 2

deg (ω) = 2g - 2 (Stichtenoth, Corollary 1.5.16): the divisor of a nonzero Weil differential has degree 2g - 2, so the canonical class has that degree.

@[simp]

theorem TauCeti.degreeClass_canonicalClass {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : (Divisor.degreeClass hF) (canonicalClass hF hex) = 2 * ↑(genus k F) - 2

The canonical class has degree 2g - 2 (Stichtenoth, Corollary 1.5.16).

theorem TauCeti.exists_isRiemannRochDivisor {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) : ∃ (W : Divisor k F), W.IsRiemannRochDivisor (genus k F)

The Riemann–Roch theorem, existence form (Stichtenoth, Theorem 1.5.15): every algebraic function field with exact constant field has a Riemann–Roch divisor, namely the divisor of any nonzero Weil differential, whose dimension and degree are recorded by TauCeti.dim_weilDifferentialDivisor and TauCeti.degree_weilDifferentialDivisor.

The characterization of canonical divisors

theorem TauCeti.isRiemannRochDivisor_of_divisorClass_eq_canonicalClass {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {D : Divisor k F} (hD : (Place.orderSystem hF).divisorClass D = canonicalClass hF hex) : D.IsRiemannRochDivisor (genus k F)

A divisor representing the canonical class is a Riemann–Roch divisor for the genus.

theorem TauCeti.exists_isGreatest_of_divisorClass_eq_canonicalClass {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) {D : Divisor k F} (hD : (Place.orderSystem hF).divisorClass D = canonicalClass hF hex) : ∃ ω ∈ weilDifferentialSpace k F, ω ≠ 0 ∧ IsGreatest {E : Divisor k F | ω ∈ weilDifferentialFiltration E} D

Every divisor of the canonical class is the divisor of a Weil differential: the canonical class does not merely contain the divisors of nonzero Weil differentials up to linear equivalence, every one of its representatives is such a divisor on the nose.

theorem TauCeti.divisorClass_eq_canonicalClass_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (hex : IsIntegrallyClosedIn k F) (D : Divisor k F) : (Place.orderSystem hF).divisorClass D = canonicalClass hF hex ↔ Divisor.degree D = 2 * ↑(genus k F) - 2 ∧ genus k F ≤ D.dim

The characterization of canonical divisors (Stichtenoth, Proposition 1.6.2): a divisor represents the canonical class exactly when it has degree 2g - 2 and its Riemann–Roch space has dimension at least the genus.