Bad primes are finite

Stream: Is there code for X?

[Kevin Buzzard]

For many number-theoretic objects there is a finite collection of "bad primes" where things aren't smooth/integral/whatever. Here is a basic example which is actually algebra rather than arithmetic, with proof extracted from this lemma of Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean:

import Mathlib.RingTheory.DedekindDomain.AdicValuation
import Mathlib.RingTheory.DedekindDomain.Factorization
import Mathlib.Algebra.Order.GroupWithZero.WithZero

open Set IsDedekindDomain IsDedekindDomain.HeightOneSpectrum

variable (R : Type*) [CommRing R] [IsDedekindDomain R] {K : Type*}
    [Field K] [Algebra R K] [IsFractionRing R K]

def BadPrimes (k : K) : Set (HeightOneSpectrum R) :=
    {v | (k : v.adicCompletion K) ∉ v.adicCompletionIntegers K}

lemma BadPrimes.finite (k : K) : (BadPrimes R k).Finite := by
  unfold BadPrimes
  simp_rw [mem_adicCompletionIntegers,
    adicCompletion, Valued.valuedCompletion_apply, not_le]
  change {v : HeightOneSpectrum R | 1 < v.valuation K k}.Finite
  obtain ⟨⟨n, ⟨d, hd⟩⟩, hk⟩ := IsLocalization.surj (nonZeroDivisors R) k
  have hd' : d ≠ 0 := nonZeroDivisors.ne_zero hd
  suffices {v : HeightOneSpectrum R | v.valuation K (algebraMap R K d) < 1}.Finite by
    apply Finite.subset this
    intro v hv
    apply_fun v.valuation K at hk
    simp only [Valuation.map_mul, valuation_of_algebraMap] at hk
    rw [mem_setOf_eq, valuation_of_algebraMap]
    have := intValuation_le_one v n
    contrapose! this
    change 1 < v.intValuation n
    rw [← hk, mul_comm]
    exact (lt_mul_of_one_lt_right (by simp) hv).trans_le <|
      mul_le_mul_of_nonneg_right this (by simp)
  simp_rw [valuation_of_algebraMap]
  change {v : HeightOneSpectrum R | v.intValuationDef d < 1}.Finite
  simp_rw [intValuation_lt_one_iff_dvd]
  apply Ideal.finite_factors
  simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]

This argument feels a bit long, and I also wonder whether it occurs anywhere else in mathlib as well as in the middle of a proof about finite adeles (which I'm refactoring by the way, to use restricted products, which hit mathlib recently; this is why I'm interested). Is this the definition we want or should we stick with {v : HeightOneSpectrum R | 1 < v.valuation K k}.Finite? Where should this go? It surely shouldn't be in FiniteAdeleRing.

[Johan Commelin]

Is this the definition we want

What does that refer to? Are you asking whether BadPrimes should exist as a name? And whether it should be a name for that specific set?

[Kevin Buzzard]

I mean there are lots of ways of saying "I am not integral at this set", and maybe introducing completions is completely overkill?

[Johan Commelin]

If introducing completions is overkill, then it is certainly complete overkill :grinning:

[Johan Commelin]

{v : HeightOneSpectrum R | 1 < v.valuation K k}.Finite also looks fine to me.

[Jz Pan]

What about "support of k"?

[Jz Pan]

{v : HeightOneSpectrum R | v.valuation K k \neq 0} should be finite, by considering the principal fraction ideal generated by k and use docs#FractionalIdeal.finite_factors