# Zulip Chat Archive

## Stream: general

### Topic: coercion from prime ideals to ideals?

#### Kevin Buzzard (Dec 30 2021 at 14:44):

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 (Dec 30 2021 at 14:51):

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 (Dec 30 2021 at 15:03):

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"

Last updated: Aug 03 2023 at 10:10 UTC