Finite-place Frobenius-twist averaging over an intermediate base

This file proves the finite-place part of Stichtenoth's Frobenius-twist average for C(X) \subseteq L \subseteq N.

@[instance_reducible]

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

The algebra structure from C to N used in the exact constant extension intermediate frobenius twist finite place average construction.

Equations

• BGS.HasseWeil.intermediateAverageTopConstantAlgebra C N = BGS.HasseWeil.bridgeBaseConstantAlgebra C N

theorem BGS.HasseWeil.intermediateAverageTopConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] : IsScalarTower C (RatFunc C) N

@[instance_reducible]

noncomputable def BGS.HasseWeil.intermediateAverageTargetPolynomialAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Algebra (RatFunc C) N] [Algebra C S] : Algebra (Polynomial S) (ExactConstantExtension C N S)

The algebra structure from S[X] to (ExactConstantExtension C N S) used in the exact constant extension intermediate frobenius twist finite place average construction.

Equations

• BGS.HasseWeil.intermediateAverageTargetPolynomialAlgebra C S N = BGS.HasseWeil.bridgeTargetPolynomialAlgebra C S N

@[instance_reducible]

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

The algebra structure from C to L used in the exact constant extension intermediate frobenius twist finite place average construction.

Equations

• BGS.HasseWeil.intermediateAverageBaseConstantAlgebra C L = ((algebraMap (RatFunc C) L).comp (algebraMap C (RatFunc C))).toAlgebra

theorem BGS.HasseWeil.intermediateAverageConstantTower (C : Type u_1) (N : Type u_3) [Field C] [Field N] [Algebra (RatFunc C) N] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] : IsScalarTower C L N

@[instance_reducible]

noncomputable def BGS.HasseWeil.intermediateAverageRationalFinitePlaceFintype (C : Type u_1) [Field C] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] : Fintype (FiniteExtensionRationalFinitePlace C L)

A finite enumeration of (FiniteExtensionRationalFinitePlace C L) used in the exact constant extension intermediate frobenius twist finite place average construction.

Equations

• BGS.HasseWeil.intermediateAverageRationalFinitePlaceFintype C L = Fintype.ofFinite (BGS.HasseWeil.FiniteExtensionRationalFinitePlace C L)

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

The exact constant extension is finite-dimensional over every intermediate function field L.

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

Compatibility of the rational-function and intermediate-base algebra maps on the exact constant extension.

@[implicit_reducible]

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldRatFuncAlgebra (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : Algebra (RatFunc C) ↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g)

The rational-function algebra on an intermediate-base Frobenius-twist field is obtained through C(X) → L → F_g.

Equations

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

theorem BGS.HasseWeil.intermediateFrobeniusTwistField_ratFunc_tower (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; IsScalarTower (RatFunc C) (↥F) (ExactConstantExtension C N S)

The induced rational-function algebra is compatible with the inclusion of the twist field into the exact constant extension.

theorem BGS.HasseWeil.finiteDimensional_intermediateFrobeniusTwistField_over_ratFunc (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; FiniteDimensional (RatFunc C) ↥F

Every intermediate-base Frobenius-twist field is a finite function field over C(X).

theorem BGS.HasseWeil.isSeparable_intermediateFrobeniusTwistField_over_ratFunc (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; Algebra.IsSeparable (RatFunc C) ↥F

Separability of the exact constant extension descends to every intermediate-base Frobenius-twist field.

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistOverFixedField (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] (g : Gal(N/L)) : ExactConstantExtension C N S ≃ₐ[↥(exactConstantExtensionFrobeniusTwistField C L N S hExact g)] ExactConstantExtension C N S

The ambient Frobenius twist regarded as an automorphism over its own fixed field.

Equations

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

@[simp]

theorem BGS.HasseWeil.intermediateFrobeniusTwistOverFixedField_apply (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] (g : Gal(N/L)) (x : ExactConstantExtension C N S) : (intermediateFrobeniusTwistOverFixedField C S N hExact L g) x = (exactConstantExtensionFrobeniusTwist C L N S g) x

theorem BGS.HasseWeil.intermediateFrobeniusTwistOverFixedField_zpowers_eq_top (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] (g : Gal(N/L)) : Subgroup.zpowers (intermediateFrobeniusTwistOverFixedField C S N hExact L g) = ⊤

The twist over its fixed field generates the full relative Galois group.

theorem BGS.HasseWeil.intermediateFrobeniusTwistField_finitePlace_ramificationIdx_eq_one (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) : let this := exactConstantExtensionField C N S hExact; let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S; let this_2 := this_1.toSMul; let this_3 := Algebra.toModule; have this_4 := ⋯; have this_5 := ⋯; have this_6 := exactConstantExtensionBaseAlgebra C L N S; let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; let this_7 := intermediateFrobeniusTwistFieldRatFuncAlgebra C S N hExact L g; let this_8 := this_7.toSMul; let this_9 := Algebra.toModule; have this_10 := ⋯; have this_11 := ⋯; let this_12 := F.toAlgebra; let this_13 := this_12.toSMul; let this_14 := Algebra.toModule; have this_15 := ⋯; have this_16 := ⋯; have this_17 := ⋯; ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)), finitePlaceRelativeRamificationIdx C (↥F) (ExactConstantExtension C N S) Q = 1

Every finite place of the exact constant extension is unramified over an intermediate-base Frobenius-twist fixed field.

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_degree_eq_finrank_of_under_intermediate_rational (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [IsGalois L N] [Finite C] (hDegreeDiv : Module.finrank L N ∣ Module.finrank C S) (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl (finitePlaceUnder C L (ExactConstantExtension C N S) Q)) = 1 → CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q) = Module.finrank C S

Every top finite place over a rational finite place of L has absolute degree [S : C] when [N : L] divides the constant-extension degree.

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_frobeniusFiber_fixedPoint_sum_of_under_intermediate_rational (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hDegreeDiv : Module.finrank L N ∣ Module.finrank C S) (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : CorvajaZannier.finiteExtensionPlaceDegree C L (Sum.inl (finitePlaceUnder C L (ExactConstantExtension C N S) Q)) = 1 → have P := finitePlaceUnder C L (ExactConstantExtension C N S) Q; have pi := exactConstantExtensionConstantQuotient C L N S hExact; ∑ g : ↑(⇑pi ⁻¹' {FiniteField.frobeniusAlgEquivOfAlgebraic C S}), Nat.card ↑(MulAction.fixedBy (FinitePlaceUnderFiber C L (ExactConstantExtension C N S) P) ↑g) = Nat.card Gal(N/L)

Presentation-free local Frobenius-coset identity over a rational finite place of the intermediate field L.

@[simp]

theorem BGS.HasseWeil.intermediate_exactConstantExtensionFrobeniusFiberEquiv_apply_val (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (g : Gal(N/L)) : ↑((exactConstantExtensionFrobeniusFiberEquiv C L N S hExact) g) = exactConstantExtensionFrobeniusTwist C L N S g

The Frobenius-fiber parametrization sends g to the ambient twist (Frob, g) over the intermediate field.

@[reducible, inline]

abbrev BGS.HasseWeil.IntermediateFrobeniusTwistFinitePlaceFiberFixedBy (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (g : Gal(N/L)) (P : FiniteExtensionRationalFinitePlace C L) : Type (max u_2 u_3)

Fixed top finite places in the restriction fiber above one rational finite place of L, for one intermediate-base Frobenius twist.

Equations

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

theorem BGS.HasseWeil.sum_card_finitePlaceUnderFiber_fixedBy_intermediateFrobeniusTwist_eq_card_galois (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hDegreeDiv : Module.finrank L N ∣ Module.finrank C S) (P : FiniteExtensionRationalFinitePlace C L) : ∑ g : Gal(N/L), Nat.card (IntermediateFrobeniusTwistFinitePlaceFiberFixedBy C S N hExact L g P) = Nat.card Gal(N/L)

Above one rational finite place of L, summing fixed top places over all intermediate-base Frobenius twists contributes exactly |Gal(N/L)|.

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalFinitePlaceEquivAmbientFixedFinitePlace (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (g : Gal(N/L)) (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) : let T := ExactConstantExtension C N S; let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; FiniteExtensionRationalFinitePlace C ↥F ≃ { Q : CorvajaZannier.FiniteExtensionFinitePlace C T // CorvajaZannier.finiteExtensionPlaceDegree C T (Sum.inl Q) = Module.finrank C S ∧ finitePlaceGalSmul C L T (exactConstantExtensionFrobeniusTwist C L N S g) Q = Q }

Rational finite places of an intermediate-base twist field are exactly the degree-[S : C] top finite places fixed by its ambient Frobenius twist.

Equations

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

theorem BGS.HasseWeil.finitePlaceUnder_intermediateFrobeniusTwist_under (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : let T := ExactConstantExtension C N S; let this := exactConstantExtensionField C N S hExact; let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S; let this_2 := this_1.toSMul; let this_3 := Algebra.toModule; have this_4 := ⋯; have this_5 := ⋯; let this_6 := exactConstantExtensionBaseAlgebra C L N S; let this_7 := this_6.toSMul; have this_8 := Algebra.toModule; have this_9 := ⋯; let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; let this_10 := SubalgebraClass.toAlgebra F.toSubalgebra; let this_11 := intermediateFrobeniusTwistFieldRatFuncAlgebra C S N hExact L g; let this_12 := this_10.toSMul; have this_13 := Algebra.toModule; have this_14 := ⋯; let this_15 := this_11.toSMul; let this_16 := Algebra.toModule; have this_17 := ⋯; have this_18 := ⋯; let this_19 := F.toAlgebra; let this_20 := this_19.toSMul; have this_21 := Algebra.toModule; have this_22 := ⋯; ∀ (Q : CorvajaZannier.FiniteExtensionFinitePlace C T), finitePlaceUnder C L (↥F) (finitePlaceUnder C (↥F) T Q) = finitePlaceUnder C L T Q

Restriction through an intermediate Frobenius-twist field agrees with direct restriction to L.

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalFinitePlaceEquivSigmaFiberFixedBy (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) (g : Gal(N/L)) : let T := ExactConstantExtension C N S; let this := exactConstantExtensionField C N S hExact; let this_1 := exactConstantExtensionBaseAlgebra C (RatFunc C) N S; let this_2 := this_1.toSMul; let this_3 := Algebra.toModule; have this_4 := ⋯; have this_5 := ⋯; let this_6 := exactConstantExtensionBaseAlgebra C L N S; let this_7 := this_6.toSMul; let this_8 := Algebra.toModule; have this_9 := ⋯; have this_10 := ⋯; have this_11 := ⋯; let F := exactConstantExtensionFrobeniusTwistField C L N S hExact g; let this_12 := SubalgebraClass.toAlgebra F.toSubalgebra; let this_13 := intermediateFrobeniusTwistFieldRatFuncAlgebra C S N hExact L g; let this_14 := this_12.toSMul; have this_15 := Algebra.toModule; have this_16 := ⋯; let this_17 := this_13.toSMul; let this_18 := Algebra.toModule; have this_19 := ⋯; have this_20 := ⋯; let this_21 := F.toAlgebra; let this_22 := this_21.toSMul; let this_23 := Algebra.toModule; have this_24 := ⋯; have this_25 := ⋯; have this := ⋯; FiniteExtensionRationalFinitePlace C ↥F ≃ (P : FiniteExtensionRationalFinitePlace C L) × IntermediateFrobeniusTwistFinitePlaceFiberFixedBy C S N hExact L g P

Rational finite places of one intermediate-base twist field are the disjoint union, over rational finite places of L, of fixed top places in the corresponding restriction fiber.

Equations

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

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalFinitePlaceCount (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : ℕ

The rational finite-place count of one intermediate-base Frobenius-twist field, with its rational-function algebra fixed explicitly.

Equations

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

theorem BGS.HasseWeil.intermediateFrobeniusTwistFieldRationalFinitePlaceCount_eq_sum_fiberFixedBy (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) (g : Gal(N/L)) : intermediateFrobeniusTwistFieldRationalFinitePlaceCount C S N hExact L g = ∑ P : FiniteExtensionRationalFinitePlace C L, Nat.card (IntermediateFrobeniusTwistFinitePlaceFiberFixedBy C S N hExact L g P)

For one twist, rational finite places split as the finite sum of fixed restriction fibers above the rational finite places of L.

theorem BGS.HasseWeil.sum_intermediateFrobeniusTwistFieldRationalFinitePlaceCount_eq_card_galois_mul_card (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Finite S] [DecidableEq C] [DecidableEq (RatFunc C)] [Algebra (RatFunc C) N] [FiniteDimensional (RatFunc C) N] [Algebra.IsSeparable (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [FiniteDimensional (RatFunc C) L] [Algebra.IsSeparable (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] [FiniteDimensional L N] [IsGalois L N] (hdiv : Nat.card Gal(N/L) ∣ Module.finrank C S) : ∑ g : Gal(N/L), intermediateFrobeniusTwistFieldRationalFinitePlaceCount C S N hExact L g = Nat.card Gal(N/L) * Nat.card (FiniteExtensionRationalFinitePlace C L)

Summed over all intermediate-base Frobenius twists, the rational finite place count is exactly |Gal(N/L)| times the rational finite-place count of L.

theorem BGS.HasseWeil.exactConstantExtensionFrobeniusTwist_restrictScalars_apply (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [IsGalois C S] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) (x : ExactConstantExtension C N S) : (exactConstantExtensionFrobeniusTwist C (RatFunc C) N S (AlgEquiv.restrictScalars (RatFunc C) g)) x = (exactConstantExtensionFrobeniusTwist C L N S g) x

Viewing an intermediate-base Frobenius twist over C(X) does not change its underlying automorphism of the exact constant extension.

theorem BGS.HasseWeil.exactConstantExtensionFrobeniusTwist_restrictScalars (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [IsGalois C S] (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : AlgEquiv.restrictScalars (RatFunc C) (exactConstantExtensionFrobeniusTwist C L N S g) = exactConstantExtensionFrobeniusTwist C (RatFunc C) N S (AlgEquiv.restrictScalars (RatFunc C) g)

Equality of the two twists as C(X)-automorphisms.

noncomputable def BGS.HasseWeil.intermediateFrobeniusTwistFieldAlgEquivRationalBaseFrobeniusTwistField (C : Type u_1) (S : Type u_2) (N : Type u_3) [Field C] [Field S] [Field N] [Fintype C] [Algebra (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (L : Type u_4) [Field L] [Algebra (RatFunc C) L] [Algebra L N] [IsScalarTower (RatFunc C) L N] (g : Gal(N/L)) : have T := ExactConstantExtension C N S; let Fₗ := exactConstantExtensionFrobeniusTwistField C L N S hExact g; have Fᵣ := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact (AlgEquiv.restrictScalars (RatFunc C) g); ↥Fₗ ≃ₐ[RatFunc C] ↥Fᵣ

The fixed field constructed over L is the same function field as the rational-base twist attached to g.restrictScalars C(X).

Equations

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