coercion from prime ideals to ideals?

Stream: general

[Kevin Buzzard]

I don't know what makes a good coercion. We have the following type in algebraic_geometry.prime_spectrum.basic:

def prime_spectrum := {I : ideal R // I.is_prime}

Unsurprisingly, given a term v : prime_spectrum R one sometimes wants to look at the underlying ideal v.val. I was expecting there to be a coercion, but in fact there is

abbreviation as_ideal (x : prime_spectrum R) : ideal R := x.val

I think abbreviation is the same as [inline, reducible]. I don't really understand inline and am wondering if this is some kind of way to say "I would be happy if the simp normal form is just v.val but my silly users want to call it something". For example this is a simp lemma:

@[simp] lemma comap_as_ideal (y : prime_spectrum S) :
  (comap f y).as_ideal = ideal.comap f y.as_ideal :=
rfl

Would it be better or worse if there was just a coercion to ideal R and the simp normal form was \u v? It would make statements like this look less clunky.

[Johan Commelin]

I think that I introduced as_ideal to make explicit the transition from the "geometrical" picture to the "algebraic" picture. Points of the spectrum can be denoted x, because they are points. But a prime ideal should be P or I, or something.
Of course this is not a Lean reason, but a linguistic(?) one.

At the same time, writing x.as_ideal helps the elaborator, so it's not only a disambiguating flag for the user/reader, but also for Lean. Since we want Lean to also find an instance of is_prime for these ideals, it helps a lot if TC isn't stuck finding a coercion before looking for is_prime.

My guess is that you would end up writing (x : ideal R) explicitly quite often. And then x.as_ideal is actually shorter in the end.

[Kevin Buzzard]

I really like the "geometry v algebra" distinction :-) I was looking at adeles code and there the non-zero primes of a Dedekind domain don't feel like they have any geometry attached to them, although we use the Zariski topology I guess in the sense of "being integral on an open set containing the generic point"