Repartitions and the finite adeles of an affine model

For a Dedekind k-algebra R with fraction field F, a repartition of F / k gives a finite adele of R: retain the entries at the adic places of R and embed each into its adic completion. This map forgets the places outside the affine chart. Its kernel consists exactly of repartitions vanishing on that chart, and it preserves the valuation bounds defining the divisor filtration.

Every finite adele can be approximated to any divisor bound by the image of a finitely supported repartition. This is the comparison between repartitions with entries in F and completion-valued adeles; it imposes no restriction on the residue fields. In particular the comparison map has dense image in the restricted product topology.

The approximation uses the existing strong approximation theorem for finite adeles, IsDedekindDomain.FiniteAdeleRing.exists_forall_valued_sub_le_and_forall_valued_sub_le_one, followed by truncation to the finitely many exceptional coordinates.

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., Sections I.5 and I.7 (repartitions and local components).
• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, Sections 14–15 (completion-valued adeles).

noncomputable def TauCeti.repartitionToFiniteAdeles {k : Type u_1} {F : Type u_2} (R : Type u_3) [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] : ↥(repartitionSpace k F) →+ IsDedekindDomain.FiniteAdeleRing R F

Restriction of a repartition to an affine chart, followed by the embeddings into the adic completions. The omitted places, such as the places at infinity, are forgotten.

Equations

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

@[simp]

theorem TauCeti.repartitionToFiniteAdeles_apply {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (b : ↥(repartitionSpace k F)) (p : IsDedekindDomain.HeightOneSpectrum R) : ((repartitionToFiniteAdeles R) b) p = (algebraMap F (IsDedekindDomain.HeightOneSpectrum.adicCompletion F p)) (↑b (Place.ofPrime k F p))

The comparison map is computed separately at each finite place.

theorem TauCeti.repartitionToFiniteAdeles_smul {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (c : k) (b : ↥(repartitionSpace k F)) : (repartitionToFiniteAdeles R) (c • b) = (algebraMap F (IsDedekindDomain.FiniteAdeleRing R F)) ((algebraMap k F) c) * (repartitionToFiniteAdeles R) b

Scalar multiplication is preserved, with constants embedded diagonally in the finite adeles. This formula does not require choosing a separate constant-field algebra instance on the finite adele ring.

theorem TauCeti.valued_repartitionToFiniteAdeles {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (b : ↥(repartitionSpace k F)) (p : IsDedekindDomain.HeightOneSpectrum R) : Valued.v (((repartitionToFiniteAdeles R) b) p) = (Place.ofPrime k F p).valuation (↑b (Place.ofPrime k F p))

The comparison preserves the value of each retained entry.

@[simp]

theorem TauCeti.repartitionToFiniteAdeles_eq_zero_iff {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (b : ↥(repartitionSpace k F)) : (repartitionToFiniteAdeles R) b = 0 ↔ ∀ (p : IsDedekindDomain.HeightOneSpectrum R), ↑b (Place.ofPrime k F p) = 0

The kernel consists exactly of the repartitions vanishing at every place on the affine chart. Thus the map can have a kernel even though each local embedding is injective.

@[simp]

theorem TauCeti.repartitionToFiniteAdeles_const {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (hF : IsFunctionField k F) (f : F) : (repartitionToFiniteAdeles R) ⟨Function.const (Place k F) f, ⋯⟩ = (algebraMap F (IsDedekindDomain.FiniteAdeleRing R F)) f

A diagonal repartition maps to the diagonal finite adele of the same function.

theorem TauCeti.repartitionToFiniteAdeles_valuation_le {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] {D : Divisor k F} {b : ↥(repartitionSpace k F)} (hb : ↑b ∈ adeleFiltration D) (p : IsDedekindDomain.HeightOneSpectrum R) : Valued.v (((repartitionToFiniteAdeles R) b) p) ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D (Place.ofPrime k F p))

A divisor bound on a repartition remains the same bound at each completed finite place.

theorem TauCeti.exists_finite_support_repartition_valuation_sub_le {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] (a : IsDedekindDomain.FiniteAdeleRing R F) (D : Divisor k F) : ∃ (b : ↥(repartitionSpace k F)), (Function.support ↑b).Finite ∧ ∀ (p : IsDedekindDomain.HeightOneSpectrum R), Valued.v (((repartitionToFiniteAdeles R) b) p - a p) ≤ WithZero.exp (AlgebraicGeometry.WeilDivisor.coeff D (Place.ofPrime k F p))

Approximation to every divisor bound by finitely supported repartitions. For a finite adele a and any divisor D, there is a repartition b with finite support such that the error at each finite place P has valuation at most exp (D P).

The bound is multiplicative, so it includes zero errors even at negative coefficients of D. No function-field, exact-constants, or perfectness hypothesis is needed.

theorem TauCeti.denseRange_repartitionToFiniteAdeles {k : Type u_1} {F : Type u_2} {R : Type u_3} [Field k] [Field F] [CommRing R] [IsDedekindDomain R] [Algebra k R] [Algebra R F] [IsFractionRing R F] [Algebra k F] [IsScalarTower k R F] : DenseRange ⇑(repartitionToFiniteAdeles R)

Repartitions have dense image in the finite adeles of every Dedekind affine model. This holds even without a function-field hypothesis.