LinearMap.stdBasis

Stream: mathlib4

[Patrick Massot]

Still trying to explain linear algebra, I have to face the canonical basis mess. Part of this mess comes from infinite dimensional vector spaces. I think there is not much we can do about the parallel existence of docs#Finsupp.basisSingleOne
and docs#Pi.basisFun since in general functions and finitely supported functions are different types (but those two declarations could have more similar names and cross reference each others in their docstrings). However there is also docs#LinearMap.stdBasis whose name is infinitely more discoverable than the other two but simply has nothing to do with docs#Basis (which should probably be in the Module namespace by the way).

Does anyone has comments about this before I try to open a PR? A suggestion for a better name for docs#LinearMap.stdBasis would be fantastic.

[Eric Wieser]

We could just delete LinearMap.stdBasis, as it's already just a synonym for docs#LinearMap.single

[Eric Wieser]

Maybe the naming there isn't ideal either, but it's at least used consistently with docs#AddMonoidHom.single etc

[Patrick Massot]

Grepping suggests this is used a lot in Mathlib, so it won’t be fun, but it seems very reasonable (and gets rid of the super confusing name).

[Eric Wieser]

I wasn't brave enough to remove stdBasis when I cleaned up all the other single API in mathlib 3, so good luck!

[Eric Wieser]

I guess we now have deprecations, which we didn't at the time.

[Patrick Massot]

The painful part is that the duplicated declaration have (again) different implicit arguments.

[Eric Wieser]

They also have different simp-normal forms I think

[Patrick Massot]

How far is lake exe refactor from allowing to change a binder type? I want lake exe refactor "make φ explicit in LinearMap.single".

[Patrick Massot]

I am not yet familiar with large scale uses of deprecated. What should I do with the statements all the duplicated lemmas. You I restate them in terms of the new definition or silence the deprecated linter and keep their old statements?

[Eric Wieser]

I think the idea is to make the change that doesn't break existing downstream code; so silence the linter and keep their old statements, applying @[deprecated] to those too

[Patrick Massot]

Let me check I understand before modifying hundreds of lines. Should the new beginning of the stdBasis file be

/-- The standard basis of the product of `φ`. -/
@[deprecated LinearMap.single (since := "08/09/2024")]
def stdBasis : ∀ i : ι, φ i →ₗ[R] ∀ i, φ i :=
  single R φ

set_option linter.deprecated false in
@[deprecated LinearMap.single_apply (since := "08/09/2024")]
theorem stdBasis_apply (i : ι) (b : φ i) : stdBasis R φ i b = update (0 : (a : ι) → φ a) i b :=
  rfl

set_option linter.deprecated false in
@[simp, deprecated LinearMap.single_apply' (since := "08/09/2024")]
theorem stdBasis_apply' (i i' : ι) : (stdBasis R (fun _x : ι => R) i) 1 i' = ite (i = i') 1 0 := by
  rw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply]
  congr 1; rw [eq_iff_iff, eq_comm]

[Eric Wieser]

The date format should be "2024-08-09", but otherwise that looks right to me

[Eric Wieser]

(I didn't think a year in the US would be enough for you to switch to their date format!)

[Patrick Massot]

I tried switching, I put the month before the day!

[Eric Wieser]

Some of these lemmas might not be worth copying across to LinearMap.single at all; you could argue that the API should only be about unfolding to Pi.single, and let the Pi.single lemmas take it from there.

[Patrick Massot]

What should I do with lemmas that I don’t copy?

[Eric Wieser]

stdBasis_apply'could have @[deprecated "use `LinearMap.single_apply` then `Pi.single_apply` instead"] or similar

[Patrick Massot]

And do you agree that I should make R and φ explicit in docs#LinearMap.single ?

[Eric Wieser]

That sounds reasonable to me

[Eric Wieser]

It matches docs#MonoidHom.single

[Patrick Massot]

It also matches stdBasis…

[Patrick Massot]

I opened #15660, but I’m not yet sure it will pass CI.

[Patrick Massot]

@Eric Wieser #15660 is now ready for review (and touches 21 files).

[Eric Wieser]

I left a few comments, all on the same idea

[Patrick Massot]

Note that I didn’t introduce any lemma in this PR, so everything that you find strange was already strange (but this is not an argument to keep it).

[Patrick Massot]

I am not super convinced that every lemma should be a simp lemma. The changes that you suggest would make rewriting with rw impossible.

[Patrick Massot]

I mean the changes where LinearMap.single appear in LHS.

[Patrick Massot]

That being said I don’t have any strong feeling here (except of course the feeling that stdBasis is a horribly confusing name).

[Eric Wieser]

Patrick Massot said:

(but this is not an argument to keep it).

I suppose it might be an argument to declare it out of scope for your PR

[Eric Wieser]

The changes that you suggest would make rewriting with rw impossible.

it would just mean to have to start by rewriting with LinearMap.coe_single

[Patrick Massot]

That’s true.

[Eric Wieser]

But I suspect that most of the proofs that would need to do that would no longer need to if their statement was also changed to use Pi.single

[Patrick Massot]

Maybe I should simply try to implement those suggestions and see how they affect existing proofs.

[Patrick Massot]

I am a bit tired of this PR, but this is useful maintenance work.

[Patrick Massot]

I pushed a commit with those suggestions, we’ll see how CI likes it.

[Eric Wieser]

I pushed a few more

[Eric Wieser]

CI will surely be unhappy, but I think the fixes downstream will be trivial

[Patrick Massot]

Eric, are you still working on this or should I continue this effort?

[Eric Wieser]

Sorry, was offline for a bit. Feel free to push as needed to fix CI issues if I don't get there first

[Eric Wieser]

Could you cleanup the docstring in StdBasis.lean to reflect what you want to write about in MIL?

[Patrick Massot]

In the mean time I got required by my family. I am not sure when I'll be available again.

[Eric Wieser]

Nevermind, I just pushed the removal of stdBasis from the docstring

[Eric Wieser]

I think this is probably ready to go now, but you should look over the changes I pushed

[Patrick Massot]

Great! Thanks for all your help!

[Eric Wieser]

Will docs#Matrix.stdBasisMatrix be next to fall?

[Patrick Massot]

That one is much less surprising.

[Eric Wieser]

#15693 has a small related cleanup

[Eric Wieser]

(it had a TODO suggesting we reintroduce stdBasis as std_basis_vec!)