Coordinate-free places and the two-chart presentation

This file proves that the intrinsic valuation-subring places of a one-dimensional function field are equivalent to the finite/infinite two-chart presentation. The proof restricts a place to k(X), applies Ostrowski's theorem, and recovers the unique height-one centre in the appropriate integral closure.

Main definitions

• FunctionField.Place.ofChart: regard a coordinate place as an intrinsic place.
• FunctionField.Place.toChart: recover a coordinate chart from an intrinsic place.
• FunctionField.chartToPlace: the equivalence between the two presentations.
• FunctionField.placeValuation_isEquiv: compatibility of normalized valuations.

@[instance_reducible]

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

Classical decidable equality for the rational function field used by Ostrowski.

Equations

• FunctionField.instDecidableEqRatFuncPlaceEquiv k = Classical.decEq (RatFunc k)

noncomputable def FunctionField.Place.ofChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : Place k K

A coordinate place, regarded as an intrinsic valuation subring.

Equations

• FunctionField.Place.ofChart k K w = { toValuationSubring := (FunctionField.Chart.placeValuation k K w).valuationSubring, ne_top := ⋯, triv_on_k := ⋯, isDiscrete := ⋯ }

@[simp]

theorem FunctionField.Place.ofChart_toValuationSubring (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : (ofChart k K w).toValuationSubring = (Chart.placeValuation k K w).valuationSubring

theorem FunctionField.Place.ofChart_valuation_isEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : (Chart.placeValuation k K w).IsEquiv (ofChart k K w).valuation

theorem FunctionField.Place.ofChart_valuation_eq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : (ofChart k K w).valuation = Chart.placeValuation k K w

The normalized intrinsic valuation attached to a coordinate place is exactly its coordinate valuation. This strengthens equivalence by using uniqueness of the ordered ℤᵐ⁰ normalization.

theorem FunctionField.Place.finite_X_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] (w : IsDedekindDomain.HeightOneSpectrum ↥(ringOfIntegers k K)) : (IsDedekindDomain.HeightOneSpectrum.valuation K w) ((algebraMap (RatFunc k) K) RatFunc.X) ≤ 1

noncomputable def FunctionField.Place.centerIdeal {R : Type u_3} {L : Type u_4} [CommRing R] [Field L] [Algebra R L] (V : ValuationSubring L) (hR : ∀ (r : R), (algebraMap R L) r ∈ V) : Ideal R

The centre in a Dedekind model of a valuation subring containing that model.

Equations

• FunctionField.Place.centerIdeal V hR = Ideal.comap ((algebraMap R L).codRestrict V hR) (IsLocalRing.maximalIdeal ↥V)

instance FunctionField.Place.centerIdeal_isPrime {R : Type u_3} {L : Type u_4} [CommRing R] [Field L] [Algebra R L] (V : ValuationSubring L) (hR : ∀ (r : R), (algebraMap R L) r ∈ V) : (centerIdeal V hR).IsPrime

noncomputable def FunctionField.Place.center {R : Type u_3} {L : Type u_4} [CommRing R] [Field L] [Algebra R L] (V : ValuationSubring L) (hR : ∀ (r : R), (algebraMap R L) r ∈ V) (hne : centerIdeal V hR ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum R

A nonzero centre is a height-one prime of a Dedekind model.

Equations

• FunctionField.Place.center V hR hne = { asIdeal := FunctionField.Place.centerIdeal V hR, isPrime := ⋯, ne_bot := hne }

theorem FunctionField.Place.valuationSubringAtPrime_center {R : Type u_3} {L : Type u_4} [CommRing R] [IsDedekindDomain R] [Field L] [Algebra R L] [IsFractionRing R L] (V : ValuationSubring L) (hV : V ≠ ⊤) (hR : ∀ (r : R), (algebraMap R L) r ∈ V) (hne : centerIdeal V hR ≠ ⊥) : IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime L (center V hR hne) = V

theorem FunctionField.Place.instTowerConstantsRatFunc (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] : IsScalarTower k (RatFunc k) K

noncomputable def FunctionField.Place.restrict (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (RatFunc k) K] (v : Place k K) : Valuation (RatFunc k) (WithZero (Multiplicative ℤ))

The restriction of an intrinsic place to the rational function subfield.

Equations

• FunctionField.Place.restrict k K v = Valuation.comap (algebraMap (RatFunc k) K) v.valuation

instance FunctionField.Place.restrict_isTrivialOn (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] (v : Place k K) : Valuation.IsTrivialOn k (restrict k K v)

theorem FunctionField.Place.restrict_isNontrivial (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (RatFunc k) K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) : (restrict k K v).IsNontrivial

theorem FunctionField.Place.restrict_classification (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) : Xor ((restrict k K v).IsEquiv (RatFunc.inftyValuation k)) (∃! u : IsDedekindDomain.HeightOneSpectrum (Polynomial k), (restrict k K v).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc k) u))

theorem FunctionField.Place.finiteRing_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] (v : Place k K) (u : IsDedekindDomain.HeightOneSpectrum (Polynomial k)) (h : (restrict k K v).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc k) u)) (r : ↥(ringOfIntegers k K)) : (algebraMap (↥(ringOfIntegers k K)) K) r ∈ v.toValuationSubring

theorem FunctionField.Place.finiteCenter_ne (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) (u : IsDedekindDomain.HeightOneSpectrum (Polynomial k)) (h : (restrict k K v).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc k) u)) : centerIdeal v.toValuationSubring ⋯ ≠ ⊥

theorem FunctionField.Place.infiniteRing_le (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (RatFunc k) K] (v : Place k K) (h : (restrict k K v).IsEquiv (RatFunc.inftyValuation k)) (r : ↥(Chart.infiniteIntegers k K)) : (algebraMap (↥(Chart.infiniteIntegers k K)) K) r ∈ v.toValuationSubring

theorem FunctionField.Place.infiniteCenter_ne (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) (h : (restrict k K v).IsEquiv (RatFunc.inftyValuation k)) : centerIdeal v.toValuationSubring ⋯ ≠ ⊥

theorem FunctionField.Place.infinite_X_gt_one (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : IsDedekindDomain.HeightOneSpectrum ↥(Chart.infiniteIntegers k K)) : 1 < (IsDedekindDomain.HeightOneSpectrum.valuation K w) ((algebraMap (RatFunc k) K) RatFunc.X)

theorem FunctionField.Place.ofChart_injective (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Function.Injective (ofChart k K)

theorem FunctionField.Place.exists_chart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) : ∃ (w : Chart.PlaceA k K), ofChart k K w = v

Every intrinsic place occurs on one of the two coordinate charts.

noncomputable def FunctionField.Place.toChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) : Chart.PlaceA k K

Recover a coordinate chart containing an intrinsic place.

Equations

• FunctionField.Place.toChart k K v = Classical.choose ⋯

theorem FunctionField.Place.ofChart_toChart (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (v : Place k K) : ofChart k K (toChart k K v) = v

noncomputable def FunctionField.Place.chartToPlaceCore (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Chart.PlaceA k K ≃ Place k K

Coordinate places and intrinsic places are equivalent.

Equations

• FunctionField.Place.chartToPlaceCore k K = { toFun := FunctionField.Place.ofChart k K, invFun := FunctionField.Place.toChart k K, left_inv := ⋯, right_inv := ⋯ }

@[reducible, inline]

noncomputable abbrev FunctionField.chartToPlace (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] : Chart.PlaceA k K ≃ Place k K

The equivalence from the two-chart construction to coordinate-free places.

Equations

• FunctionField.chartToPlace k K = FunctionField.Place.chartToPlaceCore k K

@[simp]

theorem FunctionField.chartToPlace_apply (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : (chartToPlace k K) w = Place.ofChart k K w

theorem FunctionField.placeValuation_isEquiv (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : (Chart.placeValuation k K w).IsEquiv ((chartToPlace k K) w).valuation

The coordinate valuation and the normalized intrinsic valuation define the same place.

theorem FunctionField.placeValuation_eq (k : Type u_1) (K : Type u_2) [Field k] [Field K] [Algebra k K] [Algebra (Polynomial k) K] [Algebra (RatFunc k) K] [IsScalarTower k (Polynomial k) K] [IsScalarTower (Polynomial k) (RatFunc k) K] [FunctionField k K] [Algebra.IsSeparable (RatFunc k) K] (w : Chart.PlaceA k K) : ((chartToPlace k K) w).valuation = Chart.placeValuation k K w

Compatibility of the chart and intrinsic normalized valuations.