Degree-one places of a finite function field

This file defines the actual degree-one place type used by the fixed-field argument and proves that it is finite over a finite constant field. The proof does not assume a point-count bound: finite degree-one places inject into the finite family of linear base primes together with their finite lying-over fibers, while the places above infinity already form a finite lying-over fiber.

@[reducible, inline]

abbrev BGS.HasseWeil.RatFuncRationalFinitePlace (K : Type u_1) [Field K] [DecidableEq K] : Type u_1

Degree-one finite places of the rational function field K(t).

Equations

• BGS.HasseWeil.RatFuncRationalFinitePlace K = { P : IsDedekindDomain.HeightOneSpectrum (Polynomial K) // BGS.CorvajaZannier.ratFuncFinitePlaceDegree P = 1 }

noncomputable def BGS.HasseWeil.ratFuncRationalFinitePlaceToDegreeLT (K : Type u_1) [Field K] [DecidableEq K] : RatFuncRationalFinitePlace K → ↥(Polynomial.degreeLT K 2)

Embed a degree-one rational-function-field place into the finite coefficient space of polynomials of degree less than two.

Equations

• BGS.HasseWeil.ratFuncRationalFinitePlaceToDegreeLT K P = ⟨↑(BGS.CorvajaZannier.finitePlaceNormalizedPrime ↑P), ⋯⟩

theorem BGS.HasseWeil.ratFuncRationalFinitePlaceToDegreeLT_injective (K : Type u_1) [Field K] [DecidableEq K] : Function.Injective (ratFuncRationalFinitePlaceToDegreeLT K)

instance BGS.HasseWeil.ratFuncRationalFinitePlace_finite (K : Type u_1) [Field K] [DecidableEq K] [Finite K] : Finite (RatFuncRationalFinitePlace K)

There are finitely many degree-one finite places of K(t) when K is finite.

@[instance_reducible]

noncomputable def BGS.HasseWeil.rationalPlacePolynomialAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the rational place construction.

Equations

• BGS.HasseWeil.rationalPlacePolynomialAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.rationalPlacePolynomialScalarTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

theorem BGS.HasseWeil.rationalPlaceFiniteClosureModuleFinite (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.Finite (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.rationalPlaceFiniteClosureIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra.IsIntegral (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.rationalPlacePolynomialTorsionFreeTop (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) L

theorem BGS.HasseWeil.rationalPlaceFiniteClosureTorsionFree (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module.IsTorsionFree (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.rationalPlaceFiniteClosureDedekind (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsDedekindDomain ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

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

theorem BGS.HasseWeil.rationalPlaceInfinityClosureIntegral (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : Algebra.IsIntegral ↥(CorvajaZannier.RatFuncInfinityIntegers K) ↥(CorvajaZannier.RatFuncInfinityIntegralClosure K L)

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

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

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionRationalFinitePlace (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : Type u_2

Degree-one finite places of a finite extension of K(t).

Equations

• BGS.HasseWeil.FiniteExtensionRationalFinitePlace K L = { Q : BGS.CorvajaZannier.FiniteExtensionFinitePlace K L // BGS.CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = 1 }

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionRationalInfinityPlace (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : Type u_2

Degree-one places above infinity of a finite extension of K(t).

Equations

• BGS.HasseWeil.FiniteExtensionRationalInfinityPlace K L = { Q : ↑(BGS.CorvajaZannier.FiniteExtensionInfinityPlace K L) // BGS.CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inr Q) = 1 }

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionRationalPlace (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : Type u_2

The exhaustive type of degree-one places of a finite extension of K(t), split into the finite and above-infinity parts.

Equations

• BGS.HasseWeil.FiniteExtensionRationalPlace K L = (BGS.HasseWeil.FiniteExtensionRationalFinitePlace K L ⊕ BGS.HasseWeil.FiniteExtensionRationalInfinityPlace K L)

def BGS.HasseWeil.finiteExtensionRationalPlaceEquivSubtype (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : FiniteExtensionRationalPlace K L ≃ { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P = 1 }

The split rational-place type is exactly the subtype of exhaustive places whose place degree is one.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionRationalPlaceCount (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : ℕ

The number of degree-one places of the finite function field.

Equations

• BGS.HasseWeil.finiteExtensionRationalPlaceCount K L = Nat.card (BGS.HasseWeil.FiniteExtensionRationalPlace K L)

theorem BGS.HasseWeil.finiteExtensionRationalPlaceCount_eq_natCard_subtype (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : finiteExtensionRationalPlaceCount K L = Nat.card { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P = 1 }

noncomputable def BGS.HasseWeil.rationalFinitePlaceToBaseFiber (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] (Q : FiniteExtensionRationalFinitePlace K L) : (P : RatFuncRationalFinitePlace K) × ↑((↑P).asIdeal.primesOver ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L))

A rational finite place determines a rational base place together with a prime in its finite lying-over fiber.

Equations

• BGS.HasseWeil.rationalFinitePlaceToBaseFiber K L Q = ⟨⟨IsDedekindDomain.HeightOneSpectrum.under (Polynomial K) ↑Q, ⋯⟩, ⟨(↑Q).asIdeal, ⋯⟩⟩

theorem BGS.HasseWeil.rationalFinitePlaceToBaseFiber_injective (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [DecidableEq (RatFunc K)] : Function.Injective (rationalFinitePlaceToBaseFiber K L)

instance BGS.HasseWeil.finiteExtensionRationalFinitePlace_finite (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] [Finite K] : Finite (FiniteExtensionRationalFinitePlace K L)

The degree-one finite places of a finite function field are finite over a finite constant field.

instance BGS.HasseWeil.finiteExtensionRationalInfinityPlace_finite (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] : Finite (FiniteExtensionRationalInfinityPlace K L)

The degree-one places above infinity are finite.

instance BGS.HasseWeil.finiteExtensionRationalPlace_finite (K : Type u_1) [Field K] [DecidableEq K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] [Finite K] : Finite (FiniteExtensionRationalPlace K L)

The exhaustive degree-one place type is finite over a finite constant field.