Splitting effective exhaustive divisors at infinity

An effective divisor on the exhaustive place type of a finite extension of K(X) is a finitely supported natural-number-valued function. Since that place type is a sum of finite and above-infinity places, such a divisor splits canonically into its finite and infinity parts.

This file records the inverse equivalence, degree additivity, the conversion to the repository's integer-valued effective divisors, and the resulting fixed-degree convolution. The finite component is also identified with a nonzero ideal in the normalization of K[X].

@[reducible, inline]

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

Effective divisors on all exhaustive places.

Equations

• BGS.HasseWeil.FiniteExtensionEffectiveDivisor K L = (BGS.CorvajaZannier.FiniteExtensionPlace K L →₀ ℕ)

@[reducible, inline]

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

Effective divisors supported above the place at infinity.

Equations

• BGS.HasseWeil.FiniteExtensionEffectiveInfinityDivisor K L = (↑(BGS.CorvajaZannier.FiniteExtensionInfinityPlace K L) →₀ ℕ)

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorDegree (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) : ℕ

Natural-number degree of an effective exhaustive divisor.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveInfinityDivisorDegree (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionEffectiveInfinityDivisor K L) : ℕ

Natural-number degree of an effective divisor supported at infinity.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitEquiv (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FiniteExtensionEffectiveDivisor K L ≃ (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) × FiniteExtensionEffectiveInfinityDivisor K L

An effective exhaustive divisor is exactly a pair consisting of its finite-place and infinity-place components.

Equations

• BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitEquiv K L = Finsupp.sumFinsuppEquivProdFinsupp

@[simp]

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitEquiv_finite_apply (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionEffectiveDivisor K L) (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : ((finiteExtensionEffectiveDivisorSplitEquiv K L) D).1 P = D (Sum.inl P)

@[simp]

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitEquiv_infinity_apply (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionEffectiveDivisor K L) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ((finiteExtensionEffectiveDivisorSplitEquiv K L) D).2 P = D (Sum.inr P)

@[simp]

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitEquiv_symm_inl (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) × FiniteExtensionEffectiveInfinityDivisor K L) (P : CorvajaZannier.FiniteExtensionFinitePlace K L) : ((finiteExtensionEffectiveDivisorSplitEquiv K L).symm D) (Sum.inl P) = D.1 P

@[simp]

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitEquiv_symm_inr (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) × FiniteExtensionEffectiveInfinityDivisor K L) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : ((finiteExtensionEffectiveDivisorSplitEquiv K L).symm D) (Sum.inr P) = D.2 P

theorem BGS.HasseWeil.finiteExtensionEffectiveFiniteDivisorDegree_eq_placeDegree (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.FiniteExtensionFinitePlace K L →₀ ℕ) : finiteExtensionEffectiveFiniteDivisorDegree K L D = D.sum fun (P : CorvajaZannier.FiniteExtensionFinitePlace K L) (e : ℕ) => e * CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl P)

The existing finite-divisor degree is the restriction of exhaustive place degree to the finite branch.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorDegree_split (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 : FiniteExtensionEffectiveDivisor K L) : finiteExtensionEffectiveDivisorDegree K L D = finiteExtensionEffectiveFiniteDivisorDegree K L ((finiteExtensionEffectiveDivisorSplitEquiv K L) D).1 + finiteExtensionEffectiveInfinityDivisorDegree K L ((finiteExtensionEffectiveDivisorSplitEquiv K L) D).2

Degree is additive across the finite/infinity split.

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

Cast an effective natural-number divisor to the integer-valued divisor type used by Riemann spaces and divisor classes.

Equations

• BGS.HasseWeil.finiteExtensionEffectiveDivisorToDivisor K L D = Finsupp.mapRange (fun (n : ℕ) => ↑n) BGS.HasseWeil.finiteExtensionEffectiveDivisorToDivisor._proof_1 D

@[simp]

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorToDivisor_apply (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionEffectiveDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) : (finiteExtensionEffectiveDivisorToDivisor K L D) P = ↑(D P)

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorToDivisor_effective (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (D : FiniteExtensionEffectiveDivisor K L) (P : CorvajaZannier.FiniteExtensionPlace K L) : 0 ≤ (finiteExtensionEffectiveDivisorToDivisor K L D) P

The cast divisor is effective.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorDegree_cast (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) = CorvajaZannier.finiteExtensionDivisorDegree K L (finiteExtensionEffectiveDivisorToDivisor K L D)

Natural degree casts to the integer degree of the associated exhaustive divisor.

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorEquivEffectiveIntegralDivisor (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : FiniteExtensionEffectiveDivisor K L ≃ { D : CorvajaZannier.FiniteExtensionDivisor K L // ∀ (P : CorvajaZannier.FiniteExtensionPlace K L), 0 ≤ D P }

Natural effective exhaustive divisors are equivalent to the subtype of pointwise-effective integer-valued exhaustive divisors.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorAffineInfinityEquiv (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] : FiniteExtensionEffectiveDivisor K L ≃ ↥(FiniteExtensionAffineIdeal K L) × FiniteExtensionEffectiveInfinityDivisor K L

Splitting an effective exhaustive divisor and replacing its finite part by the corresponding nonzero affine ideal.

Equations

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

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorDegree_eq_affine_add_infinity (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] [Finite K] (D : FiniteExtensionEffectiveDivisor K L) : finiteExtensionEffectiveDivisorDegree K L D = finiteExtensionAffineIdealDegree K L ((finiteExtensionEffectiveDivisorAffineInfinityEquiv K L) D).1 + finiteExtensionEffectiveInfinityDivisorDegree K L ((finiteExtensionEffectiveDivisorAffineInfinityEquiv K L) D).2

Under the ideal/infinity equivalence, exhaustive degree is affine ideal degree plus infinity degree.

theorem BGS.HasseWeil.effectiveDivisorInfinityPlaceFinite (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] : Finite ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)

theorem BGS.HasseWeil.finiteExtensionEffectiveInfinityDivisor_apply_le_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] (D : FiniteExtensionEffectiveInfinityDivisor K L) (P : ↑(CorvajaZannier.FiniteExtensionInfinityPlace K L)) : D P ≤ finiteExtensionEffectiveInfinityDivisorDegree K L D

Every infinity coefficient is bounded by the weighted degree.

@[instance_reducible]

noncomputable instance BGS.HasseWeil.finiteExtensionEffectiveInfinityDivisorsOfDegreeFintype (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 : ℕ) : Fintype { D : FiniteExtensionEffectiveInfinityDivisor K L // finiteExtensionEffectiveInfinityDivisorDegree K L D = n }

Effective infinity divisors of a fixed degree form a finite type.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveInfinityDivisorCount (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 : ℕ) : ℕ

The effective-infinity-divisor coefficient of degree n.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorsOfDegreeSplitEquiv (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 : FiniteExtensionEffectiveDivisor K L // finiteExtensionEffectiveDivisorDegree K L D = n } ≃ (m : Fin (n + 1)) × { D : (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) × FiniteExtensionEffectiveInfinityDivisor K L // finiteExtensionEffectiveFiniteDivisorDegree K L D.1 = ↑m ∧ finiteExtensionEffectiveInfinityDivisorDegree K L D.2 = n - ↑m }

Fixed-degree effective exhaustive divisors split according to the degree of their finite component.

Equations

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

def BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitFiberEquiv (K : Type u_1) [Field K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] (n : ℕ) (m : Fin (n + 1)) : { D : (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) × FiniteExtensionEffectiveInfinityDivisor K L // finiteExtensionEffectiveFiniteDivisorDegree K L D.1 = ↑m ∧ finiteExtensionEffectiveInfinityDivisorDegree K L D.2 = n - ↑m } ≃ { D : CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ // finiteExtensionEffectiveFiniteDivisorDegree K L D = ↑m } × { D : FiniteExtensionEffectiveInfinityDivisor K L // finiteExtensionEffectiveInfinityDivisorDegree K L D = n - ↑m }

Each fixed split-degree fiber is the product of its finite and infinity fixed-degree components.

Equations

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

@[instance_reducible]

noncomputable instance BGS.HasseWeil.finiteExtensionEffectiveDivisorSplitFiberFintype (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] (n : ℕ) (m : Fin (n + 1)) : Fintype { D : (CorvajaZannier.FiniteExtensionFinitePlace K L →₀ ℕ) × FiniteExtensionEffectiveInfinityDivisor K L // finiteExtensionEffectiveFiniteDivisorDegree K L D.1 = ↑m ∧ finiteExtensionEffectiveInfinityDivisorDegree K L D.2 = n - ↑m }

Equations

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

@[instance_reducible]

noncomputable instance BGS.HasseWeil.finiteExtensionEffectiveDivisorsOfDegreeFintype (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] (n : ℕ) : Fintype { D : FiniteExtensionEffectiveDivisor K L // finiteExtensionEffectiveDivisorDegree K L D = n }

Effective exhaustive divisors of fixed degree form a finite type.

Equations

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

noncomputable def BGS.HasseWeil.finiteExtensionEffectiveDivisorCount (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] (n : ℕ) : ℕ

The effective-exhaustive-divisor coefficient of degree n.

Equations

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

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_eq_sum_mul_infinityCount (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] (n : ℕ) : finiteExtensionEffectiveDivisorCount K L n = ∑ m : Fin (n + 1), finiteExtensionEffectiveFiniteDivisorCount K L ↑m * finiteExtensionEffectiveInfinityDivisorCount K L (n - ↑m)

Fixed-degree exhaustive divisor counts are the convolution of the affine ideal coefficients with the infinity-divisor coefficients.

theorem BGS.HasseWeil.finiteExtensionEffectiveDivisorCount_eq_sum_affineIdealCount_mul_infinityCount (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] (n : ℕ) : finiteExtensionEffectiveDivisorCount K L n = ∑ m : Fin (n + 1), finiteExtensionAffineIdealCount K L ↑m * finiteExtensionEffectiveInfinityDivisorCount K L (n - ↑m)

The same convolution with the finite coefficient written as the affine ideal count in the normalization of K[X].