The rational-function constant base of the normal closure

Let N / K(t) be the chosen function-field normal closure and let C be its full algebraic constant field. The field generated in N by K(t) and C is exactly the fixed field of the automorphisms acting trivially on C. This is the Galois-theoretic identification of that fixed field with the constant extension C(t).

@[instance_reducible]

noncomputable def BGS.HasseWeil.ratFuncBaseConstantSMul (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 rat func base construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.ratFuncBaseConstantModule (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 rat func base construction.

Equations

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

theorem BGS.HasseWeil.normalClosureConstantBaseRatFuncTower (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : IsScalarTower K (RatFunc K) ↥(FunctionFieldNormalClosureConstantBase K L)

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantCompositum (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 compositum of the original rational function field and the algebraic constant field, formed inside the chosen normal closure.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantCompositum K L = IntermediateField.adjoin (RatFunc K) (Set.range fun (c : ↥(BGS.HasseWeil.FunctionFieldNormalClosureConstantField K L)) => ↑c)

theorem BGS.HasseWeil.functionFieldNormalClosureConstantCompositum_fixingSubgroup (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : (functionFieldNormalClosureConstantCompositum K L).fixingSubgroup = (functionFieldNormalClosureConstantRestriction K L).ker

The subgroup fixing the constant compositum is precisely the kernel of restriction to the algebraic constant field.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantBase_eq_compositum (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] : FunctionFieldNormalClosureConstantBase K L = functionFieldNormalClosureConstantCompositum K L

The kernel fixed field is the compositum K(t)C inside the normal closure.

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

The original parameter t as an element of the kernel fixed field.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantBaseX K L = ⟨(algebraMap (RatFunc K) ↥(BGS.HasseWeil.FunctionFieldNormalClosure K L)) RatFunc.X, ⋯⟩

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

The K-, C-, and kernel-fixed-field algebra structures form a tower.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantBaseX_transcendental (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Transcendental (↥(FunctionFieldNormalClosureConstantField K L)) (functionFieldNormalClosureConstantBaseX K L)

The original parameter remains transcendental after adjoining all algebraic constants of the normal closure.

theorem BGS.HasseWeil.functionFieldNormalClosureConstantBase_adjoin_X (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] : (↥(FunctionFieldNormalClosureConstantField K L))⟮functionFieldNormalClosureConstantBaseX K L⟯ = ⊤

The kernel fixed field is generated over the full constant field by the original rational parameter.