## Stream: new members

### Topic: subtypes and stuff

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

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

no

good call

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

#### Jon Eugster (Feb 23 2021 at 17:41):

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

#### Johan Commelin (Feb 23 2021 at 17:42):

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

#### Johan Commelin (Feb 23 2021 at 17:42):

Or on mathlib itself?

#### Johan Commelin (Feb 23 2021 at 17:42):

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

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

#### Jon Eugster (Feb 23 2021 at 17:42):

nvm worked. after restarting VS

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

especially (2)

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


#### Jon Eugster (Feb 23 2021 at 17:46):

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

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

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

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

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

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

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