Element of a Dedekind domain only has finitely many divisors

Stream: Is there code for X?

[Kevin Buzzard]

I need that a non-zero element of a Dedekind domain only has finitely many prime divisors. The variant I need is this, but is there anything close?

example (R : Type*) [CommRing R] [IsDedekindDomain R] (d : R) (hd : d ≠ 0) :
  {v : HeightOneSpectrum R | v.intValuation d < 1}.Finite := sorry

[Adam Topaz]

docs#Ideal.finite_factors is promising

[Adam Topaz]

That file also has some stuff about fractional ideals which would be more appropriate if you want to do this for elements of the fraction field as well

[Junyan Xu]

This holds for all 1D noetherian domains: https://math.stackexchange.com/a/3930565/12932

[Filippo A. E. Nuccio]

import Mathlib.RingTheory.DedekindDomain.AdicValuation
import Mathlib.RingTheory.DedekindDomain.Factorization

open IsDedekindDomain IsDedekindDomain.HeightOneSpectrum

example (R : Type*) [CommRing R] [IsDedekindDomain R] (d : R) (hd : d ≠ 0) :
  {v : HeightOneSpectrum R | v.intValuation d < 1}.Finite := by
  change {v : HeightOneSpectrum R | v.intValuationDef d < 1}.Finite
  simp_rw [int_valuation_lt_one_iff_dvd]
  apply Ideal.finite_factors
  simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]

[Kevin Buzzard]

Thanks!

[Ruben Van de Velde]

Wow, the naming around intValuationDef is a mess:

• IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos
• IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd
• IsDedekindDomain.HeightOneSpectrum.IntValuation.map_zero'

[Filippo A. E. Nuccio]

OK, I agree. It probably calls for a fixing PR... I might try this later on unless @Ruben Van de Velde you're already on it.

[Ruben Van de Velde]

I'm perfectly happy for someone else to take it on :)

[Yaël Dillies]

(Please apply the new #naming convention around namespaced declarations :pray:)

[Kevin Buzzard]

So what I actually want is

example (R : Type*) [CommRing R] [IsDedekindDomain R] [Algebra R K] [IsFractionRing R K]
    (k : K) : {v : HeightOneSpectrum R | 1 < v.valuation k}.Finite :=
  sorry

but I had reduced it to the integral case using some slightly painful arithmetic in ℤₘ₀ (in particular I had to prove some inequalities which were a bit painful because of a lack of tactic which would do it for me). Can this example be done directly without reducing to the integral case?

[Adam Topaz]

You could use FractionalIdeal.finite_factors

[Adam Topaz]

Or FractionalIdeal.finite_factors' (with this one I hope that Filippo's argument could be modified to work)

[Adam Topaz]

That would give you finiteness of the support of k (i.e. those valuations where k is not a unit at the valuation ring), and you could get finiteness of the set you want because it's a subset of the support.

[Kevin Buzzard]

Ok my reduction to the integral case is now less painful but I'll take a look at this too because it's the right way to do it (although you need a case split on whether k=0 in this route)

[Adam Topaz]

Honestly I'm surprised we don't have a better API for such supports

[Kevin Buzzard]

Yeah I know Anne and Maria Ines did a bunch of work here, but this is the first time I'm using it myself and I'm still finding my feet.

[Filippo A. E. Nuccio]

Just because I got trapped into this, I post one solution, that " reduces to the integral case but only a little bit". At any rate I still agree we lack a good API.

lemma bar (R : Type*) [CommRing R] [IsDedekindDomain R] (d : R) (hd : d ≠ 0) :
  {v : HeightOneSpectrum R | v.intValuation d < 1}.Finite := by
  change {v : HeightOneSpectrum R | v.intValuationDef d < 1}.Finite
  simp_rw [int_valuation_lt_one_iff_dvd]
  apply Ideal.finite_factors
  simpa only [Submodule.zero_eq_bot, ne_eq, Ideal.span_singleton_eq_bot]

lemma foo (K : Type*) [Field K] (R : Type*) [CommRing R] [IsDedekindDomain R] [Algebra R K]
    [IsFractionRing R K] (k : K) (hk₀ : k ≠ 0) :
    {v : HeightOneSpectrum R | v.valuation k < 1}.Finite := by
  obtain ⟨r, ⟨s₀, hs₀, rfl⟩⟩ := IsFractionRing.div_surjective (A := R) (K := K) k
  have hr₀ : r ≠ 0 := by
    intro abs
    simp only [abs, map_zero, zero_div, ne_eq, not_true_eq_false] at hk₀
  simp_rw [← IsFractionRing.mk'_mk_eq_div hs₀, @valuation_of_mk' R _ _ K _ _ _]
  suffices {v : HeightOneSpectrum R | v.intValuation r / v.intValuation s₀ < 1} ⊆
    {v : HeightOneSpectrum R | v.intValuation r < 1 } by
    apply Set.Finite.subset (bar R r hr₀) this
  intro v h
  have hr_val : v.intValuation r ≠ 0 := int_valuation_ne_zero _ _ hr₀
  have hs_val : v.intValuation s₀ ≠ 0 := int_valuation_ne_zero _ _ (nonZeroDivisors.ne_zero hs₀)
  rw [Set.mem_setOf_eq, ← WithZero.coe_unzero hr_val, ← WithZero.coe_one, ← WithZero.coe_unzero hs_val,
    ← WithZero.coe_div, WithZero.coe_lt_coe] at h
  rw [Set.mem_setOf_eq, ← WithZero.coe_unzero hr_val, ← WithZero.coe_one, WithZero.coe_lt_coe]
  apply lt_of_le_of_lt ((le_div_self_iff _).mpr _) h
  rw [← WithZero.coe_le_coe, WithZero.coe_one, WithZero.coe_unzero hs_val]
  apply int_valuation_le_one

example (K : Type*) [Field K] (R : Type*) [CommRing R] [IsDedekindDomain R] [Algebra R K]
    [IsFractionRing R K] (k : K) (hk₀ : k ≠ 0) :
    {v : HeightOneSpectrum R | 1 < v.valuation k}.Finite := by
  convert foo K R (k⁻¹) (inv_ne_zero hk₀) using 1
  ext v
  have hvk : (v.valuation k) ≠ 0 := by simpa only [ne_eq, map_eq_zero]
  simp only [map_inv₀, coe_one, Set.mem_setOf_eq, gt_iff_lt]
  rw [← WithZero.coe_unzero hvk, ← WithZero.coe_one, WithZero.coe_lt_coe, ← WithZero.coe_inv,
    WithZero.coe_lt_coe, ← one_lt_inv', inv_inv]

[Filippo A. E. Nuccio]

In our project with @María Inés de Frutos Fernández we improve the API for the type $\mathbb{Z}_{m0}$, see in particular the file https://github.com/mariainesdff/LocalClassFieldTheory/blob/master/LocalClassFieldTheory/ForMathlib/WithZero.lean
that will soon be PR'd.

[Kevin Buzzard]

I think that a bunch of stuff there (e.g. withZeroMultIntToNNReal_pos) just follows from general lemmas like mul_pos once #13111 is merged.

[Filippo A. E. Nuccio]

Oh sure, thanks for the hint!

[Kevin Buzzard]

By the way @Filippo A. E. Nuccio I used your original argument to prove that the finite adeles were a $K$-algebra in #13021

[Filippo A. E. Nuccio]

I might have a round of review to both these PR's.

[Riccardo Brasca]

Note that #13111 is awaiting-author

[Riccardo Brasca]

Having a look at #13020

[Kevin Buzzard]

Yeah I changed it to that a couple of hours ago myself, because Yael told me I should move it to a new file, and then I realised that probably I should add the symmetric versions of both instances as well (except that I have a meeting in ten minutes :-/ )

[Filippo A. E. Nuccio]

Having a look at #13021

[Kevin Buzzard]

OK I just made it. Sorry about the code duplication :-)

[Filippo A. E. Nuccio]

Also, #13111 currently has some build issue.

[Ruben Van de Velde]

Filippo A. E. Nuccio said:

Also, #13111 currently has some build issue.

I pushed a fix, Yaël moved a file that you imported :)