For a Dedekind domain, UFD implies PID

Stream: Is there code for X?

[Raphael Douglas Giles]

For Dedekind domains, being a UFD and being a PID are equivalent. This doesn't seem to be in mathlib yet as far as I can tell. Does anyone have this lying around in a ForMathlib folder somewhere?

[Riccardo Brasca]

Not sure if someone has this, but it should be quite easy, we have everything is needed, in particular the fact that it is enough to prove that prime ideals are principal.

[Kenny Lau]

import Mathlib.RingTheory.DedekindDomain.Dvr
import Mathlib.RingTheory.PrincipalIdealDomainOfPrime

theorem PID_of_UFD_of_dedekind (R : Type*) [CommRing R]
    [IsDedekindDomain R] [UniqueFactorizationMonoid R] :
    IsPrincipalIdealRing R := by
  refine .of_prime fun P hp ↦ ?_
  by_cases hp₀ : P = ⊥
  · rw [hp₀]
    infer_instance
  obtain ⟨x, hx₁, hx₂⟩ := hp.exists_mem_prime_of_ne_bot hp₀
  suffices Ideal.span {x} = P by
    rw [← this]
    infer_instance
  have h₁ : (Ideal.span {x}).IsPrime := (Ideal.span_singleton_prime hx₂.ne_zero).mpr hx₂
  have h₂ := h₁.isMaximal (by simpa using hx₂.ne_zero)
  exact h₂.eq_of_le hp.ne_top <| (Ideal.span_singleton_le_iff_mem _).mpr hx₁

#min_imports

[Kenny Lau]

@Riccardo Brasca which file would this go to?

[Riccardo Brasca]

What does find_home! says?

[Riccardo Brasca]

Now I am curious to see if I can find a better proof :)

[Riccardo Brasca]

it seems longer than I thought

[Kenny Lau]

Riccardo Brasca said:

What does find_home! says?

Mathlib

[Kenny Lau]

i guess i can make a new file within DedekindDomain/

[Riccardo Brasca]

import Mathlib

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

open Ideal

lemma foo : IsPrincipalIdealRing R := by
  refine IsPrincipalIdealRing.of_prime (fun p hp ↦ ?_)
  by_cases h0 : p = ⊥
  · exact h0 ▸ bot_isPrincipal
  obtain ⟨x, hxmem, hxprime⟩ := hp.exists_mem_prime_of_ne_bot h0
  refine ⟨x, (IsMaximal.eq_of_le ?_ hp.ne_top (span_le.2 (by simp [hxmem]))).symm⟩
  refine Ring.DimensionLEOne.maximalOfPrime (by simpa using hxprime.ne_zero)
    ((span_singleton_prime hxprime.ne_zero).2 hxprime)

[Riccardo Brasca]

But find_home! still says mathlib, so a new file is probably a good idea.

[Riccardo Brasca]

Anyway we can improve IsPrincipalIdealRing.of_prime doing the bot case

[Riccardo Brasca]

I realize it's literally the same proof, sorry I couldn't resist writing one myself.

[Kenny Lau]

import Mathlib

theorem PID_of_UFD_of_dedekind (R : Type*) [CommRing R]
    [IsDedekindDomain R] [UniqueFactorizationMonoid R] :
    IsPrincipalIdealRing R := by
  refine .of_prime fun P hp ↦ (eq_or_ne P ⊥).elim (· ▸ inferInstance) fun hp₀ ↦ ?_
  obtain ⟨x, hx₁, hx₂⟩ := hp.exists_mem_prime_of_ne_bot hp₀
  have := (Ideal.span_singleton_prime hx₂.ne_zero).mpr hx₂
  exact (Ring.DimensionLeOne.prime_le_prime_iff_eq (by simp [hx₂.ne_zero])).mp
    ((Ideal.span_singleton_le_iff_mem _).mpr hx₁) ▸ inferInstance

I tried to do trivial (and vertical) golfing on my proof

[Riccardo Brasca]

If you open a PR please modify the statement of IsPrincipalIdealRing.of_prime.

[Kenny Lau]

@Riccardo Brasca #31061