Elliptic function fields #
An algebraic function field F / k is elliptic when it has genus one and carries a divisor of
degree one. The degree-one divisor belongs to the definition and is not a consequence of the
genus: it is what Riemann–Roch converts into a place of degree one, and nothing about a
genus-one function field over a general constant field produces one.
This file proves the basic dictionary of an elliptic function field over an exact constant
field. A divisor of degree one is linearly equivalent to exactly one place of degree one, so an
elliptic function field has a place of degree one; and once a place P₀ of degree one is
chosen, P ↦ [P - P₀] is a bijection from the places of degree one onto the degree-zero divisor
class group Cl⁰(F). The addition of Cl⁰(F) transported along that bijection is the
intrinsic group law of the degree-one places: it makes the bijection an isomorphism of groups,
and P ⊕ Q = R exactly when the divisors P + Q and R + P₀ are linearly equivalent. The
transported group depends on the choice of P₀, so it is a definition, not an instance.
Main definitions #
TauCeti.IsEllipticFunctionField: genus one together with a divisor of degree one.TauCeti.Place.degreeOneEquivDegreeZeroClassGroup: the bijectionP ↦ [P - P₀]from the degree-one places of a genus-one function field ontoCl⁰(F).TauCeti.Place.degreeOneAddCommGroupandTauCeti.Place.degreeOneAddEquivDegreeZeroClassGroup: the addition ofCl⁰(F)transported along that bijection, and the bijection read as an isomorphism of groups.
Main results #
TauCeti.Divisor.exists_linearlyEquivalent_ofPoint_of_genus_eq_oneandTauCeti.Place.eq_of_linearlyEquivalent_ofPoint_of_genus_eq_one: in genus one a divisor of degree one is linearly equivalent to exactly one place of degree one.TauCeti.IsEllipticFunctionField.exists_place_degree_eq_one: an elliptic function field has a place of degree one;TauCeti.isEllipticFunctionField_iff_genus_eq_one_and_exists_place_degree_eq_oneis the converse.TauCeti.Place.degreeOneAddCommGroup_add_eq_iff: the group law of the degree-one places,P ⊕ Q = R ↔ P + Q ∼ R + P₀.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Section VI.1: Definition 6.1.1, Proposition 6.1.6 and Proposition 6.1.7.
An elliptic function field (Stichtenoth, Definition 6.1.1): this predicate records the two conditions of the definition, genus one and the existence of a divisor of degree one.
Being an algebraic function field is not part of the predicate: the hypothesis
TauCeti.IsFunctionField, like the exactness of the constant field, is kept as a separate
hypothesis on the statements that need it, as everywhere in this development.
An elliptic function field has genus one.
- exists_divisor_degree_eq_one : ∃ (D : Divisor k F), Divisor.degree D = 1
An elliptic function field carries a divisor of degree one.
Instances For
Degree-one divisors and degree-one places #
A divisor of degree one with a nonzero Riemann–Roch space is linearly equivalent to a place
of degree one: this is the genus-free half of Stichtenoth, Proposition 6.1.6(a). A nonzero
L(D) puts an effective divisor in the class of D, and an effective divisor of degree one is
the prime divisor of a place of degree one.
A divisor of degree one of a genus-one function field is linearly equivalent to a place of
degree one (Stichtenoth, Proposition 6.1.6(a)): in genus one Riemann–Roch gives ℓ(D) = 1, so
L(D) is nonzero.
Linearly equivalent places of degree one of a genus-one function field are equal
(Stichtenoth, Proposition 6.1.6(b)): over an exact constant field ℓ(P) = 1 forces the complete
linear system of P to be the single divisor P.
Places of degree one #
An elliptic function field has a place of degree one (Stichtenoth, Proposition 6.1.6(a)).
Over an exact constant field, a function field is elliptic exactly when it has genus one and a place of degree one.
The degree-one places as the degree-zero divisor class group #
Distinct places of degree one of a genus-one function field have distinct classes relative to a base place.
Every degree-zero divisor class of a genus-one function field is the class of a difference of places of degree one (Stichtenoth, Proposition 6.1.6(b)).
The places of degree one of an elliptic function field are the degree-zero divisor
classes (Stichtenoth, Proposition 6.1.6(b)): relative to a chosen place P₀ of degree one,
P ↦ [P - P₀] is a bijection onto Cl⁰(F).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class attached to a degree-one place by the bijection onto Cl⁰(F).
The base place is the zero of the group law.
Addition of the classes of two degree-one places (Stichtenoth, Proposition 6.1.7): the
images of P and Q in Cl⁰(F) add up to the image of R exactly when the divisors P + Q
and R + P₀ are linearly equivalent.
The group law of the degree-one places of an elliptic function field (Stichtenoth,
Proposition 6.1.7): the addition of Cl⁰(F) transported along the bijection
P ↦ [P - P₀]. It depends on the base place P₀, so it is a definition and not an instance;
TauCeti.Place.degreeOneAddCommGroup_add_eq_iff characterises it by linear equivalence.
Equations
- TauCeti.Place.degreeOneAddCommGroup hF hex hg hP₀ = (TauCeti.Place.degreeOneEquivDegreeZeroClassGroup hF hex hg hP₀).addCommGroup
Instances For
The degree-one places of an elliptic function field are the group Cl⁰(F) (Stichtenoth,
Proposition 6.1.7): for the transported addition, P ↦ [P - P₀] is an isomorphism of groups.
Equations
- TauCeti.Place.degreeOneAddEquivDegreeZeroClassGroup hF hex hg hP₀ = (TauCeti.Place.degreeOneEquivDegreeZeroClassGroup hF hex hg hP₀).addEquiv
Instances For
The isomorphism of groups is the underlying bijection.
The zero of the transported group law is the base place.
The group law of the degree-one places is linear equivalence of divisors (Stichtenoth,
Proposition 6.1.7): P ⊕ Q = R exactly when P + Q ∼ R + P₀.