subtypes and stuff

Stream: new members

[Jon Eugster]

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]

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

[Jon Eugster]

no

[Jon Eugster]

good call

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Or on mathlib itself?

[Johan Commelin]

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

[Johan Commelin]

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

[Jon Eugster]

nvm worked. after restarting VS

[Jon Eugster]

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

[Jon Eugster]

especially (2)

[Jon Eugster]

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]

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

[Jon Eugster]

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]

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]

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]

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]

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

[Jon Eugster]

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