The divisor-degree index #
For a finite separable extension of K(X), divisor degree is an additive map
from the exhaustive divisor group to ℤ. Its image is a nonzero subgroup of
ℤ, hence is generated by one positive natural number. This file defines
that generator and proves its two equivalent universal properties:
- it generates every divisor degree; and
- it is the greatest common divisor of the degrees of all exhaustive places.
This is the integer δ introduced in Stichtenoth, Lemma 5.1.4 (printed
p. 187). The zeta-function rationality argument initially works with δ
arbitrary. The later theorem δ = 1 is F. K. Schmidt's theorem (Corollary
5.1.11, printed p. 191); Stichtenoth proves it only after rationality and the
constant-extension identity for zeta functions. Consequently no implication
from exact constants to δ = 1 is asserted here: doing so at this stage would
make the intended zeta proof circular. The exact missing conclusion is
isolated by the degree-one criterion at the end of the file.
Divisor degree as an additive homomorphism to ℤ.
Equations
- BGS.HasseWeil.finiteExtensionDivisorDegreeHom K L = { toFun := BGS.CorvajaZannier.finiteExtensionDivisorDegree K L, map_zero' := ⋯, map_add' := ⋯ }
Instances For
A cyclic generator of the image of divisor degree in the integers.
Equations
Instances For
The positive generator of the image of divisor degree. Equivalently, this is the gcd of the degrees of all exhaustive places.
Equations
Instances For
The divisor-degree index is strictly positive.
Every divisor degree is an integer multiple of the index.
The index itself occurs as the degree of an exhaustive divisor.
The image of divisor degree is exactly the subgroup of multiples of the index.
An integer occurs as a divisor degree exactly when it is a multiple of the index.
Natural-valued form of index divisibility, used for zeta coefficients.
If the index does not divide n, there is no divisor (and hence no
effective divisor) of degree n.
The index divides the degree of each exhaustive place.
Any natural number dividing every place degree also divides the divisor
degree index. Together with finiteExtensionDivisorDegreeIndex_dvd_placeDegree,
this is the gcd universal property.
Universal characterization of the divisor-degree index as the gcd of all exhaustive place degrees.
A positive divisor degree is at least the index.
The index is one exactly when there exists an exhaustive divisor of degree one. Thus an exact-constants-to-index-one proof must genuinely construct (or otherwise imply) such a degree-one divisor; exact constants by themselves only control the kernel of principal divisor, not this image.