naming: finrank and rank lemmas

Stream: general

[Eric Wieser]

For the dimension (docs#module.rank) of a product space (over modules satisfying docs#module.free) we have docs#dim_prod.

For the finite dimension (docs#finite_dimensional.finrank) of a product space (over modules additionally satisfying docs#module.finite), we have... docs#module.free.finrank_prod, which is in neither namespace!

[Eric Wieser]

What names should we pick up clean this up?

[Eric Wieser]

I'm aware that dim was the old name of module.rank, and that changing the name is annoying

[Eric Wieser]

But even ignoring that, it would be good to pick a namespace to put the finrank lemmas in

[Eric Wieser]

/poll Where do the finrank lemmas belong?

• In the finite_dimensional namespace
• In the module.free namespace
• In the module.finite namespace
• In the namespace of the type they are describing the dimension of

[Eric Wieser]

Kevin Buzzard said:

A couple of years ago I did a twitch livestream where I formalised an example sheet question (if $A$,$B$ are two 5-dimensional subspaces of a 9-dimensional vector space then $A\cap B\not=0$). I just tried this again and noticed a couple of things; firstly [...] and secondly (perhaps when findim got refactored to finrank?) namespaces are all over the place. If you import linear_algebra.finite_dimensional then you get finite_dimensional.finrank (the nat-valued dimension of a f.d. vector space) and then lemmas like finrank_bot (in the root namespace) and also lemmas like submodule.finrank_le (in the submodule namespace).

[...] I don't quite know whether all this inconsistency is somehow expected (i.e. it's a consequence of our conventions) or whether everything should just be in the finite_dimensional namespace really.

Note also that dim_sup_add_dim_inf_eq is a statement about module.rank but submodule.dim_sup_add_dim_inf_eq is a statement about finranks. Should we expect the naming convention (whatever it is) to do better here? Why are either of these things called dim anyway if the convention now is to call things rank or finrank? Is this just an oversight?

[Eric Wieser]

cc @Riccardo Brasca, since you put some of these lemmas in the module.free namespace

[Riccardo Brasca]

Sorry for that, I think that all results involving any notion of dimension should not live in the module.free namespace (since it's clear that they hold for free modules).

[Eric Wieser]

No worries, lots of these things make sense at the time then seem silly after 6 months of extra refactors elsewhere have landed

[Eric Wieser]

#18733 does the easy rename from module.free to finite_dimensional, we can revisit the fourth option in the poll another time.

[Eric Wieser]

I suspect there's a lot of overlap between file#linear_algebra/finrank, file#linear_algebra/free_module/finite/rank, and file#linear_algebra/finite_dimensional (which import each other in a chain with finite_dimensional as the leaf)

[Riccardo Brasca]

Yes, my plan was to clean this up at some point. Everything should be done for module.free, but because of the import structure the easiest thing was to duplicate stuff and then start cleaning. I guess that now it's possible to deduplicate.

[Eric Wieser]

On a similar note to the above; what should docs#module.free.rank_finsupp' and docs#finsupp.dim_eq be merged to?

[Eric Wieser]

dim_finsupp in the root namespace? Or module.rank_finsupp?

[Anne Baanen]

I would certainly prefer rank over dim in any new lemmas, since dim doesn't exist anymore.

[Riccardo Brasca]

Maybe it's time to do this properly, before the tide arrives. I think there should be only one file between linear_algebra.dimension and linear_algebra.free_module.rank, and similarly for finrank.

[Eric Wieser]

My current plan was to generalize everything in finrank first, then merge the files once the lemmas are less likely to complain about being relocated

[Riccardo Brasca]

BTW docs#finsupp.dim_eq is more general than docs#module.free.rank_finsupp', so we should keep it.

[Eric Wieser]

Anne Baanen said:

I would certainly prefer rank over dim in any new lemmas, since dim doesn't exist anymore.

docs#rank already exists though and is something else! (fixed in #18734)

[Riccardo Brasca]

Why not linear_map.rank? Writing f.rank seems reasonable.

[Eric Wieser]

That's what I renamed it to :)

[Eric Wieser]

Anne Baanen said:

I would certainly prefer rank over dim in any new lemmas, since dim doesn't exist anymore.

I've started renaming them in #18735

[Eric Wieser]

Riccardo Brasca said:

Why not linear_map.rank? Writing f.rank seems reasonable.

I've just realized I made this same suggestion over a year ago

[Eric Wieser]

Eric Wieser said:

I've started renaming them in #18735

Apparently I caught all of them in my first try, this is now green

[Eric Wieser]

Bors seems to be confused about this PR

[Eric Wieser]

Riccardo Brasca said:

BTW docs#finsupp.dim_eq is more general than docs#module.free.rank_finsupp', so we should keep it.

I've tidied up the names of these in #18743

[Eric Wieser]

Kevin Buzzard said:

Note also that dim_sup_add_dim_inf_eq is a statement about module.rank but submodule.dim_sup_add_dim_inf_eq is a statement about finranks. Should we expect the naming convention (whatever it is) to do better here? Why are either of these things called dim anyway if the convention now is to call things rank or finrank? Is this just an oversight?

This is fixed in #18747

[Kevin Buzzard]

Thank you!

[Eric Wieser]

Eric Wieser said:

My current plan was to generalize everything in finrank first, then merge the files once the lemmas are less likely to complain about being relocated

Up next, #18716

[Riccardo Brasca]

I will have a look in about one hour and half.

[Eric Wieser]

Thanks!

[Eric Wieser]

#18748 is I think my final PR in this direction; I'll pass the baton to someone else for any future rounds of cleanup

[Jeremy Tan]

What's the status of this refactor?

[Eric Wieser]

Why, has port-status#linear_algebra/dimension met the tide?

[Jeremy Tan]

Yes, it has no unported dependencies

[Eric Wieser]

I've just noticed I made a mess of the docstring when doing some of the refactor above; I'll make a quick PR from mobile

[Eric Wieser]

#18759

[Riccardo Brasca]

I am merging the two remaining PRs.

[Eric Wieser]

There's now another one, #18770. It turns out that we had a proof that the space of linear maps is finite dimensional in three places. This tidies up the import graph in a way that port-status#linear_algebra/dimension should become lower priority; it's no longer needed for port-status#linear_algebra/matrix/to_lin

[Scott Morrison]

Okay, with these all merged, I'm going to declare that linear_algebra.dimension has now got its feet wet. No more refactors please on the mathlib3 file, and whenever mathport is ready (already?) someone can try to port it. :-)

[Jeremy Tan]

Scott Morrison said:

No more refactors please on the mathlib3 file, and whenever mathport is ready (already?) someone can try to port it. :-)

there's still the forwardports: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/!4.233247

[Eric Wieser]

I had a look through the file this morning and concluded there was no remaining low-hanging refactor-fruit; so do not intend to make more PRs to it.

[Scott Morrison]

The forward ports are now all in the merge queue. When mathport next runs, someone can have a go at linear_algebra.dimension. :-)

[Jeremy Tan]

Scott Morrison said:

The forward ports are now all in the merge queue. When mathport next runs, someone can have a go at linear_algebra.dimension. :-)

mathport has already included the latest changes to LinearAlgebra.Dimension.

!4#3354 is the mathlib4 port; I haven't done comment renaming yet, and there is a universe problem at cardinal_le_rank_of_linearIndependent I don't know how to solve

[Jeremy Tan]

OK, done the comment naming