Places attached to the height-one primes of a Dedekind model

Let k be a field and R a Dedekind domain which is a k-algebra, with fraction field F. Every height-one prime p of R gives a place of F / k: the normalized p-adic valuation is surjective onto ℤᵐ⁰ by IsDedekindDomain.HeightOneSpectrum.valuation_surjective, and it is trivial on k because the nonzero constants are units of R. Distinct primes give distinct places, and the residue field of the place is the residue field R ⧸ p of the prime, so the degree of the place is [R ⧸ p : k].

This is the affine half of the place vocabulary: applied to R = k[X] and F = k(x) it produces the finite places of the rational function field (Stichtenoth, Algebraic Function Fields and Codes, second edition, Proposition 1.2.1(a)), and applied to the integral closure of k[x] in a function field it produces the places of a chosen affine model.

Main definitions

• TauCeti.Place.ofPrime: the place of F / k attached to a height-one prime of R.
• TauCeti.Place.integersOfPrimeEquiv: the valuation ring of that place is the localization of R at p.

Reduction R → F_P at an adic place is the canonical map algebraMap R (TauCeti.Place.ofPrime k F p).ResidueField.

Main results

• TauCeti.Place.ofPrime_injective: distinct height-one primes give distinct places.
• TauCeti.Place.quotientAlgEquivResidueFieldOfPrime: the residue field of Place.ofPrime k F p is R ⧸ p, as a k-algebra. TauCeti.Place.quotientAlgEquivResidueFieldOfPrime_mk computes this equivalence on quotient representatives, and TauCeti.Place.degree_ofPrime reads off the degree of the place. The valuation ring is the localization of R at p, so this is Mathlib's IsLocalization.AtPrime.equivQuotMaximalIdeal.
• TauCeti.Place.ord_ofPrime_algebraMap: the order of r : R at the place is the multiplicity of p in (r); TauCeti.Place.isUniformizer_ofPrime_algebraMap specializes this to a generator of p, which is therefore a prime element for the place.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Sections I.1 and III.2.
• The adic valuation of a height-one prime, its valuation subring and the identification of that subring with the localization at the prime are Mathlib/RingTheory/DedekindDomain/AdicValuation.lean (María Inés de Frutos-Fernández); the residue field of a localization at a prime is Mathlib/RingTheory/Localization/AtPrime/Basic.lean.

noncomputable def TauCeti.Place.ofPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : Place k F

The place of F / k attached to a height-one prime p of a Dedekind k-algebra R with fraction field F: the normalized p-adic valuation.

Equations

• TauCeti.Place.ofPrime k F p = { valuation := IsDedekindDomain.HeightOneSpectrum.valuation F p, valuation_surjective := ⋯, isTrivialOn := ⋯ }

@[simp]

theorem TauCeti.Place.valuation_ofPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : (ofPrime k F p).valuation = IsDedekindDomain.HeightOneSpectrum.valuation F p

theorem TauCeti.Place.integers_ofPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : (ofPrime k F p).integers = IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F p

theorem TauCeti.Place.ofPrime_injective (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] : Function.Injective (ofPrime k F)

Distinct height-one primes give distinct places: the place remembers its prime.

Orders of elements of R

theorem TauCeti.Place.algebraMap_mem_integers_ofPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (r : R) : (algebraMap R F) r ∈ (ofPrime k F p).integers

theorem TauCeti.Place.valuation_ofPrime_algebraMap (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (r : R) : (ofPrime k F p).valuation ((algebraMap R F) r) = p.intValuation r

The valuation of the place of p extends the p-adic valuation of the model.

theorem TauCeti.Place.valuation_ofPrime_algebraMap_lt_one_iff (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) {r : R} : (ofPrime k F p).valuation ((algebraMap R F) r) < 1 ↔ r ∈ p.asIdeal

The elements of the model with a zero at the place of p are exactly the elements of p.

theorem TauCeti.Place.ord_ofPrime_algebraMap_nonneg (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (r : R) : 0 ≤ (ofPrime k F p).ord ((algebraMap R F) r)

theorem TauCeti.Place.ord_ofPrime_algebraMap_pos_iff_mem (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r ≠ 0) : 0 < (ofPrime k F p).ord ((algebraMap R F) r) ↔ r ∈ p.asIdeal

An element of R has positive order at ofPrime k F p exactly when it lies in p.

theorem TauCeti.Place.ord_ofPrime_algebraMap (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r ≠ 0) : (ofPrime k F p).ord ((algebraMap R F) r) = ↑(multiplicity p.asIdeal (Ideal.span {r}))

The order of an element of R at the place ofPrime k F p is the multiplicity of p in the principal ideal it generates.

theorem TauCeti.Place.isUniformizer_ofPrime_algebraMap (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) {π : R} (h : p.asIdeal = Ideal.span {π}) : (ofPrime k F p).valuation.IsUniformizer ((algebraMap R F) π)

A generator of p is a prime element for the place ofPrime k F p, i.e. a uniformizer for its normalized valuation.

The residue field

@[instance_reducible]

noncomputable instance TauCeti.Place.instAlgebraSubtypeMemValuationSubringIntegersOfPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : Algebra R ↥(ofPrime k F p).integers

R maps into the valuation ring of ofPrime k F p: every element is integral there.

Equations

• TauCeti.Place.instAlgebraSubtypeMemValuationSubringIntegersOfPrime k F p = ((algebraMap R F).codRestrict (TauCeti.Place.ofPrime k F p).integers ⋯).toAlgebra

instance TauCeti.Place.instIsScalarTowerSubtypeMemValuationSubringIntegersOfPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : IsScalarTower R (↥(ofPrime k F p).integers) F

instance TauCeti.Place.instIsScalarTowerSubtypeMemValuationSubringIntegersOfPrime_1 (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : IsScalarTower k R ↥(ofPrime k F p).integers

noncomputable def TauCeti.Place.integersOfPrimeEquiv (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F p) ≃ₐ[R] ↥(ofPrime k F p).integers

The valuation ring of an adic place is the localization at its prime, by IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime_eq_valuationSubring.

Equations

• TauCeti.Place.integersOfPrimeEquiv k F p = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem TauCeti.Place.integersOfPrimeEquiv_apply (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime F p)) : ↑((integersOfPrimeEquiv k F p) x) = ↑x

The equivalence from the localization at p to the integers of the adic place preserves the underlying element of F.

instance TauCeti.Place.instAtPrimeSubtypeMemValuationSubringIntegersOfPrimeAsIdeal (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : IsLocalization.AtPrime (↥(ofPrime k F p).integers) p.asIdeal

@[simp]

theorem TauCeti.Place.algebraMap_residueField_ofPrime_eq_zero_iff {k : Type u} {F : Type v} {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] {p : IsDedekindDomain.HeightOneSpectrum R} {r : R} : (algebraMap R (ofPrime k F p).ResidueField) r = 0 ↔ r ∈ p.asIdeal

Reduction from R at an adic place vanishes exactly on its prime ideal.

noncomputable def TauCeti.Place.quotientAlgEquivResidueFieldOfPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : (R ⧸ p.asIdeal) ≃ₐ[k] (ofPrime k F p).ResidueField

The residue field of an adic place is the residue field of its prime: reduction at ofPrime k F p identifies R ⧸ p with F_P, as k-algebras. Its valuation ring is the localization of R at p, so this is Mathlib's IsLocalization.AtPrime.equivQuotMaximalIdeal, restricted from R to k.

Equations

• TauCeti.Place.quotientAlgEquivResidueFieldOfPrime k F p = AlgEquiv.restrictScalars k (IsLocalization.AtPrime.equivQuotMaximalIdeal p.asIdeal ↥(TauCeti.Place.ofPrime k F p).integers)

@[simp]

theorem TauCeti.Place.quotientAlgEquivResidueFieldOfPrime_mk (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) (r : R) : (quotientAlgEquivResidueFieldOfPrime k F p) ((Ideal.Quotient.mk p.asIdeal) r) = (algebraMap R (ofPrime k F p).ResidueField) r

theorem TauCeti.Place.degree_ofPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) : (ofPrime k F p).degree = Module.finrank k (R ⧸ p.asIdeal)

The degree of an adic place is the degree of the residue field of its prime.

instance TauCeti.Place.finiteDimensional_residueField_ofPrime (k : Type u) (F : Type v) {R : Type w} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (p : IsDedekindDomain.HeightOneSpectrum R) [Module.Finite k (R ⧸ p.asIdeal)] : Module.Finite k (ofPrime k F p).ResidueField