Bundled basis

Stream: general

[Anne Baanen]

I recently did another refactoring experiment: what happens if we turn {b : ι → M} (hb : is_basis R b) into a bundled type (b : basis ι R M)?

Some observations:

• The code got a bit longer overall because I proved more, smaller, lemmas. I feel that the overall complexity is lower.
• Many parts of the code use the obtain \<b, hb\> := exists_is_basis K V idiom. Even if we don't do the bundled basis refactor, we should still turn these b and hb into their own (noncomputable) definitions to save some lines.
• I really need to learn advanced applications of simps, since it should save quite a bit of trivial lemma declaration.
• I didn't encounter any hard-to-fix breakages: basically everything was changing is_basis into basis and some renames.
• With some tricks, both the coercion to a function b : ι → M and the coordinate function b.repr : M → ι →₀ R can be computable, which makes me happy as an intuitionist. (Actually the data stored in an element of basis ι R M is the repr function. This should not change the API, we still have a (now noncomputable) basis.mk which takes a linear independent family spanning the whole space and turns it into a basis.)

[Anne Baanen]

(This refactor has been on my TODO list ever since #4949).

[Johan Commelin]

Sounds good!

[David Wärn]

Is there any particular reason not to bundle \iota?

[Eric Wieser]

Would there be any advantage to doing so?

[Anne Baanen]

Whether to bundle the ι is a good question! I suspect that bundling it may cause universe trouble (what if ι ; Type 2 and K V : Type 1?), and it may lead to more awkward definitions for maps "out of" bases. But for maps "into" bases, like docs#exists_is_basis currently, it might give cleaner results.

[David Wärn]

If you bundle ι, and give it a third universe level, separate from M and R,, won't that give the same universe behaviour as the unbundled definition? That is, whenever you stipulate variable b : basis M R, you're introducing a new universe variable, just like with variables (ι : Type*) (basis ι R M). If you put the universe variable of ι first, you'll also be able to pin it down by saying b : basis.{u} M R

[David Wärn]

Eric Wieser said:

Would there be any advantage to doing so?

I don't know (I've never done linear algebra in mathlib). But certainly "let b be a basis" is more concise than saying "let ι be a type and let b be an ι-indexed basis". I would say that it also aligns better with mathematical practice, but when I think about it that's probably false: usually people mention ι (or n) when they stipulate a basis

[Kevin Buzzard]

When people are doing finite-dimensional spaces they often have an index type but when they're doing infinite-dimensional spaces they often treat them as subsets

[Kevin Buzzard]

This is because a lot of the finite-dimensional theory relies on computations with matrices but the infinite-dimensional theory is usually just doing stuff like free modules are projective

[David Wärn]

But you might still say something like "let $\{e_i\}_{i \in I}$ be a basis", right?

[Kevin Buzzard]

Sure you can say it, but for example in the proof that bases of vector spaces exist you just consider linearly subsets ordered by inclusion and take a maximal element

[Kevin Buzzard]

The index set gets in the way there

[Anne Baanen]

David Wärn said:

If you bundle ι, and give it a third universe level, separate from M and R,, won't that give the same universe behaviour as the unbundled definition? That is, whenever you stipulate variable b : basis M R, you're introducing a new universe variable, just like with variables (ι : Type*) (basis ι R M). If you put the universe variable of ι first, you'll also be able to pin it down by saying b : basis.{u} M R

I don't have a good intuition how often you need to specify the universe variable: if this is all the time, then I'd rather have the index variable. Maybe someone with more experience in the category theory areas can comment (@Scott Morrison?).

[Eric Wieser]

If you bundle iota, then to talk about bases over the same index you have to start inserting proofs that the indexes are the same

[Eric Wieser]

(deleted)

[Yury G. Kudryashov]

I think that this is a good reason not to bundle ι.

[Mario Carneiro]

Yes, it's generally not a good idea to bundle types for the reason Eric Wieser mentioned

[Eric Wieser]

This came up recently for @David Wärn and I in the definition of docs#is_free_group, where the type generators is bundled

[Eric Wieser]

Do you think it shouldn't be, @Mario Carneiro?

[Mario Carneiro]

I think that it should be bundled

[Mario Carneiro]

not the index type, but the basis itself, like Anne implemented

[Eric Wieser]

I'm not sure you're answering the question I asked

[Mario Carneiro]

Maybe I don't know what the question is

[Mario Carneiro]

is_free_group bundles the type, and I don't think this is a good idea for the same reasons

[Eric Wieser]

Ok, that's the question I was asking, thanks!

[Mario Carneiro]

Not to mention it's often useful to say that a type is freely generated by n elements, rather than just free on some set

[Mario Carneiro]

In fact it might even be useful to pull the generators out of the structure too, have a function f : I -> G as a parameter to is_free_group

[Anne Baanen]

It took a lot of spare hours over the course of a couple of weeks, but the bundled basis refactor PR is here! #7496