Rational-place count of an exact constant extension

The packaged exact constant-extension count at level one is definitionally the complete rational-place count of the scalar-extended function field. This small bridge keeps the instance choices used by the global splitting formula explicit.

@[instance_reducible]

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

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

Equations

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

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

theorem BGS.HasseWeil.exactConstantExtensionClosedPlaceExtensionCount_one_eq_rationalPlaceCount (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Fintype S] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [Field N] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] (hExact : algebraicClosure C N = ⊥) : exactConstantExtensionClosedPlaceExtensionCount C S N hExact 1 = let E := ExactConstantExtension C N S; finiteExtensionRationalPlaceCount S E

The packaged level-one exact-extension count is the complete rational place count of the extended function field.