Global finite-place averaging for Frobenius twists

This file removes the presentation choice from the local Frobenius-coset fixed-point identity and assembles the rational finite places of all Frobenius-twist fields without duplication.

theorem BGS.HasseWeil.finitePlaceUnder_ratFunc_under (K : Type u_1) (M : Type u_2) (L : Type u_3) [Field K] [Field M] [Field L] [Algebra (RatFunc K) M] [Algebra (RatFunc K) L] [Algebra M L] [IsScalarTower (RatFunc K) M L] (Q : CorvajaZannier.FiniteExtensionFinitePlace K L) : finitePlaceUnder K (RatFunc K) M (finitePlaceUnder K M L Q) = finitePlaceUnder K (RatFunc K) L Q

Restricting a finite place first to an intermediate function field and then to K(X) agrees with direct restriction to K(X). This is the finite-extension-place version of Ideal.under_under; unlike the raw chart statement finitePlaceUnder_under, both sides live in the normalized finite-place model of K(X).

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAverageRatFuncRationalFinitePlaceFintype (C : Type u_1) [Field C] [Fintype C] [DecidableEq C] : Fintype (RatFuncRationalFinitePlace C)

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

Equations

• BGS.HasseWeil.finiteAverageRatFuncRationalFinitePlaceFintype C = Fintype.ofFinite (BGS.HasseWeil.RatFuncRationalFinitePlace C)

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAverageBaseConstantAlgebra (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 frobenius twist finite place average construction.

Equations

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

theorem BGS.HasseWeil.finiteAverageBaseConstantTower (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.finiteAverageTargetPolynomialAlgebra (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 frobenius twist finite place average construction.

Equations

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

@[instance_reducible]

noncomputable def BGS.HasseWeil.finiteAverageRatFuncClosureConstantAlgebra (C : Type u_1) [Field C] : Algebra C ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (RatFunc C))

The algebra structure from C to (RatFuncFiniteIntegralClosure C (RatFunc C)) used in the exact constant extension frobenius twist finite place average construction.

Equations

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

theorem BGS.HasseWeil.finiteAverageRatFuncClosureConstantTower (C : Type u_1) [Field C] : IsScalarTower C (Polynomial C) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (RatFunc C))

noncomputable def BGS.HasseWeil.ratFuncFiniteBasePolynomialAlgEquivChart (C : Type u_1) [Field C] : Polynomial C ≃ₐ[Polynomial C] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (RatFunc C))

The chart-normalization equivalence over the polynomial base ring.

Equations

• BGS.HasseWeil.ratFuncFiniteBasePolynomialAlgEquivChart C = { toEquiv := (BGS.HasseWeil.ratFuncFiniteBaseRingEquivChart C).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

noncomputable def BGS.HasseWeil.ratFuncFiniteBaseAlgEquivChart (C : Type u_1) [Field C] : Polynomial C ≃ₐ[C] ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (RatFunc C))

The same equivalence over the constant field.

Equations

• BGS.HasseWeil.ratFuncFiniteBaseAlgEquivChart C = AlgEquiv.restrictScalars C (BGS.HasseWeil.ratFuncFiniteBasePolynomialAlgEquivChart C)

theorem BGS.HasseWeil.finiteAverageRatFuncClosureModuleFinite (C : Type u_1) [Field C] : Module.Finite (Polynomial C) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure C (RatFunc C))

noncomputable def BGS.HasseWeil.ratFuncFinitePlaceEquivFiniteExtension (C : Type u_1) [Field C] : IsDedekindDomain.HeightOneSpectrum (Polynomial C) ≃ CorvajaZannier.FiniteExtensionFinitePlace C (RatFunc C)

The finite-chart normalization of C[X] in C(X) is canonically equivalent to C[X] itself, hence their finite-place models agree.

Equations

• BGS.HasseWeil.ratFuncFinitePlaceEquivFiniteExtension C = BGS.HasseWeil.heightOneSpectrumEquivOfAlgEquiv (BGS.HasseWeil.ratFuncFiniteBasePolynomialAlgEquivChart C)

@[simp]

theorem BGS.HasseWeil.finiteExtensionPlaceDegree_ratFuncFinitePlaceEquivFiniteExtension (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] (P : IsDedekindDomain.HeightOneSpectrum (Polynomial C)) : CorvajaZannier.finiteExtensionPlaceDegree C (RatFunc C) (Sum.inl ((ratFuncFinitePlaceEquivFiniteExtension C) P)) = CorvajaZannier.ratFuncFinitePlaceDegree P

The chart-normalization equivalence preserves finite-place degree.

noncomputable def BGS.HasseWeil.ratFuncRationalFinitePlaceEquivFiniteExtension (C : Type u_1) [Field C] [DecidableEq C] [DecidableEq (RatFunc C)] : RatFuncRationalFinitePlace C ≃ FiniteExtensionRationalFinitePlace C (RatFunc C)

Degree-one finite places in the direct C[X] chart and in the generic finite-extension place model of C(X) are canonically equivalent.

Equations

• BGS.HasseWeil.ratFuncRationalFinitePlaceEquivFiniteExtension C = (BGS.HasseWeil.ratFuncFinitePlaceEquivFiniteExtension C).subtypeEquiv ⋯

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_degree_eq_finrank_of_under_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] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) [Finite C] (hDegreeDiv : Module.finrank (RatFunc C) N ∣ Module.finrank C S) (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : CorvajaZannier.finiteExtensionPlaceDegree C (RatFunc C) (Sum.inl (finitePlaceUnder C (RatFunc C) (ExactConstantExtension C N S) Q)) = 1 → CorvajaZannier.finiteExtensionPlaceDegree C (ExactConstantExtension C N S) (Sum.inl Q) = Module.finrank C S

Every actual top finite place over a rational finite place of C(X) has ambient degree [S : C], provided the constant-extension degree is divisible by the original Galois degree.

theorem BGS.HasseWeil.exactConstantExtensionFinitePlace_frobeniusFiber_fixedPoint_sum_of_under_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] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hDegreeDiv : Module.finrank (RatFunc C) N ∣ Module.finrank C S) (Q : CorvajaZannier.FiniteExtensionFinitePlace C (ExactConstantExtension C N S)) : CorvajaZannier.finiteExtensionPlaceDegree C (RatFunc C) (Sum.inl (finitePlaceUnder C (RatFunc C) (ExactConstantExtension C N S) Q)) = 1 → have P := finitePlaceUnder C (RatFunc C) (ExactConstantExtension C N S) Q; have pi := exactConstantExtensionConstantQuotient C (RatFunc C) N S hExact; ∑ g : ↑(⇑pi ⁻¹' {FiniteField.frobeniusAlgEquivOfAlgebraic C S}), Nat.card ↑(MulAction.fixedBy (FinitePlaceUnderFiber C (RatFunc C) (ExactConstantExtension C N S) P) ↑g) = Nat.card Gal(N/RatFunc C)

Presentation-free local Frobenius-coset identity above an arbitrary rational finite base place.

@[simp]

theorem BGS.HasseWeil.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] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) : ↑((exactConstantExtensionFrobeniusFiberEquiv C (RatFunc C) N S hExact) g) = exactConstantExtensionFrobeniusTwist C (RatFunc C) N S g

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

theorem BGS.HasseWeil.sum_card_finitePlaceUnderFiber_fixedBy_frobeniusTwist_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] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hDegreeDiv : Module.finrank (RatFunc C) N ∣ Module.finrank C S) (P : RatFuncRationalFinitePlace C) : have P₀ := (ratFuncRationalFinitePlaceEquivFiniteExtension C) P; ∑ g : Gal(N/RatFunc C), Nat.card ↑(MulAction.fixedBy (FinitePlaceUnderFiber C (RatFunc C) (ExactConstantExtension C N S) ↑P₀) (exactConstantExtensionFrobeniusTwist C (RatFunc C) N S g)) = Nat.card Gal(N/RatFunc C)

Above one rational finite place of C(X), summing fixed top places over all canonical Frobenius twists contributes exactly |Gal(N/C(X))|.

@[reducible, inline]

abbrev BGS.HasseWeil.FrobeniusTwistFinitePlaceFiberFixedBy (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] [FiniteDimensional (RatFunc C) N] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (g : Gal(N/RatFunc C)) (P : RatFuncRationalFinitePlace C) : Type (max u_2 u_3)

Fixed top finite places in the restriction fiber above one rational finite place of C(X), for one canonical Frobenius twist.

Equations

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

theorem BGS.HasseWeil.sigma_value_injective {I : Type u_4} {A : Type u_5} {B : Type u_6} {V : I → Type u_7} (index : I → A) (hindex : Function.Injective index) (value : (i : I) → V i → B) (under : B → A) (hunder : ∀ (i : I) (x : V i), under (value i x) = index i) (hvalue : ∀ (i : I), Function.Injective (value i)) : Function.Injective fun (x : Sigma V) => value x.fst x.snd

A sigma-family value map is injective when fibers are injective and their indices can be recovered injectively from the values.

noncomputable def BGS.HasseWeil.frobeniusTwistFieldRationalFinitePlaceEquivSigmaFiberFixedBy (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] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) (g : Gal(N/RatFunc C)) : 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 := this_3.toDistribMulAction; have this_5 := this_4.toMulAction; have this_6 := ⋯; have this_7 := ⋯; have this_8 := ⋯; let F := exactConstantExtensionFrobeniusTwistField C (RatFunc C) N S hExact g; let this_9 := SubalgebraClass.toAlgebra F.toSubalgebra; let this_10 := this_9.toSMul; let this_11 := Algebra.toModule; have this_12 := ⋯; have this_13 := ⋯; let this_14 := F.toAlgebra; let this_15 := this_14.toSMul; let this_16 := Algebra.toModule; have this_17 := ⋯; have this_18 := ⋯; have this := ⋯; FiniteExtensionRationalFinitePlace C ↥F ≃ (P : RatFuncRationalFinitePlace C) × FrobeniusTwistFinitePlaceFiberFixedBy C S N hExact g P

Rational finite places of one Frobenius-twist field are the disjoint union, over rational finite places of C(X), of the ambient 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.frobeniusTwistFieldRationalFinitePlaceCount (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 = ⊥) (g : Gal(N/RatFunc C)) : ℕ

The number of rational finite places of the fixed field attached to one canonical Frobenius twist. The instances are fixed explicitly so that this number can be summed over the original Galois group.

Equations

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

theorem BGS.HasseWeil.frobeniusTwistFieldRationalFinitePlaceCount_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] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) (g : Gal(N/RatFunc C)) : frobeniusTwistFieldRationalFinitePlaceCount C S N hExact g = ∑ P : RatFuncRationalFinitePlace C, Nat.card (FrobeniusTwistFinitePlaceFiberFixedBy C S N hExact g P)

For one twist, rational finite places split as the finite sum of fixed restriction fibers above the rational finite places of C(X).

theorem BGS.HasseWeil.sum_frobeniusTwistFieldRationalFinitePlaceCount_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] [IsGalois (RatFunc C) N] [Algebra C S] [FiniteDimensional C S] [IsGalois C S] (hExact : algebraicClosure C N = ⊥) (hdiv : Nat.card Gal(N/RatFunc C) ∣ Module.finrank C S) : ∑ g : Gal(N/RatFunc C), frobeniusTwistFieldRationalFinitePlaceCount C S N hExact g = Nat.card Gal(N/RatFunc C) * Nat.card C

Summed over all canonical Frobenius twists, the number of rational finite places is exactly the order of the original Galois group times the number of constants.