DVRs

Stream: new members

[Johan Commelin]

map_top' : to_fun 0 = 1 looks wrong...

[Johan Commelin]

You could decide to map 0 to something (I would choose 0, if you don't add infinity to Z). But then you need to exclude it in map_add_leq'.

[Johan Commelin]

@Ashvni Narayanan Where do you get your errors? Could you edit your message, to add a comment in the code saying -- error here?

[Johan Commelin]

max_ideal is not known, because the full name is discrete_valuation_ring.max_ideal.
You could write open discrete_valuation_ring if you want to get access to it.

[Jalex Stark]

when I try to run your code block, I get unknown identifier 'principal_ideal_domain' is there a missing open namespace?

[Johan Commelin]

Alternative: extend local_ring R as well... and then you only need uniq_prime_ideal

[Johan Commelin]

For the other error, my guess is that you need ideal.span ({\pi} : set R)

[Patrick Massot]

variables [discrete_valuation_ring R]
open discrete_valuation_ring
def uniformizers : set R := { π | ideal.span ({π} : set R) = max_ideal }

will probably help

[Patrick Massot]

The ({π} : set R) is a shame, this is Lean 3 elaborator not being smart enough. The rest is on you.

[Patrick Massot]

And you probably want to define a version of max_ideal where R is explicit.

[Patrick Massot]

But that's up to you.

[Johan Commelin]

Well, you don't want it to conflict with local_ring. So you should reuse that.

[Patrick Massot]

Also, could you please edit your first message above to change the topic to something more useful? The whole stream is for noob questions so your simply repeating information instead of having your own cosy little topic.

[Johan Commelin]

@Ashvni Narayanan You need ` (next to the 1 on qwerty keyboards).

[Johan Commelin]

@Ashvni Narayanan Anyway, I should say that it's cool to see you attacking DVRs

[Ashvni Narayanan]

Thank you all! It is now showing me the error

type mismatch at application
  ideal.span {π} = max_ideal
term
  max_ideal
has type
  Π (R : Type ?) [c : discrete_valuation_ring R], ideal R : Type (?+1)
but is expected to have type
  ideal R : Type u

I don't see why this type mismatch occurs, because both are in ideals in R..

[Bryan Gin-ge Chen]

The first type Π (R : Type ?) [c : discrete_valuation_ring R], ideal R : Type (?+1) cannot be unified with the second type ideal R : Type u. Do you see why?

[Bryan Gin-ge Chen]

I suspect max_ideal is missing an argument.

[Ashvni Narayanan]

I am guessing I should explicitly define the type of max_ideal?

[Bryan Gin-ge Chen]

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization

universe u

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=
(max_ideal : ideal R)
(maximal : max_ideal.is_maximal)
(unique_prime_ideal : ∀ M : ideal R, M.is_prime → M = ⊥ ∨ M = max_ideal)

-- this doesn't work for me because `fraction_ring` was removed in a recent commit to mathlib:
-- https://github.com/leanprover-community/mathlib/commit/80ad9edc9a6d6d2971dd044f6079cc770e755020
-- structure discrete_valuation_ring.discrete_valuation (R : Type u) [discrete_valuation_ring R] extends localization.fraction_ring R →* ℤ :=
-- (map_top' : to_fun 0 = 1)
-- (map_add_leq' : ∀ x y, to_fun (x + y) ≤ max (to_fun x) (to_fun y))
variables {R : Type u} [discrete_valuation_ring R]
open discrete_valuation_ring
def uniformizers : set R := { π | ideal.span ({π} : set R) = max_ideal }  -- fixed

[Bryan Gin-ge Chen]

You don't have to give R as a parameter to discrete_valuation_ring.max_ideal. The discrete_valuation_ring structure on R is found via type class inference.

[Ashvni Narayanan]

Sorry, I'm not sure I understand. How do I define max_ideal without saying that it is an ideal of R? Perhaps I misunderstood.

[Kevin Buzzard]

Can you restate the problem, if there is still a problem?

[Ashvni Narayanan]

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

universe u

class discrete_valuation_ring (α : Type u) extends principal_ideal_domain α :=
(max_ideal : ideal α)
(maximal : max_ideal.is_maximal)
(unique_prime_ideal : ∀ M : ideal α, M.is_prime → M = ⊥ ∨ M = max_ideal)

structure discrete_valuation_ring.discrete_valuation (α : Type u) [discrete_valuation_ring α] extends localization.fraction_ring α →* ℤ :=

(map_top' : to_fun 0 = 1)

(map_add_leq' : ∀ x y, to_fun (x + y) ≤ max (to_fun x) (to_fun y))

variables (α : Type u) [discrete_valuation_ring α ]
open discrete_valuation_ring
def uniformizers := { π | ideal.span ({π} :set α ) = max_ideal }

The last line gives me an error :

type mismatch at application
  ideal.span {π} = max_ideal
term
  max_ideal
has type
  Π (α : Type ?) [c : discrete_valuation_ring α], ideal α : Type (?+1)
but is expected to have type
  ideal α : Type u

[Kevin Buzzard]

max_ideal is a function which eats two things, first R and second a proof that R is a DVR, and spits out the max ideal of R. Because R is in round brackets the user has to supply it themselves. Because the DVR parameter is in square brackets, Lean will supply it automatically.

[Kevin Buzzard]

wait, the error is elsewhere

[Kevin Buzzard]

Ashvni can you update your Lean to the current version? I don't get an error with the max_ideal, perhaps because I am a bit more up to date.

[Kevin Buzzard]

leanproject up should do it (then close and open VS Code, it should restore all the files you had open etc)

[Bryan Gin-ge Chen]

(You can also restart Lean without restarting VS Code by hitting ctrl+shift+P and searching for the "Lean: restart" command.)

[Ashvni Narayanan]

Still shows me the same error

[Bryan Gin-ge Chen]

That is strange. What does your leanpkg.toml say?

[Kevin Buzzard]

Did you update Lean and mathlib with leanproject up?

[Ashvni Narayanan]

No, I did Lean : restart. That did not work. Sorry, how do I update Lean using leanproject up?

[Bryan Gin-ge Chen]

leanproject up is a command you need to enter at the command line.

[Bryan Gin-ge Chen]

It should work if you followed the recommended directions at https://leanprover-community.github.io/get_started.html#regular-install

[Kevin Buzzard]

You have to run it in the directory of the project. It's the only trick you have to know about from the command line. It keeps your Lean and mathlib up to date so you have the latest tactics

[Johan Commelin]

As I've said before, I think you should extend local_ring R.

[Kevin Buzzard]

Can we just extend local_ring R and principal_ideal_domain R? That would then be the full definition, right? With old structure command true?

[Kevin Buzzard]

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization

set_option old_structure_cmd true

class discrete_valuation_ring (R : Type*)
  extends principal_ideal_domain R, local_ring R.

[Kevin Buzzard]

wait, that includes fields which are probably not DVRs

[Kevin Buzzard]

class discrete_valuation_ring (R : Type*)
  extends principal_ideal_domain R, local_ring R :=
(non_field : local_ring.nonunits_ideal R ≠ ⊥)

? What should the structure field be called?

[Kevin Buzzard]

There's no local_ring.maximal_ideal?

[Johan Commelin]

I think local_ring.max_ideal should be an alias for nonunits_ideal

[Johan Commelin]

Or the latter should simply be renamed

[Ashvni Narayanan]

I tried to update with leanproject up, says command not found. Also, Lean is taking a really long time to check goals, and is now showing me 1001 errors. Maybe I should just reinstall Lean?

[Johan Commelin]

That shouldn't be necessary

[Johan Commelin]

@Ashvni Narayanan do you have elan installed?

[Bryan Gin-ge Chen]

How did you install Lean? The recommended instructions are at this link: #install

[Ashvni Narayanan]

I installed Lean a while ago, I am quite sure I followed the instructions. I don't think I have installed elan

[Bryan Gin-ge Chen]

The instructions include installing elan as one of the steps (and have for more than a year). Try going through the directions corresponding to the operating system you're using in the link above.

[Johan Commelin]

@Ashvni Narayanan In a terminal, could you run the command which lean?

[Johan Commelin]

If it says something that ends in .elan/bin/lean, then you have elan installed

[Ashvni Narayanan]

Yes, I do have elan installed.

[Kevin Buzzard]

Did you install lean when you did that project with Lambert about six months ago?

[Ashvni Narayanan]

Yes

[Johan Commelin]

If you have elan, then leanproject up should not cause problems

[Kevin Buzzard]

She might not have leanproject

[Kevin Buzzard]

She might have followed the instructions exactly as they were before leanproject appeared

[Johan Commelin]

Aah, I see. @Ashvni Narayanan leanproject is a really useful tool. It will automatically download the latest version of mathlib, with precompiled binaries. So it exactly solves the problem of lean being very slow, and all those errors, etc...

[Ashvni Narayanan]

I see. I will try to install it.

[Ashvni Narayanan]

Installing leanproject didn't work out too well. The Lean checker was taking too long and was showing 1001 errors. So I uninstalled and reinstalled Lean. But the same thing continues. Also, when I try to use leanproject, I get :

[WinError 5] Access is denied: 'C:\\Users\\ashvn\\my_project\\_target\\deps\\mathlib\\.git\\objects\\04\\7707d4b8ad5af2062cd42ae6ea954fa9fdda62'

[Johan Commelin]

@Kenny Lau Didn't you have similar issues at some point?

[Kevin Buzzard]

What do you get if you type leanproject --version?

[Kenny Lau]

@Johan Commelin yeah and then Patrick fixed it

[Ashvni Narayanan]

leanproject, version 0.0.8

[Kevin Buzzard]

@Patrick Massot aargh

[Patrick Massot]

That's a new error, not the same as Kenny's.

[Patrick Massot]

Well, it's sort of the same error: a Windows user

[Kevin Buzzard]

So what's the workaround?

[Patrick Massot]

Installing Linux?

[Kevin Buzzard]

Is there anything which takes up fewer gigabytes of memory?

[Patrick Massot]

Before that maybe try with current leanproject master, since I changed stuff this morning.

[Bryan Gin-ge Chen]

I remember having to delete _target in an old Lean package on my Windows machine when I started using leanproject there. Maybe that will help?

[Patrick Massot]

This is worth trying.

[Patrick Massot]

This morning I was testing video conference with people that I'll interview for a job on Thursday. The first one couldn't hear what I was saying. After twenty minutes trying various stuff, he wrote he was using Windows. Not only he was using Windows, but he wasn't knowing the basics of using Windows. I had to write he should try rebooting his computer. And then it worked.

[Kevin Buzzard]

If only one could prove theorems this way

[Johan Commelin]

Did you ever try it?

[Kevin Buzzard]

I'm not on Windows so I tend not to reboot my computer

[Patrick Massot]

This is the kind of stories that tell me from time to time that nothing changed since I stopped using Windows in 1999.

[Kevin Buzzard]

@Ashvni Narayanan try removing the subdirectory _target from the root directory of your project, and then running leanproject up again

[Ashvni Narayanan]

It is finally working! Turns out my file was in the wrong location. Apologies for the bother!

[Kevin Buzzard]

Next time you want to talk about DVRs, start a chat in #maths because not everyone looks here

[Johan Commelin]

Congrats! It's a real pain, getting the setup right. But now you can finally start doing maths again...

[Ashvni Narayanan]

Thanks for all the help!

[Patrick Massot]

If you understand what you were doing wrong and have suggestions to improve the documentation then we're interested.

[Ashvni Narayanan]

The problem is back :

import ring_theory.localization

gives the error

invalid import: ring_theory.localization
excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold)

Also,

leanproject up

still does not work. This time, this is the error:

[WinError 5] Access is denied: 'C:\\Users\\ashvn\\my_project\\_target\\deps\\mathlib\\.git\\objects\\04\\7707d4b8ad5af2062cd42ae6ea954fa9fdda62'

I am totally clueless now.

[Kevin Buzzard]

Did you try closing VS Code and re-opening?

[Kevin Buzzard]

Sometimes things run out of memory, and restarting can fix it. The leanproject error is a different issue.

[Ashvni Narayanan]

I have restarted it a few times.

[Kevin Buzzard]

Can you send a screenshot? Did you "open folder" and open your project folder (if you just open a file, imports won't work)

[Ashvni Narayanan]

image.png

I restarted and tried again, got a different error.

[Kevin Buzzard]

You don't have any errors there, you have an orange bar.

[Kevin Buzzard]

The error is reporting what happened before you'd finished typing. Your problem is that you don't have a compiled mathlib. Please remove _target, upgrade leanproject and run leanproject up in the root directory of the project. And close VS Code, it's just making your computer hot.

[Yakov Pechersky]

In general, I've found leanproject up breaks my directories. You can try editing your leanpkg.toml to a more recent lean and mathlib dependencies, and then running leanpkg get-cache leanproject get-cache

[Kevin Buzzard]

Don't do this, it's not supported and for a beginner it will make matters worse

[Kevin Buzzard]

An expert can perhaps try this approach

[Bryan Gin-ge Chen]

Also, I think you mean leanproject get-cache, not leanpkg get-cache.

[Kevin Buzzard]

leanproject up shouldn't break anything, and if it's breaking something then rather than working around it you should file an issue. Who knows what Yakov means but we are trying to get a new user with little experience in the command line up and running, and starting to use deprecated commands is, for this user, a step in the wrong direction. I totally appreciate that there are other ways to do this.

[Kevin Buzzard]

@Ashvni Narayanan if on the command line, in the directory called my_project, what happens if you type lean --make DVR.lean? Do you get an error? Does the command succeed, or just sit there doing nothing?

[Ashvni Narayanan]

It does not show an error, I don't know if it is successful, some parsing seems to be happening

[Kevin Buzzard]

I think your problem is that you don't have a compiled Lean. Can you try updating leanproject to 0.0.9?

[Kevin Buzzard]

Just do what you did to install it -- it got updated today.

[Kevin Buzzard]

Then try, in your project, rm -rf _target and then leanproject up again. Do all of these with the command line in root directory of your project folder. You can check to see if the rm command worked by typing ls before and after -- before, ls should show a directory called _target but afterwards it should be gone

[Bryan Gin-ge Chen]

I don't think 0.0.9 has been released yet: https://pypi.org/project/mathlibtools/

[Kevin Buzzard]

Thanks Bryan. In that case, just try removing _target and seeing what happens.

[Kevin Buzzard]

If you get the same error about access is denied, I'll have to leave you in the hands of someone who understands Windows. @Yakov Pechersky can you suggest anything less drastic than editing leanpkg.toml? I really want this to be a last resort because it will be hard to explain

[Yakov Pechersky]

I would remove the entire directory using File Explorer, and start over with a leanproject get ...

[Yakov Pechersky]

and hope it works! What's the leanproject project name that is causing issues? I can try it on my windows machine

[Kevin Buzzard]

ha ha! Ashvni this is certainly another approach! Is the project you're working on on GitHub?

[Kevin Buzzard]

If not, then try leanproject new dvr-project and then copy stuff over. Perhaps this is the simplest solution.

[Kevin Buzzard]

Output should look something like this:

$ leanproject new dvr_project
> mkdir -p dvr_project
> cd dvr_project
> mkdir src
> git init -q
> git checkout -b lean-3.4.2
Switched to a new branch 'lean-3.4.2'
configuring dvr_project 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 290, done.
remote: Counting objects: 100% (290/290), done.
remote: Compressing objects: 100% (214/214), done.
remote: Total 51776 (delta 181), reused 130 (delta 74), pack-reused 51486
Receiving objects: 100% (51776/51776), 22.32 MiB | 1.07 MiB/s, done.
Resolving deltas: 100% (39965/39965), done.
> git checkout --detach 470ccd328e15391cf328e0e006e13a06ff7d7b29    # in directory _target/deps/mathlib
HEAD is now at 470ccd32 chore(scripts): update nolints.txt (#2993)
configuring dvr_project 0.1
mathlib: trying to update _target/deps/mathlib to revision 470ccd328e15391cf328e0e006e13a06ff7d7b29
> git checkout --detach 470ccd328e15391cf328e0e006e13a06ff7d7b29    # in directory _target/deps/mathlib
HEAD is now at 470ccd32 chore(scripts): update nolints.txt (#2993)
Looking for local mathlib oleans
Looking for remote mathlib oleans
Trying to download https://oleanstorage.azureedge.net/mathlib/470ccd328e15391cf328e0e006e13a06ff7d7b29.tar.xz to /home/buzzard/.mathlib/470ccd328e15391cf328e0e006e13a06ff7d7b29.tar.xz
100%|█████████████████████████████████████████████████████████████████████████████████████| 22.5M/22.5M [00:21<00:00, 1.07MiB/s]
Found mathlib oleans at https://oleanstorage.azureedge.net/mathlib/

[Ashvni Narayanan]

I tried removing target, and

leanproject up

worked. Currently, it shows 10 problems instead of 1001, so I assume things are working okay

[Kevin Buzzard]

rofl, working OK is 0 problems :D

[Bryan Gin-ge Chen]

Glad you got things working! I opened an issue: mathlib-tools#55