The affine-model bridge at divisor level #
An affine model of F / k is a Dedekind k-subalgebra R of F whose fraction field is F.
TauCeti/FieldTheory/FunctionField/AffineModel/Prime.lean identifies the places of F / k finite
on R with the height one primes of R, place by place. This file carries that dictionary up to
divisors and divisor classes.
Restricting a divisor of F / k to the finite chart — discarding the coefficients at the places
infinite on R — is a surjective homomorphism Divisor k F →+ WeilDivisor (HeightOneSpectrum R)
onto the divisor group of the model, and it carries div z to the divisor of the principal
fractional ideal generated by z. It therefore descends to divisor classes, where Tau Ceti's
classGroupAddEquiv — the identification of the Weil divisor class group of a Dedekind domain
with Mathlib's ClassGroup R, built from FractionalIdeal.count — turns it into a surjection
Cl(F) →+ Additive (ClassGroup R)
whose kernel is exactly the subgroup generated by the classes of the places infinite on R. That
is the exact sequence ⟨[P] : P ∤ R⟩ → Cl(F) → ClassGroup R → 0: the ideal class group of an
affine model is the divisor class group of F / k with the classes of the places at infinity
killed. The kernel is a subgroup generated by those classes rather than a free group on them,
because a function whose divisor is supported at infinity imposes a relation.
The specialization Mathlib's elliptic curves want closes the file: when the model has a single
place at infinity and that place is rational, the surjection restricts to an isomorphism
Cl⁰(F) ≃+ ClassGroup R from the degree-zero class group.
Restriction is split by pushforward along TauCeti.Place.ofPrime, so the divisor group of the
model sits inside Divisor k F as the divisors supported on the finite chart; composing with Tau
Ceti's fractionalIdealDivisorAddEquiv turns divisors of the model into invertible fractional
ideals, so no fractional-ideal calculus is redeveloped here.
This is the affine-model bridge of Stichtenoth's Section I.4: the Dedekind factorization calculus of the model computes divisors on its chart.
Main definitions #
TauCeti.Divisor.restrict: restriction of a divisor ofF / kto the finite chart of a model.TauCeti.Divisor.classGroupHom: the induced map from the divisor class group ofF / kto the ideal class group of the model.TauCeti.Divisor.degreeZeroClassGroupEquiv: the isomorphismCl⁰(F) ≃+ ClassGroup Rfor a model whose only place at infinity is rational.
Main results #
TauCeti.Divisor.restrict_principal: restriction carries principal divisors to principal divisors.TauCeti.Divisor.classGroupHom_surjective: the induced map on class groups is surjective.TauCeti.Divisor.ker_classGroupHom: its kernel is generated by the classes of the places infinite on the model.TauCeti.Divisor.exists_degreeClass_mem_Ico_and_classGroupHom_eq: every ideal class of the model is the image of a divisor class whose degree lies in[0, deg P), for any placePinfinite on the model.TauCeti.Divisor.classGroupHom_comp_subtype_surjective: if some place infinite on the model is rational, thenCl⁰(F)already surjects onto the ideal class group of the model.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.4 and III.2.
Restriction to the finite chart #
Restriction of a divisor to the finite chart of an affine model R: the coefficient at a
height one prime 𝔭 of R is the coefficient at the place of 𝔭, and the coefficients at the
places infinite on R are discarded.
Instances For
A place at which some element of the model has a pole contributes nothing to the finite chart.
Restriction carries principal divisors to principal divisors. The order at the place of a
height one prime 𝔭 is the 𝔭-adic order, because the place of 𝔭 has the 𝔭-adic valuation
on the nose; so div z restricts to the divisor of the principal fractional ideal of z.
The order-system form of TauCeti.Divisor.restrict_principal.
The class group of the model as a quotient #
The ideal class group of an affine model, as a quotient of the divisor class group of
F / k: the map induced by restriction to the finite chart, read through the identification
TauCeti.AlgebraicGeometry.WeilDivisor.classGroupAddEquiv of the Weil divisor class group of a
Dedekind domain with Mathlib's ClassGroup.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The class of a place finite on the model goes to the ideal class of the corresponding height
one prime. This is the non-vacuity of TauCeti.Divisor.classGroupHom.
The class of a place infinite on the model dies in the ideal class group of the model.
Every ideal class of an affine model comes from a divisor class of F / k.
The kernel of the class-group surjection is generated by the classes of the places infinite
on the model: the sequence ⟨[P] : P ∤ R⟩ → Cl(F) → ClassGroup R → 0 is exact. It is the
subgroup generated by those classes, not a free group on them: a function whose divisor is
supported at infinity imposes a relation.
Every ideal class of an affine model comes from a divisor class of bounded degree. Fix a
place P infinite on R; its class dies in the ideal class group of the model, so a preimage of
an ideal class may be corrected by an integer multiple of [P] without changing its image, and
the multiple can be chosen to move its degree into [0, deg P).
This is what makes the ideal class group of a model a quotient of finitely many degree classes:
over a finite constant field each of those degree classes is a coset of the finite group Cl⁰(F).
With a rational place at infinity, every ideal class of the model comes from a degree-zero
divisor class: the bounded-degree representative above then has degree in [0, 1), hence degree
zero. Uniqueness of the place at infinity is not needed.
With a rational place at infinity, the ideal class group of the model is a quotient of
Cl⁰(F). Uniqueness of the place at infinity is not needed; with it, the map is also injective
and TauCeti.Divisor.degreeZeroClassGroupEquiv upgrades it to an isomorphism.
A model with a single rational place at infinity #
With a single place at infinity, the kernel of the class-group surjection is the group of integer multiples of the class of that place.
The class of the single place at infinity dies in the ideal class group of the model.
With a single rational place at infinity, the class-group map is injective on degree-zero classes: such a class in the kernel is an integer multiple of the class of the place at infinity, and its degree reads off that integer.
The degree-zero class group of F / k is the ideal class group of a model whose only place
at infinity is rational — the form Mathlib's elliptic curves need, Cl⁰(F) ≅ ClassGroup R.
Equations
- TauCeti.Divisor.degreeZeroClassGroupEquiv R hF hP hdeg = AddEquiv.ofBijective ((TauCeti.Divisor.classGroupHom R hF).comp (TauCeti.Divisor.degreeClass hF).ker.subtype) ⋯