Zulip Chat Archive

Stream: new members

Topic: subtypes and stuff


view this post on Zulip Jon Eugster (Feb 23 2021 at 17:36):

I have two conceptual questions. I'll ask them together because I think the answers might be related and are generally about automated type conversion/coercion etc..

1) In my little project I often work with (p: prime_spectrum A) (prime_spectrum is defined as def prime_spectrum := {I : ideal R // I.is_prime} so I think it is a subtype, right?) so whenever I want to use a fact about ideals I have to enter p.val instead of p, is there a general way in Lean to lift all properties to a subtype? For example, I defined

-- Lifting the partial order of ideals to a partial order on prime ideals.
instance has_le_prime_spec {A: Type*} [comm_ring A]: has_le (prime_spectrum A) :=
  λp q, p.val  q.val

which I was wondering if there was an approach to not do that manually?

2) I made the following two definitions.

def is_integrally_closed (A: Type*) [integral_domain A]:=
  integral_closure A (fraction_ring A) = 

def loc (A: Type*) [comm_ring A] (p: prime_spectrum A) :=
  localization (p.val).prime_compl

The first one takes an integral domain, the second one defines a localisation at a prime ideal.
Now the latter should be an integral domain and thus I would want to be able to do is_integrally_closed (loc A p) but this doesn't type check as Lean doesn't know it is a integral domain (I think localization returns a quotient type, not sure what that is).

What is the structure of lemma I would need to prove and how do I make Lean automatically find it?

Thank you for the help and sorry for the long question!

view this post on Zulip Johan Commelin (Feb 23 2021 at 17:38):

@Jon Eugster The order on prime_spectrum was added to mathlib last week. Do you have the latest version?

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:38):

no

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:38):

good call

view this post on Zulip Johan Commelin (Feb 23 2021 at 17:39):

Also, it is recommended to write x.as_ideal instead of x.val. For x.as_ideal there are special lemmas and instances that for example automatically add the fact that it is a prime ideal to the typeclass system.

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:41):

do I just run leanproject upgrade-mathlib or is there more to it?

view this post on Zulip Johan Commelin (Feb 23 2021 at 17:42):

that should do it, are you working in a project that depends on mathlib?

view this post on Zulip Johan Commelin (Feb 23 2021 at 17:42):

Or on mathlib itself?

view this post on Zulip Johan Commelin (Feb 23 2021 at 17:42):

Note that is_integrally_closed is also already in mathlib, I think.

view this post on Zulip Johan Commelin (Feb 23 2021 at 17:42):

And schemes are there, so the stuff about localizations must probably be there as well in one form or another.

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:42):

nvm worked. after restarting VS

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:44):

I'll look again. But the conceptual questions would still be useful, assuming stuff wasn't already in the mathlib

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:44):

especially (2)

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:45):

would it be like

lemma loc_of_integral_domain {A: Type*} [integral_domain A] (p: prime_spectrum A):
  integral_domain (loc A p) :=
begin
  sorry
end

view this post on Zulip Jon Eugster (Feb 23 2021 at 17:46):

(I think I missed something here that was mentioned somewhere in a tutorial)

view this post on Zulip Jon Eugster (Feb 23 2021 at 18:01):

Johan Commelin said:

Or on mathlib itself?

a project that depends on mathlib. Don't feel comfortable enough with lean yet to contribute to mathlib. (but I have a notion of a regular local ring in terms of Krull dimension, so they might eventually be of interest if I learn enough how to write a nice API around stuff )

view this post on Zulip Johan Commelin (Feb 23 2021 at 18:07):

so, if you have a project that depends on mathlib, then yes leanproject up will do the job, and you don't have to worry about your commits on master fighting with mathlib master.

view this post on Zulip Johan Commelin (Feb 23 2021 at 18:08):

also... if you already have Krull dimension and regular local ring and you are potentially interested in contributing to mathlib, then I suggest you start with some small PRs

view this post on Zulip Johan Commelin (Feb 23 2021 at 18:09):

It doesn't make sense to write 3500 lines of code, and discover that you need to rewrite all of it because mathlib wants the basics to be a bit different or more general etc...

view this post on Zulip Johan Commelin (Feb 23 2021 at 18:09):

once you have 500 lines of code, look for 100 self-contained lines (e.g. basics of Krull dimension) and PR them

view this post on Zulip Jon Eugster (Feb 23 2021 at 18:29):

good call. I mean I have a definition of both, but basically no facts about them, so it's not really helpful (yet).


Last updated: May 11 2021 at 00:31 UTC