Exact constants and finite constant extensions

Let N / C be a field extension whose exact constant field is C, meaning that no element of N \ C is algebraic over C. If S / C is finite Galois, then S and N are linearly disjoint over C. Consequently the tensor product S ⊗[C] N is a field, and its degree over N is [S : C].

Mathlib's finite-Galois intersection criterion assumes both intermediate fields are finite over the base. The first theorem below proves the variant needed here: only the Galois field on the left must be finite. This is the algebraic foundation for the constant-extension twists in Stichtenoth, Proposition 5.2.8.

theorem BGS.HasseWeil.linearDisjoint_of_inf_eq_bot_of_finite_galois_left {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (A B : IntermediateField F E) [IsGalois F ↥A] [FiniteDimensional F ↥A] (hinf : A ⊓ B = ⊥) : A.LinearDisjoint ↥B

A finite Galois intermediate field is linearly disjoint from any other intermediate field having trivial intersection with it. Unlike Mathlib's finite intersection criterion, the field on the right need not be finite over the base.

theorem BGS.HasseWeil.exactConstantExtensionImages_linearDisjoint (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : let Ω := AlgebraicClosure N; have fS := IsAlgClosed.lift; fS.fieldRange.LinearDisjoint ↥(IsScalarTower.toAlgHom C N Ω).fieldRange

Inside a common algebraic closure, a finite Galois constant extension and a field with exact constant field C are linearly disjoint over C.

theorem BGS.HasseWeil.exactConstantExtensionTensor_isField (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : IsField (TensorProduct C S N)

If C is the exact constant field of N, adjoining any finite Galois extension S / C by tensor product produces a field.

@[reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionAlgebra (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] : Algebra N (TensorProduct C S N)

The algebra structure on S ⊗[C] N induced by the copy of N in the right tensor factor.

Equations

• BGS.HasseWeil.exactConstantExtensionAlgebra C N S = Algebra.TensorProduct.includeRight.toAlgebra

noncomputable def BGS.HasseWeil.exactConstantExtensionLinearEquiv (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] : TensorProduct C N S ≃ₗ[N] TensorProduct C S N

Commuting the tensor factors identifies the constant extension with the usual scalar extension of S from C to N.

Equations

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

theorem BGS.HasseWeil.exactConstantExtension_finrank (C : Type u_1) (N : Type u_2) (S : Type u_3) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] : Module.finrank N (TensorProduct C S N) = Module.finrank C S

A finite constant extension has the expected degree over the original field.