Affine models: the place of a height one prime, and the two-way correspondence #
An affine model of F / k is a Dedekind k-subalgebra R of F whose fraction field is F.
TauCeti/FieldTheory/FunctionField/AffineModel/Place.lean sends a place of F / k that is finite
on R to a height one prime of R, its centre. The converse construction,
TauCeti.Place.ofPrime, and its order and residue-field API live in
TauCeti/FieldTheory/FunctionField/Place/Adic.lean. This file proves that the two constructions
are mutually inverse and packages the correspondence as a bijection
{P : Place k F | R โ ๐ช_P} โ HeightOneSpectrum R.
The correspondence is then made quantitative. On R the order function of the place of ๐ญ is
the multiplicity of ๐ญ in a principal ideal, so divisor coefficients on the finite chart are read
off from Mathlib's factorization calculus; and the residue field of the place of ๐ญ is R โงธ ๐ญ,
so the degree of the place is the residue degree [R โงธ ๐ญ : k] of the prime. Together these say
that divisor theory on the finite chart of a model is exactly the ideal theory of the model.
Holomorphy rings supply the examples: once ๐ช_S is a Dedekind domain with fraction field F โ
which TauCeti.isPrincipalIdealRing_holomorphyRing and TauCeti.isFractionRing_holomorphyRing
give for a finite S omitting some place โ its finite chart is S itself, so the correspondence
above becomes the bijection S โ HeightOneSpectrum ๐ช_S.
Main definitions #
TauCeti.Place.residueHom: evaluation of the elements of the model at a place finite on it, ak-algebra mapR โ F_Pwhose kernel is the centre of the place (TauCeti.Place.ker_residueHom).TauCeti.Place.heightOneSpectrumEquiv: the bijection between the places finite on a model and the height one primes of the model.TauCeti.holomorphyRingHeightOneSpectrumEquiv: that bijection for the model๐ช_S, whose finite chart isS, as the identification ofSwith the height one primes of๐ช_S.
Main results #
TauCeti.Place.center_ofPrimeandTauCeti.Place.ofPrime_center: the two constructions are mutually inverse, andTauCeti.Place.exists_eq_ofPrime_iffidentifies the places in the image as exactly the places finite on the model, withTauCeti.Place.range_ofPrimeandTauCeti.Place.compl_range_ofPrimethe same statement for the finite chart and its complement as sets of places.TauCeti.Place.quotientAlgEquivResidueField: the residue field of a place finite on the model isRmodulo the centre of the place, whenceTauCeti.Place.degree_eq_finrank_quotient_center; the corresponding formulas atTauCeti.Place.ofPrimeare supplied by the basic adic-place API.
References #
- H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.1 and III.2.
The centre on R of the place of a height one prime ๐ญ of R is ๐ญ itself.
The place of the centre on R of a place finite on R is that place.
The places of F / k finite on an affine model R are exactly the height one primes of
R (Stichtenoth, Section III.2): the centre of a place and the adic place of a prime are
mutually inverse bijections.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A place of F / k is the place of a height one prime of an affine model R exactly when
it is finite on R: the image of TauCeti.Place.ofPrime is the finite chart of the model.
The finite chart of an affine model, as a set of places: the image of
TauCeti.Place.ofPrime consists of the places finite on R.
The places infinite on an affine model are the complement of its finite chart: a place
lies outside the image of TauCeti.Place.ofPrime exactly when some element of the model has a
pole there.
Evaluation of the elements of an affine model at a place finite on it, as a map of
k-algebras R โ F_P. It is surjective with kernel the centre of the place, which is the
content of TauCeti.Place.quotientAlgEquivResidueField.
Equations
- P.residueHom hR = { toRingHom := (IsLocalRing.residue โฅP.integers).comp ((algebraMap R F).codRestrict P.integers hR), commutes' := โฏ }
Instances For
The kernel of evaluation at P is the centre of P on the model: this is the
evaluation-map form of TauCeti.Place.mem_center_asIdeal, which says the same thing about the
valuation of P.
Every residue at a place finite on an affine model is the residue of an element of the
model. This is Mathlib's approximation theorem for the adic valuation of the centre, at the
accuracy 1: a function integral at the place is within 1 of an element of the model, so the
two have the same residue.
The residue field of a place finite on an affine model is the model modulo the centre of
the place, as k-algebras.
Equations
Instances For
The degree of a place finite on an affine model is the residue degree of its centre: the weight a divisor attaches to a place of the finite chart is the one Mathlib's ideal theory attaches to the corresponding prime.
Holomorphy rings as affine models #
The height one primes of the affine model ๐ช_S are the places of S. Once ๐ช_S is a
Dedekind domain with fraction field F โ which TauCeti.isPrincipalIdealRing_holomorphyRing and
TauCeti.isFractionRing_holomorphyRing supply for a finite S avoiding at least one place โ the
finite chart of the model ๐ช_S is exactly S by
TauCeti.forall_algebraMap_mem_integers_holomorphyRing_iff, so this is
TauCeti.Place.heightOneSpectrumEquiv for ๐ช_S, read along that identification of subtypes.