Rational finite places after exact constant extension

For a finite Galois function-field extension, the degree of a place above a rational base place divides the relative field degree. Combining this fact with the constant-extension degree formula shows that an extension of constants whose degree is divisible by the Galois degree makes every such lifted place rational.

This is the numerical-to-geometric bridge used when Stichtenoth chooses the constant-extension degree to be divisible by the Galois-group order.

theorem BGS.HasseWeil.finiteExtensionFinitePlace_degree_dvd_relative_finrank_of_under_degree_one (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (M : Type u_2) [Field M] [Algebra (RatFunc K) M] [FiniteDimensional (RatFunc K) M] [Algebra.IsSeparable (RatFunc K) M] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] [IsGalois M L] (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) (hUnder : CorvajaZannier.finiteExtensionPlaceDegree K M (Sum.inl (finitePlaceUnder K M L Q)) = 1) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) ∣ Module.finrank M L

In a finite Galois tower, a finite place over a degree-one intermediate place has degree dividing the relative field degree.

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactRationalBaseConstantAlgebra (C : Type u_4) (N : Type u_6) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the constant extension rational place construction.

Equations

• BGS.HasseWeil.exactRationalBaseConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactRationalBasePolynomialAlgebra (C : Type u_4) (N : Type u_6) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra (Polynomial C) N

The algebra structure from C[X] to N used in the constant extension rational place construction.

Equations

• BGS.HasseWeil.exactRationalBasePolynomialAlgebra C N = BGS.HasseWeil.bridgeBasePolynomialAlgebra C N

@[instance_reducible]

noncomputable def BGS.HasseWeil.exactRationalTargetPolynomialAlgebra (C : Type u_4) (S : Type u_5) (N : Type u_6) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] : Algebra (Polynomial S) (ExactConstantExtension C N S)

The algebra structure from S[X] to (ExactConstantExtension C N S) used in the constant extension rational place construction.

Equations

• BGS.HasseWeil.exactRationalTargetPolynomialAlgebra C S N = BGS.HasseWeil.bridgeTargetPolynomialAlgebra C S N

theorem BGS.HasseWeil.exactConstantExtensionUpstairsFinitePlace_degree_eq_one_of_under_degree_one (C : Type u_4) (S : Type u_5) (N : Type u_6) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq S] [DecidableEq (RatFunc C)] [DecidableEq (RatFunc S)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial S) (ExactConstantExtension C N S))) (hUnder : CorvajaZannier.finiteExtensionPlaceDegree C (RatFunc C) (Sum.inl (finitePlaceUnder C (RatFunc C) N (exactConstantExtensionDownstairsFinitePlace C S N hExact q))) = 1) (hDegree : Module.finrank (RatFunc C) N ∣ Module.finrank C S) : CorvajaZannier.finiteExtensionPlaceDegree S (ExactConstantExtension C N S) (Sum.inl (exactConstantExtensionUpstairsFinitePlace C S N hExact q)) = 1

If the constant-extension degree is divisible by the Galois degree, then an upstairs finite place whose contraction lies over a rational base place has degree one over the enlarged constants.