zero locus of an ideal

Stream: new members

[Aniruddh Agarwal]

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]

try zero_locus (I : set R)

[Aniruddh Agarwal]

That did it!

[Aniruddh Agarwal]

Does the notation set R mean subset of R?

[Johan Commelin]

If you are a mathematician: yes

[Johan Commelin]

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

[Johan Commelin]

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]

All elements of a set must have the same type.

[Johan Commelin]

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

[Patrick Massot]

@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]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

He meant "primitive" = "less nice"