Choosing the constant extension of divisor-index degree

The geometric F. K. Schmidt composition in FiniteExtensionZetaDegreeIndexOne accepts a finite constant extension whose degree is the divisor-degree index. Finite-field theory supplies such an extension in every positive degree. This file isolates that final choice: if the closed-place splitting identity is available for every finite Galois constant extension, then the divisor-degree index is one.

@[instance_reducible]

noncomputable def BGS.HasseWeil.selectedExtensionBaseConstantAlgebra (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] : Algebra C N

The algebra structure from C to N used in the finite extension zeta degree index one from all counts construction.

Equations

• BGS.HasseWeil.selectedExtensionBaseConstantAlgebra C N = ((algebraMap (RatFunc C) N).comp (algebraMap C (RatFunc C))).toAlgebra

theorem BGS.HasseWeil.selectedExtensionBaseConstantTower (C : Type u_1) (N : Type u_2) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

theorem BGS.HasseWeil.finiteExtensionDivisorDegreeIndex_eq_one_of_all_exactConstantExtension_closedPlaceCount (C : Type u_1) (N : Type u_2) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (hExact : algebraicClosure C N = ⊥) (hcount : ∀ (S : Type) [inst : Field S] [inst_1 : Fintype S] [inst_2 : Algebra C S] [inst_3 : FiniteDimensional C S] [inst_4 : IsGalois C S] (r : ℕ), exactConstantExtensionClosedPlaceExtensionCount C S N hExact r = finiteExtensionClosedPlaceExtensionCount C N (Module.finrank C S * r)) : finiteExtensionDivisorDegreeIndex C N = 1

It suffices to prove the exact constant-extension closed-place identity uniformly for finite Galois extensions of the constant field. The required extension of degree equal to the divisor-degree index is the standard finite field extension FiniteField.Extension.