Local trace image for cotrace maximality

This file formalizes the exact local trace-image argument in Stichtenoth, Theorem 3.4.6, Step (b1). Weak approximation creates an element just outside the complementary module at an offending extension place; trace duality then shows that any prescribed base element of order -1 is a trace without losing the required lower bounds at the places over the chosen base place.

def BGS.HasseWeil.heightOneOfPrimesOverFinset (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (p : IsDedekindDomain.HeightOneSpectrum A) (Q : Ideal B) (hQ : Q ∈ IsDedekindDomain.primesOverFinset p.asIdeal B) : IsDedekindDomain.HeightOneSpectrum B

Rebuild a height-one prime from an ideal in the finite primes-over set.

Equations

• BGS.HasseWeil.heightOneOfPrimesOverFinset A p Q hQ = { asIdeal := Q, isPrime := ⋯, ne_bot := ⋯ }

@[simp]

theorem BGS.HasseWeil.heightOneOfPrimesOverFinset_asIdeal (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (p : IsDedekindDomain.HeightOneSpectrum A) (Q : Ideal B) (hQ : Q ∈ IsDedekindDomain.primesOverFinset p.asIdeal B) : (heightOneOfPrimesOverFinset A p Q hQ).asIdeal = Q

theorem BGS.HasseWeil.mem_primesOverFinset_iff_under_eq (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] (p : IsDedekindDomain.HeightOneSpectrum A) (q : IsDedekindDomain.HeightOneSpectrum B) : q.asIdeal ∈ IsDedekindDomain.primesOverFinset p.asIdeal B ↔ IsDedekindDomain.HeightOneSpectrum.under A q = p

Membership in the finite primes-over set is equivalent to contraction to the selected height-one prime.

theorem BGS.HasseWeil.prime_of_mem_primesOverFinset (A : Type u_1) {B : Type u_3} [CommRing A] [CommRing B] [Algebra A B] [IsDedekindDomain A] [IsDedekindDomain B] [Module.IsTorsionFree A B] (p : IsDedekindDomain.HeightOneSpectrum A) (Q : Ideal B) (hQ : Q ∈ IsDedekindDomain.primesOverFinset p.asIdeal B) : Prime Q

Every ideal selected by primesOverFinset is prime in the factorization monoid sense required by the weak-approximation theorem.

theorem BGS.HasseWeil.le_count_spanSingleton_of_valuation_le_exp_neg {L : Type u} {B : Type u_3} [CommRing B] [Field L] [Algebra B L] [IsFractionRing B L] [IsDedekindDomain B] (q : IsDedekindDomain.HeightOneSpectrum B) {x : L} (hx : x ≠ 0) (n : ℤ) (hval : (IsDedekindDomain.HeightOneSpectrum.valuation L q) x ≤ WithZero.exp (-n)) : n ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) x)

A valuation bound on a nonzero element gives the corresponding lower bound for its principal fractional-ideal coefficient.

theorem BGS.HasseWeil.exists_element_with_counts_over_and_exact_at (A : Type u_1) {L : Type u} {B : Type u_3} [CommRing A] [CommRing B] [Field L] [Algebra B L] [Algebra A B] [IsDedekindDomain A] [IsFractionRing B L] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] (p : IsDedekindDomain.HeightOneSpectrum A) (n : IsDedekindDomain.HeightOneSpectrum B → ℤ) (q₀ : IsDedekindDomain.HeightOneSpectrum B) (hq₀ : IsDedekindDomain.HeightOneSpectrum.under A q₀ = p) (hn₀ : n q₀ < 0) : ∃ (u : L), u ≠ 0 ∧ (∀ (q : IsDedekindDomain.HeightOneSpectrum B), IsDedekindDomain.HeightOneSpectrum.under A q = p → n q ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) u)) ∧ FractionalIdeal.count L q₀ ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) u) = n q₀ ∧ ∀ (q : IsDedekindDomain.HeightOneSpectrum B), IsDedekindDomain.HeightOneSpectrum.under A q ≠ p → 0 ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) u)

Weak approximation realizes simultaneous lower order bounds over one base prime and realizes a prescribed negative order exactly at one chosen prime.

theorem BGS.HasseWeil.exists_trace_eq_of_count_threshold_lt_neg_different (A : Type u_1) (K₀ : Type u_2) {L : Type u} {B : Type u_3} [CommRing A] [Field K₀] [CommRing B] [Field L] [Algebra A K₀] [Algebra B L] [Algebra A B] [Algebra K₀ L] [Algebra A L] [IsScalarTower A K₀ L] [IsScalarTower A B L] [IsDedekindDomain A] [IsFractionRing A K₀] [FiniteDimensional K₀ L] [Algebra.IsSeparable K₀ L] [IsIntegralClosure B A L] [IsFractionRing B L] [IsDedekindDomain B] [Module.IsTorsionFree A B] [Algebra.IsIntegral A B] (p : IsDedekindDomain.HeightOneSpectrum A) (n : IsDedekindDomain.HeightOneSpectrum B → ℤ) (q₀ : IsDedekindDomain.HeightOneSpectrum B) (hq₀ : IsDedekindDomain.HeightOneSpectrum.under A q₀ = p) (hbad : n q₀ < -↑(multiplicity q₀.asIdeal (differentIdeal A B))) (w : K₀) (hw : w ≠ 0) (hwVal : (IsDedekindDomain.HeightOneSpectrum.valuation K₀ p) w = WithZero.exp 1) : ∃ (z : L), z ≠ 0 ∧ (Algebra.trace K₀ L) z = w ∧ ∀ (q : IsDedekindDomain.HeightOneSpectrum B), IsDedekindDomain.HeightOneSpectrum.under A q = p → n q ≤ FractionalIdeal.count L q ((FractionalIdeal.spanSingleton (nonZeroDivisors B)) z)

If one local order bound is strictly below the complementary-module threshold, then every element of base order -1 occurs as a trace while all the prescribed order bounds over the chosen base prime are retained.

This is the algebraic core of Stichtenoth, Theorem 3.4.6, Step 1(b).