Documentation

TauCeti.FieldTheory.FunctionField.Divisor.Basic

Divisors of an algebraic function field #

A divisor of F / k is a finite integer combination of its normalized places. The underlying free abelian group, its coefficientwise order, effectivity, and its positive/negative part decomposition are supplied by TauCeti.AlgebraicGeometry.WeilDivisor; this file specializes that API rather than constructing a second formal-divisor theory.

The degree of a function-field divisor is the weighted degree

\sum_P D(P) [F_P : k].

The residue degrees are finite and positive when F / k is an algebraic function field. Thus degree is nonnegative on effective divisors, and is positive on every nonzero effective divisor. The weights cannot be omitted over a general constant field: this file identifies the weighted degree with the unweighted coefficient sum only when every place is rational, in particular over an algebraically closed constant field.

This is the divisor carrier and degree portion of Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Definition 1.4.1. Principal divisors and the product formula follow after the finiteness of zeros and poles.

source
@[reducible, inline]
abbrev TauCeti.Divisor (k : Type u_1) (F : Type u_2) [Field k] [Field F] [Algebra k F] :
Type u_2

A divisor of F / k is a finite formal integer combination of its normalized places.

Equations
Instances For
    source
    noncomputable def TauCeti.Divisor.degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] :
    Divisor k F →+ ℤ

    The degree of a function-field divisor, weighted by the degrees of its residue fields.

    Equations
    Instances For
      source
      theorem TauCeti.Divisor.degree_apply {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
      degree D = Finsupp.sum D fun (P : Place k F) (n : ℤ) => n * ↑P.degree

      The degree is the finite sum of each coefficient times the corresponding residue degree.

      source
      theorem TauCeti.Divisor.degree_eq_weightedDegree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
      degree D = (AlgebraicGeometry.WeilDivisor.weightedDegree fun (P : Place k F) => ↑P.degree) D

      The degree of a function-field divisor is the formal weighted degree against the residue degrees; this is the bridge to the weight-generic TauCeti.AlgebraicGeometry.WeilDivisor API.

      source
      theorem TauCeti.Divisor.ker_degree_eq_weightedDegreeZeroSubgroup {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] :
      degree.ker = AlgebraicGeometry.WeilDivisor.weightedDegreeZeroSubgroup fun (P : Place k F) => ↑P.degree

      The degree-zero divisors are the weighted-degree-zero divisors for the residue-degree weights. This is the bridge from the degree kernel to the weight-generic WeilDivisor API, and in particular to Pic⁰.

      source
      theorem TauCeti.Divisor.degree_eq_sum_support {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
      degree D = ∑ P ∈ D.support, D P * ↑P.degree

      The support-indexed form of the degree sum.

      source
      @[simp]
      theorem TauCeti.Divisor.degree_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] :
      degree 0 = 0
      source
      @[simp]
      theorem TauCeti.Divisor.degree_add {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) :
      degree (D + E) = degree D + degree E
      source
      @[simp]
      theorem TauCeti.Divisor.degree_neg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
      degree (-D) = -degree D
      source
      @[simp]
      theorem TauCeti.Divisor.degree_sub {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) :
      degree (D - E) = degree D - degree E
      source
      @[simp]
      theorem TauCeti.Divisor.degree_zsmul {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (n : ℤ) (D : Divisor k F) :
      degree (n • D) = n * degree D
      source
      @[simp]
      theorem TauCeti.Divisor.degree_ofPoint {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) :
      degree (AlgebraicGeometry.WeilDivisor.ofPoint P) = ↑P.degree

      A place viewed as a prime divisor has degree equal to its residue degree.

      source
      @[simp]
      theorem TauCeti.Divisor.degree_single {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (n : ℤ) :
      degree (Finsupp.single P n) = n * ↑P.degree

      The degree of a divisor supported at one place.

      source
      theorem TauCeti.Divisor.degree_range {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] :
      degree.range = AddSubgroup.closure (Set.range fun (P : Place k F) => ↑P.degree)

      The image of the degree map is the subgroup of ℤ generated by all residue degrees.

      source
      theorem TauCeti.Divisor.degree_surjective_of_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (hP : P.degree = 1) :
      Function.Surjective ⇑degree

      A rational place makes the divisor degree map surjective.

      source
      theorem TauCeti.Divisor.degree_range_eq_top_of_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (P : Place k F) (hP : P.degree = 1) :
      degree.range = ⊤

      A rational place makes the image of the divisor degree map all of ℤ.

      source
      theorem TauCeti.Divisor.degree_nonneg {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} (hD : 0 ≤ D) :
      0 ≤ degree D

      The degree of an effective divisor is nonnegative. This does not need a function-field hypothesis, since finrank is always a natural number even before its finiteness is known.

      source
      theorem TauCeti.Divisor.degree_le_of_le {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D E : Divisor k F} (hDE : D ≤ E) :
      degree D ≤ degree E

      Residue-degree weighting is monotone for the coefficientwise order on divisors.

      source
      theorem TauCeti.Divisor.monotone_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] :
      Monotone ⇑degree

      Bundled monotonicity of the function-field divisor degree.

      source
      theorem TauCeti.Divisor.degree_pos {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : 0 ≤ D) (hD0 : D ≠ 0) :
      0 < degree D

      A nonzero effective divisor of a function field has positive degree.

      source
      theorem TauCeti.Divisor.degree_eq_zero_iff {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : 0 ≤ D) :
      degree D = 0 ↔ D = 0

      An effective divisor of a function field has degree zero exactly when it is zero.

      source
      theorem TauCeti.Divisor.degree_le_degree_of_coeff_ne_zero {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] {D : Divisor k F} (hD : 0 ≤ D) {P : Place k F} (hP : AlgebraicGeometry.WeilDivisor.coeff D P ≠ 0) :
      ↑P.degree ≤ degree D

      A place carrying a nonzero coefficient in an effective divisor has degree at most the degree of that divisor.

      source
      theorem TauCeti.Divisor.card_support_le_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : 0 ≤ D) :
      ↑D.support.card ≤ degree D

      An effective divisor of a function field is supported at no more places than its degree, each place of its support contributing at least one to the degree.

      source
      theorem TauCeti.Divisor.exists_place_degree_eq_one_of_isEffective_of_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : 0 ≤ D) (hdeg : degree D = 1) :
      ∃ P ∈ D.support, P.degree = 1

      An effective divisor of degree one on an algebraic function field contains a rational place.

      Indeed, any place in its support contributes at least its positive residue degree to the total degree, so both that residue degree and its coefficient must equal one.

      source
      theorem TauCeti.Divisor.coeff_le_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : 0 ≤ D) (P : Place k F) :
      AlgebraicGeometry.WeilDivisor.coeff D P ≤ degree D

      The coefficients of an effective divisor of a function field are bounded by its degree.

      source
      theorem TauCeti.Divisor.eq_of_le_of_degree_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D E : Divisor k F} (hDE : D ≤ E) (hdeg : degree D = degree E) :
      D = E

      Equality of degrees under a coefficientwise inequality forces equality of divisors.

      source
      theorem TauCeti.Divisor.exists_eq_ofPoint_of_degree_eq_one {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) {D : Divisor k F} (hD : 0 ≤ D) (hdeg : degree D = 1) :
      ∃ (P : Place k F), P.degree = 1 ∧ D = AlgebraicGeometry.WeilDivisor.ofPoint P

      An effective divisor of degree one is a place of degree one: since every place of an algebraic function field has degree at least one, an effective divisor of degree one is the prime divisor of a single place, and that place has degree one.

      source
      theorem TauCeti.Divisor.strictMono_degree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) :
      StrictMono ⇑degree

      Degree is strictly monotone on divisors of an algebraic function field.

      source
      theorem TauCeti.Divisor.exists_le_degree_add_nsmul_ofPoint {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (hF : IsFunctionField k F) (D : Divisor k F) (P : Place k F) (c : ℤ) :
      ∃ (n : ℕ), c ≤ degree (D + n • AlgebraicGeometry.WeilDivisor.ofPoint P)

      Degrees grow without bound along a single place: since every place of an algebraic function field has degree at least one, adding enough copies of a fixed place P to D carries the degree past any prescribed bound c. This is how a divisor is made to satisfy a large-degree hypothesis while its coefficients away from P are left untouched.

      source
      theorem TauCeti.Divisor.degree_posPart_sub_degree_negPart {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D : Divisor k F) :
      degree D⁺ - degree D⁻ = degree D

      Degree splits over the positive and negative parts of a divisor.

      source
      theorem TauCeti.Divisor.degree_inf_add_degree_sup {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (D E : Divisor k F) :
      degree (D ⊓ E) + degree (D ⊔ E) = degree D + degree E

      Degree satisfies inclusion-exclusion for the coefficientwise infimum and supremum.

      source
      theorem TauCeti.Divisor.degree_eq_weilDivisorDegree {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] (h : ∀ (P : Place k F), P.degree = 1) :
      degree = AlgebraicGeometry.WeilDivisor.degree

      If every place is rational, weighted degree is the ordinary sum of coefficients.

      source
      theorem TauCeti.Divisor.degree_eq_weilDivisorDegree_of_isAlgClosed {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [IsAlgClosed k] (hF : IsFunctionField k F) :
      degree = AlgebraicGeometry.WeilDivisor.degree

      Over an algebraically closed constant field, divisor degree is the ordinary coefficient sum.

      source
      theorem TauCeti.Divisor.degree_apply_of_isAlgClosed {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra k F] [IsAlgClosed k] (hF : IsFunctionField k F) (D : Divisor k F) :
      degree D = ∑ P ∈ D.support, D P

      Over an algebraically closed constant field, the degree is the sum of the coefficients.