## 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)

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