algebra.category.Module.algebra

Stream: mathlib4

[Lars Ericson]

algebra.category.Module.algebra shows an empty dependency graph.

The code shows an import

import Mathbin.Algebra.Category.Module.Basic

The imported file is marked as a ported file .

However, it is not present in the Mathlib4 github (no Module directory here. When I do a git clone of mathlib4, it is not present.

Question: Should a file marked as Ported be present in Mathlib4 master branch?

[Apurva Nakade]

It has probably been renamed to ModuleCat.Basic

[Eric Wieser]

Lars Ericson said:

The imported file is marked as a ported file .

The page you link to tells you what the new name is at the top of the page

[Eric Wieser]

(it is indeed Mathlib.Algebra.Category.ModuleCat.Basic)

[Lars Ericson]

Thanks @Apurva Nakade and @Eric Wieser, I will look for those renames going forward.

[Lars Ericson]

Does this mean that every file in the Algebrra.Category.Module folder should be in ModuleCat and probably doesn't need to be ported? This would seem to be the case for algebra.category.Module.algebra. which refers to the moved file Module.basic.

I am looking at Unported files in mathlib port status for short unported files with no dependencies. That's why I'm looking at this one, but the move of Module to ModuleCat results in some sort of false positives in the unported file list.

[Eric Wieser]

There should be no false positives in the unported files list

[Eric Wieser]

Which one looks like a false positive?

[Lars Ericson]

@Eric Wieser false positive in the sense that algebra.category.Module.algebra is marked as unported and refers to Algebra.Category.Module.Basic which got moved to Algebra.Category.ModuleCat.Basic but is still present in the porting directory as a file in Module, not ModuleCat. By analogy it makes me wonder if Module.Algebra should really be in ModuleCat.Algebra. I guess that's an incorrect analogy.

[Lars Ericson]

Perhaps the underlying problem is that Lean 3 is a moving target so you can't manually adjust mathlib3port to remove files already ported but ported to a new choice of directory. I.e. I assume you regenerate mathlib3port all the time from the latest Lean 3 source, so you can't adjust the porting directory to reflect folder reorganization in the new version?

[Eric Wieser]

Lars Ericson said:

and refers to Algebra.Category.Module.Basic

Refers in what way?

[Mauricio Collares]

When you say "[it] refers to Algebra.Category.Module.Basic", "it" means the mathport output for algebra.category.Module.algebra, right?

[Lars Ericson]

@Mauricio Collares it means that line 13 of the mathlib3port of Algebra.Category.Module.Algebra is

import Mathbin.Algebra.Category.Module.Basic

but this has been relocated to ModuleCat in math4lib.

[Eric Wieser]

This is not a false positive; the dependencies are truly ported. One of your jobs when porting is to fix renamed imports.