Pulling a divisor back along an isogeny #
An isogeny embeds F(W₂) in F(W₁) as a finite extension, and the conorm of that extension is
the pullback of divisors: the coefficient of φ* D at a place P' is e(P' ∣ P) times the
coefficient of D at the place below it. Nothing about curves enters beyond the embedding being
finite, which is what the degree of an isogeny says.
The one fact the divisor construction of the Weil pairing needs of this is that it carries
principal divisors to principal divisors: φ*(div z) is the divisor of the pulled-back function.
That is what lets a function with a prescribed divisor be pulled back and its divisor read off.
Conventions #
The algebra structure on F(W₁) over F(W₂) is not an instance — it depends on φ — so it is
taken as a parameter together with the hypothesis that its structure map is fieldPullback, the
form TauCeti.Isogeny.degree_eq_finrank and TauCeti.Isogeny.finiteDimensional_functionField
already use. A caller supplies it with let _ := φ.fieldPullback.toRingHom.toAlgebra.
Main definitions #
TauCeti.Isogeny.divisorPullback: the pullback of a divisor along an isogeny.
Main results #
TauCeti.Isogeny.coeff_divisorPullbackandTauCeti.Isogeny.mem_support_divisorPullback_iff: the coefficient formula and the support, the characteristic API of the pullback.TauCeti.Isogeny.divisorPullback_ofPoint: the pullback of a point divisor is its fibre, weighted by the ramification indices.TauCeti.Isogeny.divisorPullback_mono,TauCeti.Isogeny.isEffective_divisorPullbackandTauCeti.Isogeny.divisorPullback_injective: it is monotone, preserves effectivity, and is injective.TauCeti.Isogeny.divisorPullback_principal: it carriesdiv zto the divisor of the pulled-back function, andTauCeti.Isogeny.linearlyEquivalent_divisorPullbackthat it respects linear equivalence.TauCeti.Isogeny.divisorPullback_id: the identity law —id* D = D.TauCeti.Isogeny.divisorPullback_comp: it is contravariantly functorial — pulling back along a composite is pulling back twice, in the reverse order.TauCeti.Isogeny.divisorPullbackClassGroupandTauCeti.Isogeny.divisorPullbackClassGroup_divisorClass: the induced map on divisor classes, and its value on the class of a divisor, with the identity and composition lawsTauCeti.Isogeny.divisorPullbackClassGroup_idandTauCeti.Isogeny.divisorPullbackClassGroup_comp.
Each is the corresponding TauCeti.Divisor.conorm result read through the isogeny; the definition
is opaque outside this module, so the wrappers are what a consumer has.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, Definition 3.1.8 and Proposition 3.1.9.
- J. Silverman, The Arithmetic of Elliptic Curves, II.3.
The pullback of a divisor along an isogeny: the conorm of the finite extension of function fields that the isogeny induces.
Equations
Instances For
The coefficients and the support #
These three read the place below P', so the base-field tower and the finiteness of the extension
have to be in scope for their statements to elaborate, not just for their proofs. Both follow from
h, so they are installed while the statement elaborates rather than quantified: a caller that can
supply h should not have to supply them a second time.
The defining coefficient formula: the coefficient of φ* D at a place P' of F(W₁) is
e(P' ∣ P) times the coefficient of D at the place P below it.
A place of F(W₁) lies in the support of φ* D exactly when the place below it lies in the
support of D: the ramification indices are positive, so nothing cancels.
The pullback of a point divisor is its fibre, the places above P weighted by their
ramification indices — geometrically φ⁻¹(P) with multiplicity.
The pullback is monotone: it multiplies coefficients by positive ramification indices.
The pullback of an effective divisor is effective.
The pullback is injective: every place of F(W₂) is the restriction of a place of
F(W₁), and the ramification indices are nonzero.
An isogeny carries div z to the divisor of the pulled-back function (Stichtenoth,
Proposition 3.1.9). This is the step the divisor construction of the Weil pairing runs on: a
function with a prescribed divisor pulls back to one whose divisor is the pullback.
The pullback respects linear equivalence (Stichtenoth, Proposition 3.1.9), so it descends to divisor classes.
Functoriality and divisor classes #
Pulling back along a composite is pulling back twice, in the reverse order (Stichtenoth, Definition 3.1.8): the conorm is transitive in a tower, and the three function-field embeddings form one.
The identity law: pulling back along Isogeny.id changes nothing.
The pullback on divisor classes: the pullback carries principal divisors to principal
divisors, so it descends to a homomorphism Cl(F(W₂)) →+ Cl(F(W₁)).
Equations
Instances For
The pullback on classes is the pullback on divisors, which is what makes the descent usable: a class given by a divisor is carried to the class of its pullback.
The identity law on classes.
Contravariant functoriality on classes, the quotient of divisorPullback_comp.