A finite Galois closure for a one-variable function field

For a finite separable extension L / K(t), choose an embedding of L into the absolute separable closure of K(t) and take its normal closure there. The result is a finite Galois extension of K(t) containing an embedded copy of L.

This is the field-theoretic Galois-closure layer required by the twisted fixed-field argument. It does not identify the algebraic constant field of the closure or construct any Frobenius complements.

noncomputable def BGS.HasseWeil.functionFieldSeparableClosureEmbedding (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : L →ₐ[RatFunc K] SeparableClosure (RatFunc K)

A chosen K(t)-embedding of the function field into the absolute separable closure of K(t).

Equations

• BGS.HasseWeil.functionFieldSeparableClosureEmbedding K L = IsSepClosed.lift

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

The normal closure of the chosen embedded copy of L inside the absolute separable closure of K(t).

Equations

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

noncomputable def BGS.HasseWeil.functionFieldToNormalClosure (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : L →ₐ[RatFunc K] ↥(FunctionFieldNormalClosure K L)

The original function field embeds into its chosen normal closure.

Equations

• BGS.HasseWeil.functionFieldToNormalClosure K L = (BGS.HasseWeil.functionFieldSeparableClosureEmbedding K L).codRestrict (BGS.HasseWeil.FunctionFieldNormalClosure K L).toSubalgebra ⋯

theorem BGS.HasseWeil.functionFieldToNormalClosure_injective (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Function.Injective ⇑(functionFieldToNormalClosure K L)

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

The chosen normal closure remains finite over K(t).

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

The chosen normal closure is Galois over K(t).