invalid import

Stream: new members

[Damiano Testa]

Dear All,

I am trying to

import ring_theory.polynomial.basic

but I get the error message

file 'ring_theory/polynomial/basic' not found in the LEAN_PATH

invalid import: ring_theory.polynomial.basic
could not resolve import: ring_theory.polynomial.basic

I can see that the file is in the subfolder of ring_theory called polynomial, I can import without problems other files in ring_theory, for instance localization. Is there a way of getting Lean to import the files in sub-sub-sub-...-folders?

Thank you!

[Kevin Buzzard]

This is a really common question. Isn't there some link mentioned in the error message which you can click on which suggests some solutions?

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

Oh wait -- you can import other ring theory stuff?

[Damiano Testa]

yes, I can, although not everything.

[Kevin Buzzard]

Are you happy working in the command line?

[Damiano Testa]

The error message has no link

[Damiano Testa]

I have a command line... I am happy to use it!

[Kevin Buzzard]

Are you working in mathlib or in another project which uses mathlib as a dependency?

[Damiano Testa]

I am working in lean-scheme

[Kevin Buzzard]

That's a really old repo

[Damiano Testa]

(I hope that this answers your question!)

[Kevin Buzzard]

It hasn't been updated for months

[Damiano Testa]

Ok, I have not used much from it yet, so I am happy to use a different one

[Kevin Buzzard]

Are you sure it contains something called data.polynomial.basic?

[Kevin Buzzard]

IIRC it was just called data.polynomial in those days

[Damiano Testa]

"it" meaning mathlib?

[Kevin Buzzard]

Can you say more about this claim that you can see the file in the subfolder of ring_theory called polynomial?

[Kevin Buzzard]

Which file exactly can you see?

[Kevin Buzzard]

Are you looking in the version of mathlib used by the project? That version us stored in _target

[Kenny Lau]

@Damiano Testa if you press Ctrl+Space when you put your cursor after ring_theory you can see all the files with that name

[Damiano Testa]

this is what I find when I ls:

$ ls mathlib/src/ring_theory/polynomial
basic.lean basic.olean default.lean default.olean homogeneous.lean homogeneous.olean rational_root.lean rational_root.olean

[Kevin Buzzard]

I challenge your implicit implication that those files are what your project is importing

[Damiano Testa]

maybe this is clearer

$ ls -o mathlib/src/ring_theory/polynomial
total 376
-rw-rw-r-- 1 damiano 23172 Aug 21 10:00 basic.lean
-rw-r--r-- 1 damiano 189780 Aug 21 10:01 basic.olean
-rw-r--r-- 1 damiano 36 Jul 24 15:04 default.lean
-rw-r--r-- 1 damiano 2525 Aug 21 10:01 default.olean
-rw-rw-r-- 1 damiano 9466 Aug 21 10:00 homogeneous.lean
-rw-r--r-- 1 damiano 70425 Aug 21 10:01 homogeneous.olean
-rw-rw-r-- 1 damiano 9555 Aug 21 10:00 rational_root.lean
-rw-r--r-- 1 damiano 61000 Aug 21 10:01 rational_root.olean

[Kevin Buzzard]

Which directory are you looking in?

[Kevin Buzzard]

I have literally 50 copies of mathlib on my computer

[Damiano Testa]

mathlib/src/ring_theory/polynomial

[Kevin Buzzard]

What do you mean by mathlib?

[Damiano Testa]

I think that I only have one mathlib

[Kenny Lau]

@Damiano Testa you need to look inside _target

[Kenny Lau]

inside lean-scheme

[Kevin Buzzard]

You're looking at the wrong mathlib

[Kevin Buzzard]

Each project comes with its own mathlib

[Damiano Testa]

so how do I choose which mathlib to use?

[Kevin Buzzard]

Inside the lean-scheme folder is the mathlib which lean-scheme uses

[Kevin Buzzard]

You don't choose

[Kenny Lau]

if you "choose" a different version of mathlib to use, the project will break

[Damiano Testa]

is it the one called "to_mathlib"?

[Kenny Lau]

can you ls lean_scheme?

[Kevin Buzzard]

The leanpkg.toml file of the project tells the system which mathlib to use

[Kevin Buzzard]

It's in _target

[Kenny Lau]

I mean ls lean-scheme

[Damiano Testa]

this is what I have in lean-scheme/src

$ ls -o lean-scheme/src/
total 36
drwxrwxr-x 2 damiano 4096 Aug 19 14:36 instances
drwxrwxr-x 3 damiano 4096 Aug 19 14:52 Kenny
-rw-rw-r-- 1 damiano 738 Aug 19 14:18 scheme.lean
-rw-rw-r-- 1 damiano 9943 Aug 19 14:36 scheme.olean
drwxrwxr-x 3 damiano 4096 Aug 21 10:01 sheaves
drwxrwxr-x 2 damiano 4096 Aug 21 10:01 spectrum_of_a_ring
drwxrwxr-x 3 damiano 4096 Aug 21 10:01 to_mathlib

[Kevin Buzzard]

Not src

[Kenny Lau]

can you ls lean-scheme?

[Kevin Buzzard]

It's in _target

[Damiano Testa]

$ ls -o lean-scheme/
total 32
-rw-rw-r-- 1 damiano 11400 Aug 21 08:46 Chevalley.lean
-rw-rw-r-- 1 damiano 54 Aug 19 14:24 leanpkg.path
-rw-rw-r-- 1 damiano 207 Aug 19 14:18 leanpkg.toml
-rw-rw-r-- 1 damiano 3200 Aug 19 14:18 README.md
drwxrwxr-x 7 damiano 4096 Aug 21 10:01 src
drwxrwxr-x 3 damiano 4096 Aug 19 14:24 _target

[Kenny Lau]

there's _target

[Kenny Lau]

at the bottom

[Damiano Testa]

ah, let me look in _target!

[Kevin Buzzard]

If you want to work in that old project then you're stuck with an old mathlib

[Kenny Lau]

(and an old Lean)

[Damiano Testa]

Ahhhhh!!!! found it!

$ ls -o _target/deps/mathlib/
total 48
drwxrwxr-x 2 damiano 4096 Aug 19 14:24 archive
drwxrwxr-x 7 damiano 4096 Aug 19 14:24 docs
-rw-rw-r-- 1 damiano 95 Aug 19 14:24 leanpkg.toml
-rw-rw-r-- 1 damiano 11357 Aug 19 14:24 LICENSE
-rwxrwxr-x 1 damiano 762 Aug 19 14:24 purge_olean.sh
-rw-rw-r-- 1 damiano 2797 Aug 19 14:24 README.md
drwxrwxr-x 2 damiano 4096 Aug 19 14:24 scripts
drwxrwxr-x 22 damiano 4096 Aug 19 14:24 src
drwxrwxr-x 6 damiano 4096 Aug 19 14:24 test
-rw-rw-r-- 1 damiano 540 Aug 19 14:24 travis_long.sh

[Kenny Lau]

there you go

[Damiano Testa]

ok, I did not realize that I had a second version of mathlib, inside lean_scheme

[Kevin Buzzard]

Mathlib is not backwards compatible

[Damiano Testa]

alright, then probably this copy of mathlib does not contain the file that i am trying to import

now i understand the inconsistencies!

I still would like to be able to use the "current" mathlib: I'll look for a way

[Kenny Lau]

Kenny Lau said:

if you "choose" a different version of mathlib to use, the project will break

.

[Kenny Lau]

Kevin Buzzard said:

Mathlib is not backwards compatible

.

[Damiano Testa]

indeed, there is a polynomial.lean file, but no polynomial/ directory

[Damiano Testa]

ok, I will open the current version of mathlib, copy the files that i need and see what breaks and what doesn't, then!

[Kenny Lau]

what's the point

[Damiano Testa]

I would like to use functions in lean-scheme and functions in the current mathlib...

[Damiano Testa]

(I mean, in the same proof!)

[Kenny Lau]

you can't

[Damiano Testa]

i was thinking of copying the text from the files in lean-scheme as a new project in the current mathlib.

[Damiano Testa]

this may be cumbersome, but should work, right?

[Kenny Lau]

no, because mathlib is not backwards compatible

[Kenny Lau]

let's say the old version of mathlib contains a theorem called A

[Damiano Testa]

ok, works modulo fixing the commands that no longer work... not everything will be broken!

[Kenny Lau]

and lean-scheme used the theorem A

[Kenny Lau]

then mathlib changed the name to B

[Kenny Lau]

then it will break

[Kenny Lau]

Damiano Testa said:

ok, works modulo fixing the commands that no longer work... not everything will be broken!

then that's a tedious project

[Damiano Testa]

i understand this, but i do not need much...

[Damiano Testa]

ok, works modulo fixing the commands that no longer work... not everything will be broken!

then that's a tedious project

I agree, but is there a better fix?

[Kenny Lau]

no

[Damiano Testa]

so... here i go! ahahaha

[Damiano Testa]

in fact, it might be quicker to copy the files from the current mathlib into the old project, since those should not be incompatible with something that they have not seen!

[Patrick Massot]

Damiano, I think your are vastly underestimating how much mathlib is backward incompatible.

[Patrick Massot]

Especially stuff around polynomial have been problematic for a long time and changed a lot.

[Patrick Massot]

The proper fix is to fully update mathlib in this project and fixing stuff will take a a lot of time. Or else consider this as a frozen project.

[Damiano Testa]

Ok, so it seems that I am faced with the choice of

1. redefine the Zariski topology,
2. try to import a lemma about monomials in polynomial rings

I will need to see what is harder...

[Johan Commelin]

Does lean-scheme have a Zariski topology that mathlib doesn't have?

[Damiano Testa]

I do not know, where is the Zariski topology in mathlib?

[Patrick Massot]

You should coordinate with Kevin and Kenny to know what needs to be done to incorporate more of that repo into mathlib. But I fear they are waiting for the category theory part of mathlib to become ready for sheaves of modules over a sheaf of rings.

[Johan Commelin]

algebraic_geometry/prime_spectrum

[Damiano Testa]

Patrick Massot said:

You should coordinate with Kevin and Kenny to know what needs to be done to incorporate more of that repo into mathlib. But I fear they are waiting for the category theory part of mathlib to become ready for sheaves of modules over a sheaf of rings.

Ok, I will wait for this!

[Damiano Testa]

Johan Commelin said:

algebraic_geometry/prime_spectrum

... but I will take a look at this, in the meantime!

[Damiano Testa]

thanks!

[Kevin Buzzard]

The problem with lean-scheme is that it develops the theory of sheaves in a different way to three standard mathlib way. We are blocked from continuing the development of schemes until the mathlib version of sheaves has caught up with our version. The problem is that everyone is really busy. The big divergence is in the definition of the sheaf of rings on Spec (A). The definition is technical. First we put a presheaf on the basis of standard affine opens, then we prove it's a sheaf for this basis, then we prove that sheaves on a basis are the same as sheaves on the space

[Kevin Buzzard]

All of this now needs to be redone using the mathlib version of presheaves and sheaves

[Kevin Buzzard]

And this uses category theory

[Kevin Buzzard]

And I'm pretty sure that they're not at the point where we can start doing this

[Scott Morrison]

Surely there is lots of work on schemes that can come to mathlib now, before anyone runs into needing sheaves of modules over a sheaf of rings...

[Damiano Testa]

ok, so i will try to start a project using the algebraic_geometry section of mathlib in the current version of mathlib

for this, should I then type

code mathlib? would this make me work in the current version of mathlib?

[Kevin Buzzard]

We can't even define a scheme I don't think Scott

[Kevin Buzzard]

Damiano just clone mathlib and keep it up to date

[Kevin Buzzard]

You might have lots of mathlibs on your computer as dependencies in other projects but you should only have one mathlib project

[Scott Morrison]

You're saying that checking the sheaf condition on a basis is the blocker?

[Damiano Testa]

ok, so i can

code [anything i want]

and if i import a file it will be from the version of mathlib that i have in my lean directory?

[Kevin Buzzard]

Damiano read how to install projects on the community website

[Scott Morrison]

That's good to know, I'll try to make that happen. I didn't realise anyone was yet waiting on that.

[Kevin Buzzard]

Scott here's the issue

[Kevin Buzzard]

A scheme is a ringed space locally isomorphic to Spec R

[Kevin Buzzard]

The isomorphism takes place in the category of spaces equipped with a presheaf of rings

[Kevin Buzzard]

But putting the presheaf of rings on Spec R is not as easy as it sounds because of non affine opens

[Kevin Buzzard]

In Lean-scheme we put the presheaf on a basis

[Kevin Buzzard]

Then proved it was a sheaf (although sheafifying would also work)

[Kevin Buzzard]

And then proved that sheaves on X were the same as sheaves on a basis

[Kevin Buzzard]

By hand

[Kevin Buzzard]

In our particular case

[Kevin Buzzard]

My understanding is that @Bhavik Mehta has a bunch of this stuff in the topos repo but he also has a thesis to write

[Scott Morrison]

I wish I knew whether we should be doing this with sites. Or just presheaves on opens X.

[Kevin Buzzard]

The construction I sketched needs the concept of sheaf on something more general than opens X

[Kevin Buzzard]

One could make the construction in a completely different way of course

[Kevin Buzzard]

I think Hartshorne does it totally differently

[Scott Morrison]

Are you just saying you want to check the sheaf condition only for covers consisting of opens in the basis?

[Scott Morrison]

That's easy to do in the current setup.

[Kevin Buzzard]

@Damiano Testa IIRC Hartshorne defines the sheaf of rings on Spec R directly by looking at functions on U taking values in some crazy disjoint union of rings

[Kevin Buzzard]

This might be a way to proceed

[Patrick Massot]

I think Harshorne basically defined the stalks first, and then recover the sheaf using "continuous" sections of the stalks;

[Kevin Buzzard]

Scott I'm just saying that the way we did it pre category followed the stacks project approach which needed the concept of a presheaf and sheaf on a basis

[Notification Bot]

This topic was moved by Scott Morrison to #general > status of schemes

[Patrick Massot]

I like the way this forum evolved to the point where schemes belong to "general" rather than "maths".

[Scott Morrison]

Hmm, okay, maybe that was a mistake. :-)

[Kevin Buzzard]

I decided to say nothing :D