Typeclass search for mem notation

Stream: mathlib4

[Calvin Lee]

(deleted)

[Calvin Lee]

Here's my #xy problem:
I'm working on the definition of krull dimension for prime ideals in a ring.

variable {R : Type _} [CommRing R] (I : Ideal R)
protected noncomputable def Ideal.height  [h : IsPrime I] : WithBot ℕ∞ :=
  ⟨I, h⟩ |> height (PrimeSpectrum R)

in particular, this definition needs typeclass search to find a proof that the ideal is prime, which works well for elements of the prime and maximal spectrums of R.

However, consider the following theorem:

theorem minimal_primes_height_1_of_principal (x : R) :
    ∀ p ∈ (Ideal.span {x}).minimalPrimes, p.height = 1 := sorry

In this case, we p.height fails to synthesize the instance IsPrime p, as all we know is p : Ideal R, and we cannot determine that p is prime even though this is evident from p's membership in the set of minimal primes.

I have tried to remedy this with typeclass instances, such as

instance minimalPrimes_isPrime (I p : Ideal R) {h : p ∈ I.minimalPrimes} : p.IsPrime := sorry

but this does not work (in fact, I see h : p ∈ I.minimalPrimes nowhere in the environment when using ∀ p ∈ I.minimalPrimes notation).

Is there any way to make typeclass search work well with mem notation? and use facts about membership to synthesize instances? Or should I rethink the definition of minimalPrimes in Mathlib to instead return an entirely different type that encodes primality more explicitly (such as Set PrimeSpectrum).

[Kevin Buzzard]

import Mathlib

variable {R : Type _} [CommRing R] (I : Ideal R)
protected noncomputable def Ideal.height  [h : IsPrime I] : WithBot ℕ∞ :=
  ⟨I, h⟩ |> height (PrimeSpectrum R)

open Ideal

theorem minimal_primes_height_1_of_principal (x : R) :
    ∀ p ∈ (Ideal.span {x}).minimalPrimes,
    haveI : IsPrime p := sorry
    p.height = 1 := sorry

[Calvin Lee]

right, so i can technically make it work with

theorem minimal_primes_height_1_of_principal (x : R) :
    ∀ (p : Ideal R) (h : p ∈ (Ideal.span {x}).minimalPrimes), (@Ideal.height _ _ p (@minimalPrimes_isPrime _ _ _ p h)) = 1 := sorry

using my instance from before, but this is horrible

[Kevin Buzzard]

Right, and I'm suggesting that my version is less horrible

[Kevin Buzzard]

Your instance will never fire unless explicitly invoked because typeclass inference can't find h.

[Calvin Lee]

I agree that yours is better, but it's still a bit of work whenever you need to show that an element of the set of minimalPrimes is prime (which seems rather common to me)
Maybe it would be better to change Ideal.minimalPrimes to have type Set (PrimeSpectrum R) with better coe from PrimeSpectrum to Ideal, since that type contains a witness of primality in a much more straightforward way

[Eric Rodriguez]

Kevin Buzzard said:

import Mathlib

variable {R : Type _} [CommRing R] (I : Ideal R)
protected noncomputable def Ideal.height  [h : IsPrime I] : WithBot ℕ∞ :=
  ⟨I, h⟩ |> height (PrimeSpectrum R)

open Ideal

theorem minimal_primes_height_1_of_principal (x : R) :
    ∀ p ∈ (Ideal.span {x}).minimalPrimes,
    haveI : IsPrime p := sorry
    p.height = 1 := sorry

why are we using haveI here?

[Eric Wieser]

haveI prevents a let appearing in the theorem statement

[Kevin Buzzard]

@Calvin Lee if you want to take on that refactor of docs#Ideal.minimalPrimes (which would probably then need renaming to PrimeSpectrum.minimalPrimes) then my guess is that there won't be too many objections. I am not too upset about the version I proposed with the haveI but perhaps I'm just used to this sort of thing occasionally occuring in theorem statements.