The Frobenius quotient of an exact constant extension

The direct-product description of the constant extension gives a canonical quotient from its full Galois group to the Galois group of the enlarged constants. Its kernel is exactly the original function-field Galois group. When the constants are finite, the Frobenius fiber is explicitly equivalent to that kernel; these are the twists used in the lower-bound argument.

noncomputable def BGS.HasseWeil.exactConstantExtensionConstantQuotient (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 = ⊥) : (ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S) →* Gal(S/C)

Restriction to the enlarged constants, defined through the proved direct-product description of the full Galois group.

Equations

• BGS.HasseWeil.exactConstantExtensionConstantQuotient C L N S hExact = (MonoidHom.fst Gal(S/C) Gal(N/L)).comp (BGS.HasseWeil.exactConstantExtensionAutMulEquiv C L N S hExact).symm.toMonoidHom

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_combined (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)) (g : Gal(N/L)) : (exactConstantExtensionConstantQuotient C L N S hExact) ((exactConstantExtensionCombinedAutHom C L N S) (σ, g)) = σ

On an automorphism assembled from its two tensor factors, the constant quotient returns the first factor.

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_action_on_constants (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 = ⊥) (g : ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S) (s : S) : g (Algebra.TensorProduct.includeLeft s) = Algebra.TensorProduct.includeLeft (((exactConstantExtensionConstantQuotient C L N S hExact) g) s)

The constant quotient records exactly how a full automorphism acts on the embedded enlarged constant field.

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_surjective (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 = ⊥) : Function.Surjective ⇑(exactConstantExtensionConstantQuotient C L N S hExact)

The constant quotient is onto.

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_ker (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 = ⊥) : (exactConstantExtensionConstantQuotient C L N S hExact).ker = (exactConstantExtensionFunctionAutHom C L N S).range

The kernel of the constant quotient is precisely the image of the function-field action.

theorem BGS.HasseWeil.exactConstantExtensionConstantAutHom_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 ⇑(exactConstantExtensionConstantAutHom C L N S)

The constant-factor action is faithful.

noncomputable def BGS.HasseWeil.exactConstantExtensionFrobenius (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] [IsGalois C S] [Fintype C] : ExactConstantExtension C N S ≃ₐ[L] ExactConstantExtension C N S

Frobenius on S / C, lifted to the tensor compositum while fixing N.

Equations

• BGS.HasseWeil.exactConstantExtensionFrobenius C L N S = (BGS.HasseWeil.exactConstantExtensionConstantAutHom C L N S) (FiniteField.frobeniusAlgEquivOfAlgebraic C S)

theorem BGS.HasseWeil.orderOf_exactConstantExtensionFrobenius (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] [IsGalois C S] [Fintype C] [Finite S] : orderOf (exactConstantExtensionFrobenius C L N S) = Module.finrank C S

The lifted Frobenius has order [S : C].

theorem BGS.HasseWeil.exactConstantExtensionConstantQuotient_frobenius (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] [Fintype C] (hExact : algebraicClosure C N = ⊥) : (exactConstantExtensionConstantQuotient C L N S hExact) (exactConstantExtensionFrobenius C L N S) = FiniteField.frobeniusAlgEquivOfAlgebraic C S

The constant quotient sends the lifted Frobenius to finite-field Frobenius.

noncomputable def BGS.HasseWeil.exactConstantExtensionFrobeniusFiberEquiv (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] [Fintype C] (hExact : algebraicClosure C N = ⊥) : Gal(N/L) ≃ ↑(⇑(exactConstantExtensionConstantQuotient C L N S hExact) ⁻¹' {FiniteField.frobeniusAlgEquivOfAlgebraic C S})

The Frobenius fiber of the constant quotient is parametrized exactly by the original function-field Galois group.

Equations

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

theorem BGS.HasseWeil.natCard_exactConstantExtensionFrobeniusFiber (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] [Fintype C] (hExact : algebraicClosure C N = ⊥) : Nat.card ↑(⇑(exactConstantExtensionConstantQuotient C L N S hExact) ⁻¹' {FiniteField.frobeniusAlgEquivOfAlgebraic C S}) = Nat.card Gal(N/L)

Consequently the Frobenius fiber has the same cardinality as Gal(N/L).