The rational-function equivalence for the normal-closure constant base

This file packages the generation theorem from FunctionFieldNormalClosureRatFuncBase as an explicit algebra equivalence between C(t) and the kernel fixed field.

noncomputable def BGS.HasseWeil.ratFuncEquivOfAdjoinEqTop {C : Type u_1} {B : Type u_2} [Field C] [Field B] [Algebra C B] (x : B) (hx : Transcendental C x) (hgen : C⟮x⟯ = ⊤) : RatFunc C ≃ₐ[C] B

A field generated by one transcendental element is a rational function field.

Equations

• BGS.HasseWeil.ratFuncEquivOfAdjoinEqTop x hx hgen = (RatFunc.algEquivOfTranscendental x hx).trans ((IntermediateField.equivOfEq hgen).trans IntermediateField.topEquiv)

@[reducible]

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

The canonical constant-field algebra on its rational function field.

Equations

• BGS.HasseWeil.ratFuncSelfAlgebra C = RatFunc.instAlgebraOfPolynomial C C

@[instance_reducible]

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantFieldRatFuncAlgebra (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)) (RatFunc ↥(FunctionFieldNormalClosureConstantField K L))

The algebra structure from (FunctionFieldNormalClosureConstantField K L) to (RatFunc (FunctionFieldNormalClosureConstantField K L)) used in the function field normal closure rat func equiv construction.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantFieldRatFuncAlgebra K L = BGS.HasseWeil.ratFuncSelfAlgebra ↥(BGS.HasseWeil.FunctionFieldNormalClosureConstantField K L)

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgEquiv (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] : RatFunc ↥(FunctionFieldNormalClosureConstantField K L) ≃ₐ[↥(FunctionFieldNormalClosureConstantField K L)] ↥(FunctionFieldNormalClosureConstantBase K L)

The kernel fixed field is canonically the rational function field over the exact constant field, with the original parameter corresponding to X.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgEquiv K L = BGS.HasseWeil.ratFuncEquivOfAdjoinEqTop (BGS.HasseWeil.functionFieldNormalClosureConstantBaseX K L) ⋯ ⋯

noncomputable def BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgHom (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] : RatFunc ↥(FunctionFieldNormalClosureConstantField K L) →ₐ[↥(FunctionFieldNormalClosureConstantField K L)] ↥(FunctionFieldNormalClosureConstantBase K L)

The rational-function specialization that sends X to the original parameter in the kernel fixed field.

Equations

• BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgHom K L = ↑(BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgEquiv K L)

theorem BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgHom_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] : Function.Surjective ⇑(functionFieldNormalClosureConstantBaseRatFuncAlgHom K L)

The rational-function specialization onto the kernel fixed field is surjective because the parameter generates that field over its constants.

@[simp]

theorem BGS.HasseWeil.functionFieldNormalClosureConstantBaseRatFuncAlgEquiv_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] : (functionFieldNormalClosureConstantBaseRatFuncAlgEquiv K L) RatFunc.X = functionFieldNormalClosureConstantBaseX K L