Localization at minimal prime

Stream: new members

[Dion Leijnse]

Suppose we have a commutative ring $R$ and a minimal prime ideal $\mathfrak{p} \subseteq R$. What is the most efficient way to say that an $R$-algebra $S$ is the localiztion of $R$ at $\mathfrak{p}$? The most natural thing for me to write in Lean is the following:

import Mathlib

example (R S : Type) [CommRing R] [CommRing S] (p : minimalPrimes R) [Algebra R S]
    [IsLocalization.AtPrime S p] : Type := S

However, this gives me a typeclass instance error, it is not able to recognize that p is a prime ideal. I can fix this in the following way:

import Mathlib

example (R S : Type) [CommRing R] [CommRing S] (p : Ideal R) (hp : p ∈ minimalPrimes R) [Algebra R S]
    [@IsLocalization.AtPrime _ _ S _ _ p (Ideal.minimalPrimes_isPrime hp)] : Type := S

However, this second solution is a lot more verbose. Is there a more efficient way of doing this?

[Aaron Liu]

add an instance

[Yiming Fu]

I think you can refer to docs#IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes.

[Dion Leijnse]

Thanks, that works for me!