Zulip Chat Archive

Stream: new members

Topic: zero locus of an ideal


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 24 2020 at 07:07):

try zero_locus (I : set R)

view this post on Zulip Aniruddh Agarwal (Apr 24 2020 at 07:10):

That did it!

view this post on Zulip Aniruddh Agarwal (Apr 24 2020 at 07:15):

Does the notation set R mean subset of R?

view this post on Zulip Johan Commelin (Apr 24 2020 at 07:15):

If you are a mathematician: yes

view this post on Zulip Johan Commelin (Apr 24 2020 at 07:16):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 24 2020 at 07:17):

All elements of a set must have the same type.

view this post on Zulip Johan Commelin (Apr 24 2020 at 07:17):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 24 2020 at 13:06):

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

view this post on Zulip Patrick Massot (Apr 24 2020 at 13:07):

He meant "primitive" = "less nice"


Last updated: May 13 2021 at 23:16 UTC