Placing a definition in `DedekindDomain.Ideal`

Stream: mathlib4

[Xavier Généreux]

Hi everyone :sunny:,

I would like to know if anyone has any recommandation on where I could PR the following fact:

import Mathlib

variable {R : Type*} [CommRing R] [IsDedekindDomain R]

open Polynomial Ideal in
def IsDedekindDomain.HeightOneSpectrum.of_irreducible [DecompositionMonoid R]
    {p : R} (hp : Irreducible p) : HeightOneSpectrum R where
  asIdeal := Ideal.span { p }
  isPrime := Ideal.isPrime_of_prime
    <| by simp [Ideal.prime_span_singleton_iff, (Irreducible.prime hp)]
  ne_bot := by simp only [ne_eq, span_singleton_eq_bot, Irreducible.ne_zero hp, not_false_eq_true]

theorem IsDedekindDomain.HeightOneSpectrum.of_irreducible_asIdeal
    [DecompositionMonoid R] {p : R} (hp : Irreducible p) :
  (IsDedekindDomain.HeightOneSpectrum.of_irreducible hp).asIdeal = Ideal.span { p } := rfl

---

I think this would fit well somewhere in the DedekindDomain.Ideal file. I was thinking that maybe close to the PID section (found at line 1320) would be a good fit? Let me know what you think!

Thanks:)
Xavier

[Xavier Généreux]

And btw #find_home! also suggests this file. The question is where in the file would make the most sense!

[Jz Pan]

I think it should named ofIrreducible since HeightOneSpectrum R is a Type.

[Xavier Généreux]

Yeah I agree

[Filippo A. E. Nuccio]

I confess I have a math question here, and apologies if it is stupid: are there Dedekind domains that are decomposition monoids without being UFD's, so not PID's?

[Antoine Chambert-Loir]

I believe there aren't. See the paper of Cohn, theorem 2.3 https://lohar.com/researchpdf/bezout_rings_and_their_subrings.pdf

[Andrew Yang]

I don't think we should have this. We should instead have ofPrime (that could go in Mathlib.RingTheory.DedekindDomain.Ideal):

import Mathlib

variable {R : Type*} [CommRing R] [IsDedekindDomain R]

open Polynomial Ideal IsDedekindDomain

@[simps]
def IsDedekindDomain.HeightOneSpectrum.ofPrime (p : Ideal R) (hp : Prime p) : HeightOneSpectrum R where
  asIdeal := p
  isPrime := Ideal.isPrime_of_prime hp
  ne_bot := hp.ne_zero

And the construction in the OP is then

example [DecompositionMonoid R]
    {p : R} (hp : Irreducible p) : HeightOneSpectrum R :=
  .ofPrime (.span {p}) (by simpa using hp.prime)

[Antoine Chambert-Loir]

I guess a lemma doing the last part would be useful, passing from Irreducible to Prime (span R {p}).

[Jz Pan]

I think the IsDedekindDomain.HeightOneSpectrum.of_irreducible_asIdeal can be obtained by add a @[simps] to the def ....

[Xavier Généreux]

Thank you all for the answers.
See #24036 for the suggested lemma for ofPrime. I can add the corollaries for elements of R (like for {p : R} (hp : Irreducible p)) if people think this is interesting but @Andrew Yang is right that it is somewhat straightforward using directly ofPrime.