Divisor classes and the indexed eventual recurrence

This file builds the exhaustive divisor-class quotient and partitions the effective divisors of a fixed degree into its class fibers. Under exact constants, each fiber is the projectivization of the corresponding Riemann space.

The final recurrence is conditional on one explicit geometric input: the uniform eventual Riemann formula for arbitrary exhaustive divisors, not merely divisors on one effective ray. This is the remaining theorem needed to turn the existing one-ray stabilization results into the global divisor-count recurrence. In particular, no finiteness of a projective divisor class group is assumed: it follows, in every sufficiently large degree, from the uniform formula and the already proved finiteness of the effective divisors of that degree.

@[instance_reducible]

noncomputable def BGS.HasseWeil.divisorClassConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the finite extension divisor class recurrence construction.

Equations

• BGS.HasseWeil.divisorClassConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.divisorClassConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

def BGS.HasseWeil.finiteExtensionPrincipalDivisorSubgroup (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : AddSubgroup (CorvajaZannier.FiniteExtensionDivisor K L)

The additive subgroup of exhaustive principal divisors.

Equations

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

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionDivisorClass (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : Type u_2

The exhaustive divisor class group.

Equations

• BGS.HasseWeil.FiniteExtensionDivisorClass K L = (BGS.CorvajaZannier.FiniteExtensionDivisor K L ⧸ BGS.HasseWeil.finiteExtensionPrincipalDivisorSubgroup K L)

noncomputable def BGS.HasseWeil.finiteExtensionDivisorClassMap (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] : CorvajaZannier.FiniteExtensionDivisor K L →+ FiniteExtensionDivisorClass K L

The quotient map from exhaustive divisors to divisor classes.

Equations

• BGS.HasseWeil.finiteExtensionDivisorClassMap K L = QuotientAddGroup.mk' (BGS.HasseWeil.finiteExtensionPrincipalDivisorSubgroup K L)

@[simp]

theorem BGS.HasseWeil.finiteExtensionDivisorClassMap_principal (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (x : L) (hx : x ≠ 0) : (finiteExtensionDivisorClassMap K L) (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) = 0

noncomputable def BGS.HasseWeil.finiteExtensionDivisorClassDegree (K : Type u_1) [Field 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] : FiniteExtensionDivisorClass K L →+ ℤ

Divisor degree descends to divisor classes because principal divisors have degree zero.

Equations

• BGS.HasseWeil.finiteExtensionDivisorClassDegree K L = QuotientAddGroup.lift (BGS.HasseWeil.finiteExtensionPrincipalDivisorSubgroup K L) (BGS.HasseWeil.finiteExtensionDivisorDegreeHom K L) ⋯

@[simp]

theorem BGS.HasseWeil.finiteExtensionDivisorClassDegree_mk (K : Type u_1) [Field 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] (D : CorvajaZannier.FiniteExtensionDivisor K L) : (finiteExtensionDivisorClassDegree K L) ((finiteExtensionDivisorClassMap K L) D) = CorvajaZannier.finiteExtensionDivisorDegree K L D

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionDivisorClassOfDegree (K : Type u_1) [Field 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] (n : ℤ) : Type u_2

Divisor classes of a prescribed integer degree.

Equations

• BGS.HasseWeil.FiniteExtensionDivisorClassOfDegree K L n = { c : BGS.HasseWeil.FiniteExtensionDivisorClass K L // (BGS.HasseWeil.finiteExtensionDivisorClassDegree K L) c = n }

noncomputable def BGS.HasseWeil.finiteExtensionDivisorClassRepresentative (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (c : FiniteExtensionDivisorClass K L) : CorvajaZannier.FiniteExtensionDivisor K L

A chosen divisor representative of a class.

Equations

• BGS.HasseWeil.finiteExtensionDivisorClassRepresentative K L c = Quotient.out c

@[simp]

theorem BGS.HasseWeil.finiteExtensionDivisorClassMap_representative (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (c : FiniteExtensionDivisorClass K L) : (finiteExtensionDivisorClassMap K L) (finiteExtensionDivisorClassRepresentative K L c) = c

theorem BGS.HasseWeil.finiteExtensionDivisorClassRepresentative_degree (K : Type u_1) [Field 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] {n : ℤ} (c : FiniteExtensionDivisorClassOfDegree K L n) : CorvajaZannier.finiteExtensionDivisorDegree K L (finiteExtensionDivisorClassRepresentative K L ↑c) = n

noncomputable def BGS.HasseWeil.finiteExtensionDivisorClassOfDegreeTranslateEquiv (K : Type u_1) [Field 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] (H : CorvajaZannier.FiniteExtensionDivisor K L) (n d : ℤ) (hH : CorvajaZannier.finiteExtensionDivisorDegree K L H = d) : FiniteExtensionDivisorClassOfDegree K L n ≃ FiniteExtensionDivisorClassOfDegree K L (n + d)

Translation by a divisor of degree d identifies the degree-n and degree-n+d class fibers.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorClassOfDegree (K : Type u_1) [Field 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] (n : ℕ) (D : { D : FiniteExtensionEffectiveDivisor K L // finiteExtensionEffectiveDivisorDegree K L D = n }) : FiniteExtensionDivisorClassOfDegree K L ↑n

The divisor class of an effective divisor of natural degree n.

Equations

• BGS.HasseWeil.finiteExtensionEffectiveDivisorClassOfDegree K L n D = ⟨(BGS.HasseWeil.finiteExtensionDivisorClassMap K L) (BGS.HasseWeil.finiteExtensionEffectiveDivisorToDivisor K L ↑D), ⋯⟩

@[reducible, inline]

abbrev BGS.HasseWeil.FiniteExtensionEffectiveDivisorClassFiber (K : Type u_1) [Field 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] (n : ℕ) (c : FiniteExtensionDivisorClassOfDegree K L ↑n) : Type u_2

The fixed-degree effective divisors lying in one divisor class.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorClassFiberEquiv (K : Type u_1) [Field 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] (n : ℕ) (c : FiniteExtensionDivisorClassOfDegree K L ↑n) : FiniteExtensionEffectiveDivisorClassFiber K L n c ≃ EffectiveDivisorInPrincipalClass K L (finiteExtensionDivisorClassRepresentative K L ↑c)

A fixed-degree class fiber is exactly the effective divisors in the principal class of its chosen representative.

Equations

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

def BGS.HasseWeil.HasFiniteExtensionUniformEventualRiemannFormula (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] (genus threshold : ℕ) : Prop

Uniform eventual Riemann formula for arbitrary exhaustive divisors. This is the single geometric input not supplied by the current one-ray stabilization files.

Equations

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

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorClassOfDegree_surjective_of_uniformRiemann (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] (genus threshold n : ℕ) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) : Function.Surjective (finiteExtensionEffectiveDivisorClassOfDegree K L n)

The uniform eventual formula makes every sufficiently large divisor class effective.

theorem BGS.HasseWeil.finiteExtensionDivisorClassOfDegree_finite_of_uniformRiemann (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] (genus threshold n : ℕ) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) : Finite (FiniteExtensionDivisorClassOfDegree K L ↑n)

Hence the set of divisor classes of every sufficiently large admissible degree is finite.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorClassFiber_finite_of_uniformRiemann (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] (genus threshold n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) (c : FiniteExtensionDivisorClassOfDegree K L ↑n) : Finite (FiniteExtensionEffectiveDivisorClassFiber K L n c)

Under exact constants, every sufficiently large fixed-degree class fiber is finite.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorClassFiber_card_eq_geomSum_of_uniformRiemann (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] (genus threshold n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) (c : FiniteExtensionDivisorClassOfDegree K L ↑n) : Nat.card (FiniteExtensionEffectiveDivisorClassFiber K L n c) = ∑ i ∈ Finset.range (n + 1 - genus), Nat.card K ^ i

Every large degree-n class fiber has the same geometric-sum cardinality.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_eq_classCount_mul_geomSum_of_uniformRiemann (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] (genus threshold n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) : finiteExtensionEffectiveDivisorCount K L n = Nat.card (FiniteExtensionDivisorClassOfDegree K L ↑n) * ∑ i ∈ Finset.range (n + 1 - genus), Nat.card K ^ i

The global effective-divisor coefficient is the number of degree-n classes times the common projective Riemann-space count.

noncomputable def BGS.HasseWeil.finiteExtensionDivisorIndexRepresentative (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : CorvajaZannier.FiniteExtensionDivisor K L

A canonical signed divisor whose degree is the divisor-degree index. It need not be effective; this is why translation is carried out in the class group rather than by adding an effective divisor.

Equations

• BGS.HasseWeil.finiteExtensionDivisorIndexRepresentative K L = Classical.choose ⋯

@[simp]

theorem BGS.HasseWeil.finiteExtensionDivisorIndexRepresentative_degree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : CorvajaZannier.finiteExtensionDivisorDegree K L (finiteExtensionDivisorIndexRepresentative K L) = ↑(finiteExtensionDivisorDegreeIndex K L)

theorem BGS.HasseWeil.finiteExtensionDivisorClassOfDegree_natCard_add_index (K : Type u_1) [Field 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] (n : ℕ) : Nat.card (FiniteExtensionDivisorClassOfDegree K L ↑n) = Nat.card (FiniteExtensionDivisorClassOfDegree K L ↑(n + finiteExtensionDivisorDegreeIndex K L))

Translation by the signed index representative preserves the number of classes when the degree is advanced by the index.

theorem BGS.HasseWeil.geomSum_indexed_recurrence (q ell d : ℕ) : ∑ i ∈ Finset.range (ell + 2 * d), q ^ i + q ^ d * ∑ i ∈ Finset.range ell, q ^ i = (q ^ d + 1) * ∑ i ∈ Finset.range (ell + d), q ^ i

The finite geometric sums satisfy the indexed curve-zeta recurrence.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_indexed_eventual_recurrence (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] (genus threshold n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) : finiteExtensionEffectiveDivisorCount K L (n + 2 * finiteExtensionDivisorDegreeIndex K L) + Nat.card K ^ finiteExtensionDivisorDegreeIndex K L * finiteExtensionEffectiveDivisorCount K L n = (Nat.card K ^ finiteExtensionDivisorDegreeIndex K L + 1) * finiteExtensionEffectiveDivisorCount K L (n + finiteExtensionDivisorDegreeIndex K L)

The actual eventual indexed recurrence for exhaustive effective-divisor counts. The only unproved input is the explicitly stated uniform eventual Riemann formula.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_indexed_eventual_recurrence_int (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] (genus threshold n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) : ↑(finiteExtensionEffectiveDivisorCount K L (n + 2 * finiteExtensionDivisorDegreeIndex K L)) = ↑(Nat.card K ^ finiteExtensionDivisorDegreeIndex K L + 1) * ↑(finiteExtensionEffectiveDivisorCount K L (n + finiteExtensionDivisorDegreeIndex K L)) - ↑(Nat.card K ^ finiteExtensionDivisorDegreeIndex K L) * ↑(finiteExtensionEffectiveDivisorCount K L n)

Subtractive integer form of the indexed recurrence, matching the coefficient hypothesis used by formal zeta rationality.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_indexed_eventual_recurrence_complex (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] (genus threshold n : ℕ) (hconstants : algebraicClosure K L = ⊥) (hRiemann : HasFiniteExtensionUniformEventualRiemannFormula K L genus threshold) (hn : threshold ≤ n) : ↑(finiteExtensionEffectiveDivisorCount K L (n + 2 * finiteExtensionDivisorDegreeIndex K L)) = (↑(Nat.card K) ^ finiteExtensionDivisorDegreeIndex K L + 1) * ↑(finiteExtensionEffectiveDivisorCount K L (n + finiteExtensionDivisorDegreeIndex K L)) - ↑(Nat.card K) ^ finiteExtensionDivisorDegreeIndex K L * ↑(finiteExtensionEffectiveDivisorCount K L n)

Complex form used directly by FormalZetaRationality.