# Zulip Chat Archive

## Stream: new members

### Topic: zero locus of an ideal

#### Aniruddh Agarwal (Apr 24 2020 at 07:01):

I'm trying to prove the following lemma:

lemma radical_vanishing_ideal_zero_locus (I : ideal R) : vanishing_ideal (zero_locus I) = ideal.radical I := sorry

but lean is giving me a type error at `zero_locus`

:

type mismatch at application zero_locus I term I has type ideal R : Type u but is expected to have type set ?m_1 : Type ?

This is puzzling to me because `zero_locus I`

for an ideal `I`

seems to type check when used in `prime_spectrum.lean`

in mathlib

#### Mario Carneiro (Apr 24 2020 at 07:07):

try `zero_locus (I : set R)`

#### Aniruddh Agarwal (Apr 24 2020 at 07:10):

That did it!

#### Aniruddh Agarwal (Apr 24 2020 at 07:15):

Does the notation `set R`

mean subset of `R`

?

#### Johan Commelin (Apr 24 2020 at 07:15):

If you are a mathematician: yes

#### Johan Commelin (Apr 24 2020 at 07:16):

Alternatively, read it as "a set whose elements are all of type `R`

"

#### Johan Commelin (Apr 24 2020 at 07:16):

In Lean you cannot (at least you don't want to!) have a set containing a natural number, a list of reals, a group, and a metric space.

#### Johan Commelin (Apr 24 2020 at 07:17):

All elements of a set must have the same type.

#### Johan Commelin (Apr 24 2020 at 07:17):

So you may also think of them as "subsets of the ambient space"

#### Patrick Massot (Apr 24 2020 at 12:52):

@Aniruddh Agarwal Let me emphasize that the "alternative" reading "a set whose elements are all of type `R`

" is the correct one, and you should really try to get used to it.

#### Kevin Buzzard (Apr 24 2020 at 13:03):

Johan Commelin said:

In Lean you cannot (at least you don't want to!) have a set containing a natural number, a list of reals, a group, and a metric space.

If you want to package such data together in Lean, you would use a type (a structure). Sets are more primitive than types, in Lean, because they can only have elements of one type.

#### Mario Carneiro (Apr 24 2020 at 13:06):

I think this is the wrong wording; types are of course more primitive than sets in *type* theory

#### Mario Carneiro (Apr 24 2020 at 13:06):

I think you mean to say that sets are less flexible than types in lean

#### Patrick Massot (Apr 24 2020 at 13:07):

He meant "primitive" = "less nice"

Last updated: May 13 2021 at 23:16 UTC