Galois groups of exact constant extensions

For a tower C ⊆ L ⊆ N and a finite Galois extension S / C, the tensor compositum S ⊗[C] N carries two commuting actions: constants act on the left factor and Gal(N/L) acts on the right factor. The actions are jointly faithful without any exact-constant hypothesis.

If C is the exact constant field of N, the tensor product is a field. A degree count then proves that the combined action exhausts its full Galois group over L:

Gal((S ⊗[C] N) / L) ≃ Gal(S/C) × Gal(N/L).

This is the direct-product statement used in Stichtenoth, Proposition 5.2.8.

@[reducible, inline]

abbrev BGS.HasseWeil.ExactConstantExtension (C : Type u_1) (N : Type u_2) (S : Type u_3) [CommRing C] [CommRing N] [CommRing S] [Algebra C N] [Algebra C S] : Type (max u_3 u_2)

The tensor compositum of a field N and a constant extension S / C.

Equations

• BGS.HasseWeil.ExactConstantExtension C N S = TensorProduct C S N

@[reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionField (C : Type u_1) (N : Type u_3) (S : Type u_4) [Field C] [Field N] [Field S] [Algebra C N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) : Field (ExactConstantExtension C N S)

The field structure on the tensor compositum supplied by exact constants and finite Galois constant extension.

Equations

• BGS.HasseWeil.exactConstantExtensionField C N S hExact = ⋯.toField

@[reducible]

noncomputable def BGS.HasseWeil.exactConstantExtensionBaseAlgebra (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra L N] [Algebra C N] [Algebra C S] : Algebra L (ExactConstantExtension C N S)

The L-algebra structure on the tensor compositum induced by the right factor N.

Equations

• BGS.HasseWeil.exactConstantExtensionBaseAlgebra C L N S = (Algebra.TensorProduct.includeRight.comp (algebraMap L N)).toAlgebra

theorem BGS.HasseWeil.exactConstantExtensionBaseTower (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra L N] [Algebra C N] [Algebra C S] : IsScalarTower L N (ExactConstantExtension C N S)

The L ⊆ N ⊆ S ⊗[C] N scalar tower.

noncomputable def BGS.HasseWeil.exactConstantExtensionConstantAlgEquivOverBase (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra L N] [Algebra C N] [Algebra C S] (σ : Gal(S/C)) : ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

A constant-field automorphism acting on the left tensor factor and fixing N, viewed as an automorphism over L.

Equations

• BGS.HasseWeil.exactConstantExtensionConstantAlgEquivOverBase C L N S σ = { toEquiv := (BGS.HasseWeil.tensorConstantAlgEquiv C S N σ).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.exactConstantExtensionFunctionAlgEquivOverBase (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] (g : Gal(N/L)) : ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

A function-field automorphism acting on the right tensor factor and fixing S, viewed as an automorphism over L.

Equations

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

noncomputable def BGS.HasseWeil.exactConstantExtensionConstantAutHom (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra L N] [Algebra C N] [Algebra C S] : Gal(S/C) →* ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

The constant-field action as a homomorphism into automorphisms over L.

Equations

• BGS.HasseWeil.exactConstantExtensionConstantAutHom C L N S = { toFun := BGS.HasseWeil.exactConstantExtensionConstantAlgEquivOverBase C L N S, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def BGS.HasseWeil.exactConstantExtensionFunctionAutHom (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] : Gal(N/L) →* ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

The function-field action as a homomorphism into automorphisms over L.

Equations

• BGS.HasseWeil.exactConstantExtensionFunctionAutHom C L N S = { toFun := BGS.HasseWeil.exactConstantExtensionFunctionAlgEquivOverBase C L N S, map_one' := ⋯, map_mul' := ⋯ }

theorem BGS.HasseWeil.exactConstantExtension_constant_function_commute (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] (σ : Gal(S/C)) (g : Gal(N/L)) : Commute ((exactConstantExtensionConstantAutHom C L N S) σ) ((exactConstantExtensionFunctionAutHom C L N S) g)

Constant-field and function-field automorphisms commute on the tensor compositum.

noncomputable def BGS.HasseWeil.exactConstantExtensionCombinedAutHom (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] : Gal(S/C) × Gal(N/L) →* ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

The product of the commuting constant and function-field actions.

Equations

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

theorem BGS.HasseWeil.exactConstantExtensionCombinedAutHom_injective (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] : Function.Injective ⇑(exactConstantExtensionCombinedAutHom C L N S)

The two tensor-factor actions are jointly faithful.

theorem BGS.HasseWeil.exactConstantExtension_finrank_over_base (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra L N] [Algebra C N] [Algebra C S] : Module.finrank L (ExactConstantExtension C N S) = Module.finrank L N * Module.finrank C S

The tensor compositum has degree [N : L] [S : C] over L.

theorem BGS.HasseWeil.exactConstantExtension_isGalois (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional L N] [IsGalois L N] (hExact : algebraicClosure C N = ⊥) : IsGalois L (ExactConstantExtension C N S)

With exact constants, the tensor compositum is Galois over L.

noncomputable def BGS.HasseWeil.exactConstantExtensionAutMulEquiv (C : Type u_1) (L : Type u_2) (N : Type u_3) (S : Type u_4) [Field C] [Field L] [Field N] [Field S] [Algebra C L] [Algebra L N] [Algebra C N] [IsScalarTower C L N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] [FiniteDimensional L N] [IsGalois L N] (hExact : algebraicClosure C N = ⊥) : Gal(S/C) × Gal(N/L) ≃* ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

The full Galois group of an exact finite constant extension is the direct product of the constant and function-field Galois groups.

Equations

• BGS.HasseWeil.exactConstantExtensionAutMulEquiv C L N S hExact = MulEquiv.ofBijective (BGS.HasseWeil.exactConstantExtensionCombinedAutHom C L N S) ⋯