Prove an ideal is Prime

Stream: new members

[Chengyan Hu]

Hi! I missed at a strange part, and I believe it should not be hard. I just want to prove an Ideal is prime, given that it's prime in R1, and R1 R2 are isomorphic.

import Mathlib
open Field
open LinearMap Module
open scoped NumberField
open IsDedekindDomain
open NumberField

/-- The height-one prime of `OQ` lying over the rational prime `p`, i.e. `(p)`. -/
noncomputable def placeOfNat (p : ℕ) [hp : Fact p.Prime] :
    HeightOneSpectrum (𝓞 ℚ):= by
    let I : Ideal (𝓞 ℚ) := Ideal.span ({algebraMap ℤ (𝓞 ℚ) p})
    have e := RingOfIntegers.equiv (K := ℚ) ℤ
    have hpZ : Prime (p : ℤ) := by
      simpa [Int.prime_iff_natAbs_prime] using hp.out
    have hI : Prime I := by
      sorry
    refine HeightOneSpectrum.ofPrime hI

[Aaron Liu]

well I got a proof

import Mathlib
open Field
open LinearMap Module
open scoped NumberField
open IsDedekindDomain
open NumberField

/-- The height-one prime of `OQ` lying over the rational prime `p`, i.e. `(p)`. -/
noncomputable def placeOfNat (p : ℕ) [hp : Fact p.Prime] :
    HeightOneSpectrum (𝓞 ℚ):= by
    let I : Ideal (𝓞 ℚ) := Ideal.span ({algebraMap ℤ (𝓞 ℚ) p})
    have e := RingOfIntegers.equiv (K := ℚ) ℤ
    have hpZ : Prime (p : ℤ) := by
      simpa [Int.prime_iff_natAbs_prime] using hp.out
    have hI : Prime I := by
      unfold I
      apply Ideal.prime_of_isPrime
      · rw [ne_eq, Ideal.span_singleton_eq_bot]
        simp [hp.elim.ne_zero]
      rw [← Set.image_singleton, ← Ideal.map_span]
      have he : e.symm = algebraMap ℤ (𝓞 ℚ) := by
        subsingleton
      rw [← he]
      -- I shouldn't have to do this step
      change (Ideal.map e.symm (Ideal.span {(p : ℤ)})).IsPrime
      rw [Ideal.map_symm]
      apply Ideal.comap_isPrime
    refine HeightOneSpectrum.ofPrime hI

[Chengyan Hu]

Thanks a lot! That's clever.

[Kevin Buzzard]

Oh we have this in FLT: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

[Chengyan Hu]

Great! Out of expection