Coordinate places of a function field

This file gives the coordinate presentation of the places of a finite separable extension of k(X). Finite places are the height-one primes of the integral closure of k[X]; infinite places are the height-one primes of the integral closure of the valuation subring at infinity.

Main definitions

• FunctionField.inftyValuationSubring: the valuation subring at infinity of k(X).
• FunctionField.infiniteIntegers: its integral closure in a function field K.
• FunctionField.PlaceA: the sum of the finite and infinite height-one spectra.
• FunctionField.placeValuation: the valuation of a coordinate place.
• FunctionField.DivisorA: divisors in the coordinate presentation.
• FunctionField.principalDivisorA: the principal divisor on both coordinate charts.

theorem FractionalIdeal.valuation_eq_exp_neg_count {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : Kˣ) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x = WithZero.exp (-count K v (spanSingleton (nonZeroDivisors R) ↑x))

The multiplicative adic valuation of a nonzero element is the exponential of the negative coefficient of its principal fractional ideal.

theorem RatFunc.exists_sub_C_intDegree_neg {k : Type u_1} [Field k] (z : RatFunc k) (hzdeg : z.intDegree ≤ 0) : ∃ (c : k), z - C c = 0 ∨ (z - C c).intDegree < 0

A rational function regular at infinity has a unique constant residue: after subtracting the ratio of the leading coefficients of its numerator and denominator, its degree at infinity is strictly negative (unless the difference is zero).

theorem FunctionField.orderMonoidIso_withZeroMulInt_eq_refl (e : WithZero (Multiplicative ℤ) ≃*o WithZero (Multiplicative ℤ)) : e = OrderMonoidIso.refl (WithZero (Multiplicative ℤ))

A normalized discrete rank-one value group has a unique order-preserving normalization.

theorem FunctionField.orderMonoidIso_withZeroMulInt_unique {G : Type u_3} [LinearOrderedCommGroupWithZero G] (e f : G ≃*o WithZero (Multiplicative ℤ)) : e = f

Any two order-preserving normalizations of the same value group are equal.

structure FunctionField.Place (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] : Type u_2

A coordinate-free place of K/k: a nontrivial valuation subring of K containing the constant field, together with the proposition that its value group admits the discrete rank-one normalization. The normalization is stored only through Nonempty, so a place is determined by its valuation subring rather than by a choice of uniformizer.

• toValuationSubring : ValuationSubring K

  The valuation subring underlying the place.

• ne_top : self.toValuationSubring ≠ ⊤

  A place is nontrivial.

• triv_on_k (c : k) : (algebraMap k K) c ∈ self.toValuationSubring

  Constants are integral at every place.

• isDiscrete : Nonempty ((MonoidWithZeroHom.ofClass self.toValuationSubring.valuation).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ))

  The value group is discrete of rank one, expressed without choosing a normalization.

theorem FunctionField.Place.ext {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] {v w : Place k K} (h : v.toValuationSubring = w.toValuationSubring) : v = w

Two places are equal when their valuation subrings are equal.

theorem FunctionField.Place.ext_iff {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] {v w : Place k K} : v = w ↔ v.toValuationSubring = w.toValuationSubring

@[instance_reducible]

instance FunctionField.Place.instSetLike {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] : SetLike (Place k K) K

Places inherit the membership coercion of their valuation subrings.

Equations

• FunctionField.Place.instSetLike = { coe := fun (v : FunctionField.Place k K) => ↑v.toValuationSubring, coe_injective := ⋯ }

@[simp]

theorem FunctionField.Place.mem_toValuationSubring {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) (x : K) : x ∈ v.toValuationSubring ↔ x ∈ v

noncomputable def FunctionField.Place.normalization {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : (MonoidWithZeroHom.ofClass v.toValuationSubring.valuation).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ)

A normalization of the value group of a coordinate-free place.

Equations

• v.normalization = Classical.choice ⋯

noncomputable def FunctionField.Place.valuation {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : Valuation K (WithZero (Multiplicative ℤ))

The normalized ℤᵐ⁰-valued valuation associated to a coordinate-free place.

Equations

• v.valuation = Valuation.map v.normalization.toMonoidWithZeroHom ⋯ v.toValuationSubring.valuation.restrict

theorem FunctionField.Place.valuation_isEquiv_canonical {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : v.valuation.IsEquiv v.toValuationSubring.valuation

The normalized valuation is equivalent to the canonical valuation of the valuation subring.

@[simp]

theorem FunctionField.Place.valuationSubring_valuation {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : v.valuation.valuationSubring = v.toValuationSubring

Recovering the valuation subring from the normalized valuation gives the original place.

instance FunctionField.Place.valuation_isTrivialOn {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : Valuation.IsTrivialOn k v.valuation

The normalized valuation of a place is trivial on the constant field.

instance FunctionField.Place.valuation_isNontrivial {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : v.valuation.IsNontrivial

The normalized valuation of a place is nontrivial.

@[instance_reducible]

instance FunctionField.Place.algebraValuationSubring {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : Algebra k ↥v.toValuationSubring

The valuation ring itself, viewed as a k-algebra.

Equations

• v.algebraValuationSubring = ((algebraMap k K).codRestrict v.toValuationSubring ⋯).toAlgebra

@[reducible, inline]

abbrev FunctionField.Place.residueField {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : Type u_4

The residue field of a coordinate-free place.

Equations

• v.residueField = IsLocalRing.ResidueField ↥v.toValuationSubring

noncomputable def FunctionField.Place.degree {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] (v : Place k K) : ℕ

The intrinsic degree of a place is the dimension of its residue field over k.

Equations

• v.degree = Module.finrank k v.residueField

@[instance_reducible]

noncomputable def FunctionField.Chart.instDecidableEqRatFuncRiemannRoch (k : Type u_1) [Field k] : DecidableEq (RatFunc k)

The classical decidable equality used to define the valuation at infinity.

Equations

• FunctionField.Chart.instDecidableEqRatFuncRiemannRoch k = Classical.decEq (RatFunc k)

@[reducible, inline]

noncomputable abbrev FunctionField.Chart.inftyValuationSubring (k : Type u_1) [Field k] : ValuationSubring (RatFunc k)

The valuation subring at infinity of the rational function field k(X).

Equations

• FunctionField.Chart.inftyValuationSubring k = (RatFunc.inftyValuation k).valuationSubring

instance FunctionField.Chart.inftyValuationSubring.instIsDedekindDomainSubtypeRatFuncMemValuationSubring (k : Type u_1) [Field k] : IsDedekindDomain ↥(inftyValuationSubring k)

@[instance_reducible]

noncomputable instance FunctionField.Chart.inftyValuationSubring.instAlgebraSubtypeRatFuncMemValuationSubring (k : Type u_1) [Field k] : Algebra k ↥(inftyValuationSubring k)

Equations

• FunctionField.Chart.inftyValuationSubring.instAlgebraSubtypeRatFuncMemValuationSubring k = (RatFunc.C.codRestrict (FunctionField.Chart.inftyValuationSubring k) ⋯).toAlgebra

@[instance_reducible]

noncomputable def FunctionField.Chart.inftyValuationSubring.instFieldQuotientSubtypeRatFuncMemValuationSubringIdealMaximalIdeal (k : Type u_1) [Field k] : Field (↥(inftyValuationSubring k) ⧸ IsLocalRing.maximalIdeal ↥(inftyValuationSubring k))

The residue field at infinity.

Equations

• One or more equations did not get rendered due to their size.

theorem FunctionField.Chart.inftyValuationSubring.residue_algebraMap_surjective (k : Type u_1) [Field k] : Function.Surjective ⇑(algebraMap k (↥(inftyValuationSubring k) ⧸ IsLocalRing.maximalIdeal ↥(inftyValuationSubring k)))

The residue map at infinity is onto the constant field.

noncomputable def FunctionField.Chart.inftyValuationSubring.residueAlgEquiv (k : Type u_1) [Field k] : k ≃ₐ[k] ↥(inftyValuationSubring k) ⧸ IsLocalRing.maximalIdeal ↥(inftyValuationSubring k)

The residue field of the valuation ring at infinity is canonically the constant field.

Equations

• One or more equations did not get rendered due to their size.

instance FunctionField.Chart.inftyValuationSubring.finiteDimensionalResidueField (k : Type u_1) [Field k] : FiniteDimensional k (↥(inftyValuationSubring k) ⧸ IsLocalRing.maximalIdeal ↥(inftyValuationSubring k))

@[simp]

theorem FunctionField.Chart.inftyValuationSubring.finrank_residueField (k : Type u_1) [Field k] : Module.finrank k (↥(inftyValuationSubring k) ⧸ IsLocalRing.maximalIdeal ↥(inftyValuationSubring k)) = 1

@[reducible, inline]

noncomputable abbrev FunctionField.Chart.infiniteIntegers (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : Subalgebra (↥(inftyValuationSubring k)) K

The integral closure in K of the valuation subring at infinity of k(X).

Equations

• FunctionField.Chart.infiniteIntegers k K = integralClosure (↥(FunctionField.Chart.inftyValuationSubring k)) K

instance FunctionField.Chart.infiniteIntegers.isTorsionFreeOverInfinityRing (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : Module.IsTorsionFree ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)

instance FunctionField.Chart.infiniteIntegers.instIsFractionRingSubtypeMemSubalgebraRatFuncValuationSubringInftyValuationSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] : IsFractionRing (↥(infiniteIntegers k K)) K

instance FunctionField.Chart.infiniteIntegers.instIsDedekindDomainSubtypeMemSubalgebraRatFuncValuationSubringInftyValuationSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : IsDedekindDomain ↥(infiniteIntegers k K)

instance FunctionField.Chart.infiniteIntegers.instFiniteSubtypeRatFuncMemValuationSubringInftyValuationSubringSubalgebra (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Module.Finite ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)

@[instance_reducible]

noncomputable instance FunctionField.Chart.infiniteIntegers.instAlgebraSubtypeMemSubalgebraRatFuncValuationSubringInftyValuationSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : Algebra k ↥(infiniteIntegers k K)

Equations

• One or more equations did not get rendered due to their size.

instance FunctionField.Chart.infiniteIntegers.instIsScalarTowerSubtypeRatFuncMemValuationSubringInftyValuationSubringSubalgebra (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] : IsScalarTower k ↥(inftyValuationSubring k) ↥(infiniteIntegers k K)

instance FunctionField.Chart.ringOfIntegers.isTorsionFreeOverPolynomial (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : Module.IsTorsionFree (Polynomial k) ↥(ringOfIntegers k K)

@[instance_reducible]

noncomputable instance FunctionField.Chart.ringOfIntegers.algebraOverConstants (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] : Algebra k ↥(ringOfIntegers k K)

Equations

• FunctionField.Chart.ringOfIntegers.algebraOverConstants k K = ((algebraMap (Polynomial k) ↥(FunctionField.ringOfIntegers k K)).comp (algebraMap k (Polynomial k))).toAlgebra

instance FunctionField.Chart.ringOfIntegers.isScalarTowerConstants (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] : IsScalarTower k (Polynomial k) ↥(ringOfIntegers k K)

instance FunctionField.Chart.ringOfIntegers.finiteTypeOverConstants (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Algebra.FiniteType k ↥(ringOfIntegers k K)

instance FunctionField.Chart.ringOfIntegers.moduleFiniteOverPolynomial (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Module.Finite (Polynomial k) ↥(ringOfIntegers k K)

@[reducible, inline]

abbrev FunctionField.Chart.PlaceA (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : Type u_2

Coordinate places of K: finite places on the k[X] chart and places above infinity.

Equations

• FunctionField.Chart.PlaceA k K = (IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.ringOfIntegers k K) ⊕ IsDedekindDomain.HeightOneSpectrum ↥(FunctionField.Chart.infiniteIntegers k K))

noncomputable def FunctionField.Chart.placeValuation (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : PlaceA k K → Valuation K (WithZero (Multiplicative ℤ))

The discrete valuation associated to a coordinate place.

Equations

• FunctionField.Chart.placeValuation k K (Sum.inl v) = IsDedekindDomain.HeightOneSpectrum.valuation K v
• FunctionField.Chart.placeValuation k K (Sum.inr v) = IsDedekindDomain.HeightOneSpectrum.valuation K v

@[reducible, inline]

abbrev FunctionField.Chart.DivisorA (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] : Type u_2

Divisors on K in the two-chart coordinate presentation.

Equations

• FunctionField.Chart.DivisorA k K = (FunctionField.Chart.PlaceA k K →₀ ℤ)

instance FunctionField.Chart.PlaceA.finiteDimensionalResidueFieldFinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : FiniteDimensional k (↥(ringOfIntegers k K) ⧸ v.asIdeal)

The residue field at a finite coordinate place is finite-dimensional over the constant field.

instance FunctionField.Chart.PlaceA.finiteDimensionalResidueFieldInfinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : FiniteDimensional k (↥(infiniteIntegers k K) ⧸ v.asIdeal)

The residue field at an infinite coordinate place is finite-dimensional over the constant field.

noncomputable def FunctionField.Chart.PlaceA.finiteDegree (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] (v : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : ℕ

The degree of a finite coordinate place over the constant field.

Equations

• FunctionField.Chart.PlaceA.finiteDegree k K v = Module.finrank k (↥(FunctionField.ringOfIntegers k K) ⧸ v.asIdeal)

noncomputable def FunctionField.Chart.principalDivisorA (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Additive Kˣ →+ DivisorA k K

The principal divisor of a nonzero function, combining its finite and infinite parts.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FunctionField.Chart.principalDivisorA_apply_finite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Additive Kˣ) (v : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : ((principalDivisorA k K) x) (Sum.inl v) = (FractionalIdeal.principalDivisor x) v

@[simp]

theorem FunctionField.Chart.principalDivisorA_apply_infinite (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Additive Kˣ) (v : IsDedekindDomain.HeightOneSpectrum ↥(infiniteIntegers k K)) : ((principalDivisorA k K) x) (Sum.inr v) = (FractionalIdeal.principalDivisor x) v

theorem FunctionField.Chart.placeValuation_eq_exp_neg_principalDivisor (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (x : Additive Kˣ) (v : PlaceA k K) : (placeValuation k K v) ↑(Additive.toMul x) = WithZero.exp (-((principalDivisorA k K) x) v)

A principal-divisor coefficient is the negative logarithm of the corresponding valuation.

instance FunctionField.Chart.ringOfIntegers.isScalarTowerConstantsFractions (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : IsScalarTower k (↥(ringOfIntegers k K)) K

instance FunctionField.Chart.infiniteIntegers.isScalarTowerConstantsFractions (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] : IsScalarTower k (↥(infiniteIntegers k K)) K

theorem FunctionField.Chart.placeValuation_algebraMap_le_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (v : PlaceA k K) (c : k) : (placeValuation k K v) ((algebraMap k K) c) ≤ 1

Constants have valuation at most one at every coordinate place.

theorem FunctionField.Chart.placeValuation_algebraMap_eq_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (v : PlaceA k K) (c : kˣ) : (placeValuation k K v) ((algebraMap k K) ↑c) = 1

A nonzero constant has trivial valuation at every coordinate place.

@[simp]

theorem FunctionField.Chart.principalDivisorA_algebraMap (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] [Algebra k K] [IsScalarTower k (Polynomial k) K] (c : kˣ) : (principalDivisorA k K) (Additive.ofMul ((Units.map ↑(algebraMap k K)) c)) = 0

Multiplying by a nonzero constant does not change a principal divisor.