The constant-base field inside the function-field normal closure

Let N / K(t) be the chosen function-field normal closure and let C be its algebraic constant field. The restriction map

Gal(N/K(t)) → Gal(C/K)

is already known to be onto. This file defines the fixed field of its kernel. Every element of C lies in that fixed field, so it gives a genuine tower C ⊆ L_C ⊆ N; moreover N / L_C is finite Galois. The general exact constant-extension and Frobenius-quotient theorems can therefore be applied directly to the normal closure used by the Hasse--Weil proof.

@[reducible, inline]

noncomputable abbrev BGS.HasseWeil.FunctionFieldNormalClosureConstantBase (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IntermediateField (RatFunc K) ↥(FunctionFieldNormalClosure K L)

The fixed field of the automorphisms of the normal closure that act trivially on all algebraic constants.

Equations

• BGS.HasseWeil.FunctionFieldNormalClosureConstantBase K L = IntermediateField.fixedField (BGS.HasseWeil.functionFieldNormalClosureConstantRestriction K L).ker

def BGS.HasseWeil.functionFieldNormalClosureConstantToBase (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : ↥(FunctionFieldNormalClosureConstantField K L) →ₐ[K] ↥(FunctionFieldNormalClosureConstantBase K L)

Algebraic constants embed into the fixed field of the restriction kernel.

Equations

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

@[reducible]

noncomputable instance BGS.HasseWeil.functionFieldNormalClosureConstantBaseAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Algebra ↥(FunctionFieldNormalClosureConstantField K L) ↥(FunctionFieldNormalClosureConstantBase K L)

The induced algebra structure of the kernel fixed field over the full constant field.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantBaseAlgebra K L = (BGS.HasseWeil.functionFieldNormalClosureConstantToBase K L).toAlgebra

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalClosureConstantBaseSMul (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : SMul ↥(FunctionFieldNormalClosureConstantField K L) ↥(FunctionFieldNormalClosureConstantBase K L)

The scalar action of (FunctionFieldNormalClosureConstantField K L) on (FunctionFieldNormalClosureConstantBase K L) used in the function field normal closure constant base construction.

Equations

• BGS.HasseWeil.normalClosureConstantBaseSMul K L = (BGS.HasseWeil.functionFieldNormalClosureConstantBaseAlgebra K L).toSMul

@[instance_reducible]

noncomputable def BGS.HasseWeil.normalClosureConstantBaseModule (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Module ↥(FunctionFieldNormalClosureConstantField K L) ↥(FunctionFieldNormalClosureConstantBase K L)

The module structure of (FunctionFieldNormalClosureConstantBase K L) over (FunctionFieldNormalClosureConstantField K L) used in the function field normal closure constant base construction.

Equations

• BGS.HasseWeil.normalClosureConstantBaseModule K L = Algebra.toModule

instance BGS.HasseWeil.functionFieldNormalClosureConstantBase_isScalarTower (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsScalarTower ↥(FunctionFieldNormalClosureConstantField K L) ↥(FunctionFieldNormalClosureConstantBase K L) ↥(FunctionFieldNormalClosure K L)

The embeddings of the constants into the fixed field and into the normal closure form a scalar tower.

instance BGS.HasseWeil.functionFieldNormalClosure_finiteDimensional_over_constantBase (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : FiniteDimensional ↥(FunctionFieldNormalClosureConstantBase K L) ↥(FunctionFieldNormalClosure K L)

The normal closure is finite over the kernel fixed field.

instance BGS.HasseWeil.functionFieldNormalClosure_isGalois_over_constantBase (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsGalois ↥(FunctionFieldNormalClosureConstantBase K L) ↥(FunctionFieldNormalClosure K L)

The normal closure is Galois over the kernel fixed field.

@[reducible]

noncomputable instance BGS.HasseWeil.functionFieldNormalClosureExactConstantExtensionField (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K L)) S] [FiniteDimensional (↥(FunctionFieldNormalClosureConstantField K L)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K L)) S] : Field (ExactConstantExtension (↥(FunctionFieldNormalClosureConstantField K L)) (↥(FunctionFieldNormalClosure K L)) S)

The generic exact-constant field structure specializes to the chosen function-field normal closure.

Equations

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

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantExtensionAutMulEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K L)) S] [FiniteDimensional (↥(FunctionFieldNormalClosureConstantField K L)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K L)) S] : have this := exactConstantExtensionBaseAlgebra (↥(FunctionFieldNormalClosureConstantField K L)) (↥(FunctionFieldNormalClosureConstantBase K L)) (↥(FunctionFieldNormalClosure K L)) S; Gal(S/↥(FunctionFieldNormalClosureConstantField K L)) × Gal(↥(FunctionFieldNormalClosure K L)/↥(FunctionFieldNormalClosureConstantBase K L)) ≃* Gal(ExactConstantExtension (↥(FunctionFieldNormalClosureConstantField K L)) (↥(FunctionFieldNormalClosure K L)) S/↥(FunctionFieldNormalClosureConstantBase K L))

The Galois group of the specialized constant extension is the product of the new constant Galois group and the kernel-fixed-field Galois group.

Equations

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

theorem BGS.HasseWeil.functionFieldNormalClosureConstantExtensionQuotient_surjective (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (S : Type u_3) [Field S] [Algebra (↥(FunctionFieldNormalClosureConstantField K L)) S] [FiniteDimensional (↥(FunctionFieldNormalClosureConstantField K L)) S] [IsGalois (↥(FunctionFieldNormalClosureConstantField K L)) S] : have this := exactConstantExtensionBaseAlgebra (↥(FunctionFieldNormalClosureConstantField K L)) (↥(FunctionFieldNormalClosureConstantBase K L)) (↥(FunctionFieldNormalClosure K L)) S; Function.Surjective ⇑(exactConstantExtensionConstantQuotient (↥(FunctionFieldNormalClosureConstantField K L)) (↥(FunctionFieldNormalClosureConstantBase K L)) (↥(FunctionFieldNormalClosure K L)) S ⋯)

The specialized constant quotient is onto.