Carve out Algebra, Data and Order sublibraries

[YaelDillies]

The bottom part of mathlib is quite a mess. Algebra, data structures and order theory could be developed separately (at least for a while) but are not. Instead, "horizontal" imports keep happening between what would otherwise be three disjoint trees.

The main sources of trouble are

• Nat and Int, as they are ubiquitous. Their basic properties can be accessed through typeclass-mediated lemmas by importing Data.Nat.Basic and Data.Nat.Order.Basic. However this comes at the cost of importing basic algebra or basic algebraic order theory where unnecessary. Instead, we can use the Nat- and Int-specific lemmas provided by Std.
• Many pure algebraic/order theoretic/data structuresque files import non-pure algebraic/order theoretic/data structuresque files just to prove a few properties of an object defined in the non-pure file. In that case, the import can be reversed so that the pure file has pure imports.
• Misplaced files. Eg Polynomial, Real or Set.Icc are defined under Data. The solution is to simply move them to the correct top-level folder.

The purpose of this issue is to collect the PRs doing at least one of the above:

• 11601

• 11633

• 11653

• 11661

• 11711

• 11715

• 11716

• 11725

• 11729

• 11732

• 11741

• 11750

• 11751

• 11753

• 11765

• 11845

Once all these issues will be fixed, we will be able to create three new Lean libraries Algebra, Data, Order, all still living in the current repository.

After such a split, these sublibraries would form a DAG in terms of dependencies. This adds some constraints to future refactors, as that DAG would essentially become immutable.

The benefits?

• working towards it requires drastically cleaning up the import graph, which currently is full of "horizontal gene transfer".
• the sublibrary DAG being immutable is also helpful: it prevents some dependency regressions!
• even though everything will remain in one repository (this is important to minimise the cost of cross-repository refactors), it will be possible in lake to specify that you only want to depend on a subset of these libraries.

[eric-wieser]

it will be possible in lake to specify that you only want to depend on a subset of these libraries.

I don't understand why this is useful. Already, if you do lake build in your project, it only builds the bits of mathlib that you actually import. You can use lake exe cache in a similar way. So the "unused" bits of mathlib are already not meaningfully "depended" on.