The closed-place Euler recurrence

For a finite family of positive integral weights, an effective divisor is a finitely supported family of multiplicities. Marking one occurrence of one place, together with one of as many labels as the place's weight, gives the coefficient recurrence obtained by logarithmically differentiating the Euler product.

This file proves that recurrence by an explicit bijection. It then uses the local finiteness of bounded-degree places to apply the finite combinatorial result to all exhaustive places of a finite extension of K(X).

@[reducible, inline]

abbrev BGS.HasseWeil.WeightedEffectiveDivisor {I : Type u_1} (w : I → ℕ) (n : ℕ) : Type u_1

Natural-valued divisors of a prescribed weighted degree.

Equations

• BGS.HasseWeil.WeightedEffectiveDivisor w n = { D : I →₀ ℕ // (Finsupp.weight w) D = n }

@[reducible]

noncomputable def BGS.HasseWeil.weightedEffectiveDivisorFintype {I : Type u_1} [Fintype I] (w : I → ℕ) (hw : ∀ (i : I), w i ≠ 0) (n : ℕ) : Fintype (WeightedEffectiveDivisor w n)

A finite enumeration of weighted effective divisors when every weight is nonzero.

Equations

• BGS.HasseWeil.weightedEffectiveDivisorFintype w hw n = ⋯.fintype

noncomputable def BGS.HasseWeil.weightedEffectiveDivisorCount {I : Type u_1} [Fintype I] (w : I → ℕ) (hw : ∀ (i : I), w i ≠ 0) (n : ℕ) : ℕ

The number of natural-valued divisors having weighted degree n in a finite family of nonzero weights.

Equations

• BGS.HasseWeil.weightedEffectiveDivisorCount w hw n = Fintype.card (BGS.HasseWeil.WeightedEffectiveDivisor w n)

def BGS.HasseWeil.weightedClosedPlaceExtensionCount {I : Type u_1} [Fintype I] (w : I → ℕ) (r : ℕ) : ℕ

The degree-weighted sum of the places whose weights divide r.

Equations

• BGS.HasseWeil.weightedClosedPlaceExtensionCount w r = ∑ P : I, if w P ∣ r then w P else 0

theorem BGS.HasseWeil.weightedEffectiveDivisorPointCountRecurrence {I : Type u_1} [Fintype I] (w : I → ℕ) (hw : ∀ (i : I), 0 < w i) : HasEffectiveDivisorPointCountRecurrence (weightedEffectiveDivisorCount w ⋯) (weightedClosedPlaceExtensionCount w)

The logarithmic-derivative Euler recurrence for any finite family of positive integral place weights.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorDegree_eq_weight (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionEffectiveDivisor K L) : finiteExtensionEffectiveDivisorDegree K L D = (Finsupp.weight (CorvajaZannier.finiteExtensionPlaceDegree K L)) D

The repository's effective-divisor degree is Finsupp.weight for the closed-place degree function.

noncomputable def BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (r : ℕ) : ℕ

The extension point count encoded by closed places: a closed place of degree d contributes d exactly when d ∣ r.

Equations

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

theorem BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount_eq_sum_degree_dvd (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (r : ℕ) : finiteExtensionClosedPlaceExtensionCount K L r = ∑ P : { P : { P : CorvajaZannier.FiniteExtensionPlace K L // CorvajaZannier.finiteExtensionPlaceDegree K L P ≤ r } // CorvajaZannier.finiteExtensionPlaceDegree K L ↑P ∣ r }, CorvajaZannier.finiteExtensionPlaceDegree K L ↑↑P

The closed-place extension count is equivalently the sum of the degrees over the bounded subtype of places whose degrees divide the level.

@[simp]

theorem BGS.HasseWeil.finiteExtensionClosedPlaceExtensionCount_zero (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : finiteExtensionClosedPlaceExtensionCount K L 0 = 0

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorPointCountRecurrence (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : HasEffectiveDivisorPointCountRecurrence (finiteExtensionEffectiveDivisorCount K L) (finiteExtensionClosedPlaceExtensionCount K L)

The effective-divisor coefficients for the exhaustive closed places of a finite extension satisfy the exact closed-place Euler recurrence.