Finite-place degrees under constant-field extension

The finite integral closures before and after constant extension are the same subring of the enlarged function field. This file upgrades that ring equivalence to an equivalence over the original constant field and transports it to residue fields. Consequently, if Q_E is the finite place obtained from Q after replacing K by E, then

deg_K(Q) = [E : K] * deg_E(Q_E).

This is the arithmetic content missing from a bare equivalence of finite-place types: an E-rational place is a place of degree [E : K] over K.

@[instance_reducible]

noncomputable def BGS.HasseWeil.degreePolynomialCoefficientAlgebra (K : Type u_1) (E : Type u_2) [Field K] [Field E] [Algebra K E] : Algebra (Polynomial K) (Polynomial E)

The algebra structure from K[X] to E[X] used in the constant field finite place degree construction.

Equations

• BGS.HasseWeil.degreePolynomialCoefficientAlgebra K E = (Polynomial.mapRingHom (algebraMap K E)).toAlgebra

@[instance_reducible]

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

The algebra structure from K[X] to L used in the constant field finite place degree construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.degreeExtensionPolynomialAlgebra (E : Type u_2) (L : Type u_3) [Field E] [Field L] [Algebra (RatFunc E) L] : Algebra (Polynomial E) L

The algebra structure from E[X] to L used in the constant field finite place degree construction.

Equations

• BGS.HasseWeil.degreeExtensionPolynomialAlgebra E L = ((algebraMap (RatFunc E) L).comp (algebraMap (Polynomial E) (RatFunc E))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.degreeBaseFiniteClosureConstantAlgebra (K : Type u_1) (L : Type u_3) [Field K] [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the constant field finite place degree construction.

Equations

• BGS.HasseWeil.degreeBaseFiniteClosureConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.degreeExtensionFiniteClosureConstantAlgebra (E : Type u_2) (L : Type u_3) [Field E] [Field L] [Algebra (RatFunc E) L] : Algebra E ↥(CorvajaZannier.RatFuncFiniteIntegralClosure E L)

The algebra structure from E to (RatFuncFiniteIntegralClosure E L) used in the constant field finite place degree construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.degreeExtensionFiniteClosureBaseConstantAlgebra (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [Algebra K E] [Algebra (RatFunc E) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure E L)

The algebra structure from K to (RatFuncFiniteIntegralClosure E L) used in the constant field finite place degree construction.

Equations

• BGS.HasseWeil.degreeExtensionFiniteClosureBaseConstantAlgebra K E L = ((algebraMap E ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure E L)).comp (algebraMap K E)).toAlgebra

theorem BGS.HasseWeil.degreeExtensionFiniteClosureConstantTower (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [Algebra K E] [Algebra (RatFunc E) L] : IsScalarTower K E ↥(CorvajaZannier.RatFuncFiniteIntegralClosure E L)

noncomputable def BGS.HasseWeil.ratFuncFiniteIntegralClosureBaseChangeAlgEquiv (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [Algebra.IsIntegral K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) : ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L) ≃ₐ[K] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure E L)

The identity equivalence between the two finite integral closures respects the original constants.

Equations

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

noncomputable def BGS.HasseWeil.finitePlaceResidueFieldBaseChangeAlgEquiv (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [Algebra.IsIntegral K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : Q.asIdeal.ResidueField ≃ₐ[K] ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (ratFuncFiniteIntegralClosureRingEquiv K E L hcomm)) Q).asIdeal.ResidueField

The finite-integral-closure equivalence transports residue fields as K-algebras.

Equations

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

theorem BGS.HasseWeil.finiteExtensionFinitePlace_degree_baseChange (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [DecidableEq K] [DecidableEq E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [FiniteDimensional (RatFunc E) L] [Algebra.IsSeparable (RatFunc E) L] [Algebra.IsIntegral K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = Module.finrank K E * CorvajaZannier.finiteExtensionPlaceDegree E L (Sum.inl ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (ratFuncFiniteIntegralClosureRingEquiv K E L hcomm)) Q))

A finite place in the common top function field has base-field degree equal to the constant-extension degree times its extended-field degree.

theorem BGS.HasseWeil.finiteExtensionFinitePlace_baseChange_rational_iff (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [DecidableEq K] [DecidableEq E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [FiniteDimensional (RatFunc E) L] [Algebra.IsSeparable (RatFunc E) L] [Algebra.IsIntegral K E] [FiniteDimensional K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : CorvajaZannier.finiteExtensionPlaceDegree E L (Sum.inl ((IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv (ratFuncFiniteIntegralClosureRingEquiv K E L hcomm)) Q)) = 1 ↔ CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = Module.finrank K E

A place is rational over the extended constant field exactly when its degree over the original constant field is the degree of the constant extension.

noncomputable def BGS.HasseWeil.finiteExtensionFinitePlaceDegreeEquivRationalBaseChange (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [DecidableEq K] [DecidableEq E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [FiniteDimensional (RatFunc E) L] [Algebra.IsSeparable (RatFunc E) L] [Algebra.IsIntegral K E] [FiniteDimensional K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) : { Q : CorvajaZannier.FiniteExtensionFinitePlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = Module.finrank K E } ≃ FiniteExtensionRationalFinitePlace E L

Base change identifies the finite places of degree [E : K] with the rational finite places over E.

Equations

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

theorem BGS.HasseWeil.natCard_finiteExtensionRationalFinitePlace_eq_degree_baseChange (K : Type u_1) (E : Type u_2) (L : Type u_3) [Field K] [Field E] [Field L] [DecidableEq K] [DecidableEq E] [DecidableEq (RatFunc K)] [DecidableEq (RatFunc E)] [Algebra K E] [Algebra (RatFunc K) L] [Algebra (RatFunc E) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [FiniteDimensional (RatFunc E) L] [Algebra.IsSeparable (RatFunc E) L] [Algebra.IsIntegral K E] [FiniteDimensional K E] (hcomm : ∀ (p : Polynomial K), (algebraMap (RatFunc K) L) ((algebraMap (Polynomial K) (RatFunc K)) p) = (algebraMap (RatFunc E) L) ((algebraMap (Polynomial E) (RatFunc E)) ((algebraMap (Polynomial K) (Polynomial E)) p))) : Nat.card (FiniteExtensionRationalFinitePlace E L) = Nat.card { Q : CorvajaZannier.FiniteExtensionFinitePlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl Q) = Module.finrank K E }

Cardinal form of the finite rational-place base-change correspondence.