The place at infinity and its primes in finite extensions

This file realizes the place at infinity of K(X) as an honest height-one prime. Its base ring is the integer ring of RatFunc.inftyValuation; this is a discrete valuation ring with uniformizer X⁻¹. The resulting fractional-ideal order is proved to equal the previously defined ratFuncInfinityOrder = -intDegree.

For a finite separable extension L / K(X), the integral closure of the infinity valuation ring is Dedekind and finite over the base. The final theorem specializes the finite-extension norm/count formula to the unique base prime, producing the residue-degree-weighted sum over all primes above infinity.

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.RatFuncInfinityIntegers (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : Subring (RatFunc K)

The valuation ring of the place at infinity of K(X).

Equations

• BGS.CorvajaZannier.RatFuncInfinityIntegers K = (RatFunc.inftyValuation K).integer

instance BGS.CorvajaZannier.instIsDiscreteValuationRingSubtypeRatFuncMemSubringRatFuncInfinityIntegers (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : IsDiscreteValuationRing ↥(RatFuncInfinityIntegers K)

instance BGS.CorvajaZannier.instIsDedekindDomainSubtypeRatFuncMemSubringRatFuncInfinityIntegers (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : IsDedekindDomain ↥(RatFuncInfinityIntegers K)

noncomputable def BGS.CorvajaZannier.ratFuncInfinityPlace (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : IsDedekindDomain.HeightOneSpectrum ↥(RatFuncInfinityIntegers K)

The unique height-one prime of the infinity valuation ring.

Equations

• BGS.CorvajaZannier.ratFuncInfinityPlace K = IsDiscreteValuationRing.maximalIdeal ↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)

noncomputable def BGS.CorvajaZannier.ratFuncInfinityUniformizer (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : ↥(RatFuncInfinityIntegers K)

X⁻¹ as an element of the infinity valuation ring.

Equations

• BGS.CorvajaZannier.ratFuncInfinityUniformizer K = ⟨1 / RatFunc.X, ⋯⟩

theorem BGS.CorvajaZannier.ratFuncInfinityUniformizer_isUniformizer (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : (RatFunc.inftyValuation K).IsUniformizer ↑(ratFuncInfinityUniformizer K)

theorem BGS.CorvajaZannier.ratFuncInfinityPlace_span_uniformizer (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : (ratFuncInfinityPlace K).asIdeal = Ideal.span {ratFuncInfinityUniformizer K}

noncomputable def BGS.CorvajaZannier.ratFuncInfinityFractionRingEquiv (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] : FractionRing ↥(RatFuncInfinityIntegers K) ≃ₐ[↥(RatFuncInfinityIntegers K)] RatFunc K

The canonical fraction field of the infinity valuation ring, identified with the usual rational-function field.

Equations

• BGS.CorvajaZannier.ratFuncInfinityFractionRingEquiv K = FractionRing.algEquiv (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) (RatFunc K)

theorem BGS.CorvajaZannier.ratFuncInfinityFractionRingEquiv_valuation (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (x : FractionRing ↥(RatFuncInfinityIntegers K)) : (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (ratFuncInfinityPlace K)) ((ratFuncInfinityFractionRingEquiv K) x) = (IsDedekindDomain.HeightOneSpectrum.valuation (FractionRing ↥(RatFuncInfinityIntegers K)) (ratFuncInfinityPlace K)) x

The height-one valuation is unchanged by the canonical identification of the fraction field of the infinity valuation ring with K(X).

theorem BGS.CorvajaZannier.ratFuncInfinityPlace_order_eq (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (f : RatFunc K) (hf : f ≠ 0) : finitePlaceOrder (ratFuncInfinityPlace K) f = ratFuncInfinityOrder f

The height-one-prime order on the infinity valuation ring agrees with the usual rational-function order -intDegree.

theorem BGS.CorvajaZannier.ratFuncInfinityFractionRing_order_eq (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (x : FractionRing ↥(RatFuncInfinityIntegers K)) (hx : x ≠ 0) : finitePlaceOrder (ratFuncInfinityPlace K) x = ratFuncInfinityOrder ((ratFuncInfinityFractionRingEquiv K) x)

In the canonical FractionRing model used by the norm/count theorem, the height-one-prime count still equals the ordinary rational-function order at infinity after applying the canonical field equivalence.

@[reducible, inline]

noncomputable abbrev BGS.CorvajaZannier.RatFuncInfinityIntegralClosure (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Subalgebra (↥(RatFuncInfinityIntegers K)) L

The integral closure in a finite extension at the infinity valuation ring.

Equations

• BGS.CorvajaZannier.RatFuncInfinityIntegralClosure K L = integralClosure (↥(BGS.CorvajaZannier.RatFuncInfinityIntegers K)) L

theorem BGS.CorvajaZannier.infinityIntegralClosureModuleFinite (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite ↥(RatFuncInfinityIntegers K) ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityIntegralClosureIsDedekindDomain (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(RatFuncInfinityIntegralClosure K L)

theorem BGS.CorvajaZannier.infinityIntegralClosureIsFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] : IsFractionRing (↥(RatFuncInfinityIntegralClosure K L)) L

theorem BGS.CorvajaZannier.infinityBaseFaithfulSMulExtensionFractionRing (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FaithfulSMul (↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

@[instance_reducible]

noncomputable def BGS.CorvajaZannier.infinityFractionRingAlgebra (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (FractionRing ↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

The algebra structure from (FractionRing (RatFuncInfinityIntegers K)) to (FractionRing (RatFuncInfinityIntegralClosure K L)) used in the infinity place construction.

Equations

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

theorem BGS.CorvajaZannier.infinityFractionRingSeparable (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Algebra.IsSeparable (FractionRing ↥(RatFuncInfinityIntegers K)) (FractionRing ↥(RatFuncInfinityIntegralClosure K L))

theorem BGS.CorvajaZannier.count_spanSingleton_norm_at_infinity_eq_sum (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : FractionRing ↥(RatFuncInfinityIntegralClosure K L)) : FractionalIdeal.count (FractionRing ↥(RatFuncInfinityIntegers K)) (ratFuncInfinityPlace K) ((FractionalIdeal.spanSingleton (nonZeroDivisors ↥(RatFuncInfinityIntegers K))) ((Algebra.norm (FractionRing ↥(RatFuncInfinityIntegers K))) x)) = ∑ P : ↑((ratFuncInfinityPlace K).asIdeal.primesOver ↥(RatFuncInfinityIntegralClosure K L)), ↑((↑P).inertiaDeg ↥(RatFuncInfinityIntegers K)) * FractionalIdeal.count (FractionRing ↥(RatFuncInfinityIntegralClosure K L)) (primeOverHeightOne (ratFuncInfinityPlace K) P) ((FractionalIdeal.spanSingleton (nonZeroDivisors ↥(RatFuncInfinityIntegralClosure K L))) x)

The norm/count identity at infinity in a finite separable extension of K(X): the order of the norm at infinity is the residue-degree-weighted sum of the orders at all primes above infinity.