Generalizing some statements from fields to division rings

Stream: mathlib4

[Sophie Morel]

Hi all, for my projective space/grassmannian project over division rings, I needed the fact that a linear map whose source is a finite-dimensional vector space is automatically continuous. This result is in mathlib for a NontriviallyNormedField that is complete, it's called LinearMap.continuous_of_finiteDimensional. I wanted to have it for a complete nontrivially normed division ring (such as the Hamiltonian quaternions), without assuming that this division ring is finite-dimensional over its center (which is true in my example, but I don't know how far from true it is in general).
This is not in mathlib for not much is needed to have it. I had fun modifying my own local copy of mathlib to make it happen, the result is there:
https://github.com/smorel394/JeCasseTout
I changed 3 files:

• Analysis.Normed.Field.Basic.lean
• Analysis.LocallyConvex.BalancedCoreHull.lean
• Topology.Algebra.Module.FiniteDimension.lean

The biggest changes are in the first one, I defined a NontriviallyNormedDivisionRing class and added a NontriviallyNormedField.toNontriviallyNormedDivisionRing instance. The rest was just replacing some NontriviallyNormedField variables with NontriviallyNormedDivisionRing variables until I got the continuity result I wanted. This is by no means optimal, for example you would want LinearMap.toContinuousLinearMap to work with the weaker assumption, but right now it can't because it defines a 𝕜-linear equivalence and, if 𝕜 is not commutative, the equivalence can only be linear over the center of 𝕜. So we should make 𝕜 into an algebra over a commutative thing and add a scalar tower somewhere. (This would unlock some later results too, and it might be useful for the later parts of my own project, I am not sure yet.)

But before I went too far with this, I wanted to check with the mathlib experts if what I did was stupid/dangerous for some reason that I cannot see. I'm not sure how to summon experts, should I just ping all the authors of the files I modified ?

[Eric Wieser]

So we should make 𝕜 into an algebra over a commutative thing and add a scalar tower somewhere.

I don't think you need a scalar tower, just commuting actions (via SMulCommClass)

[Eric Wieser]

I had fun modifying my own local copy of mathlib to make it happen, the result is there: https://github.com/smorel394/JeCasseTout

It would be a lot easier to give feedback on this if you modified the real mathlib, so that we can see the diff easily!

[Sophie Morel]

Eric Wieser said:

I had fun modifying my own local copy of mathlib to make it happen, the result is there: https://github.com/smorel394/JeCasseTout

It would be a lot easier to give feedback on this if you modified the real mathlib, so that we can see the diff easily!

I would be glad to, I am just not sure what to do. I did modify the files in my local copy of mathlib, so should I just ask git to stop ignoring them and push ?

[Eric Wieser]

It is absolutely fine to push broken code to a mathlib branch, and open a PR tagged WIP; PRs don't have to be polished before you push!

[Eric Wieser]

What do you mean by "your local copy of mathlib"? Are you talking about something in the lake-packages directory? Or are you already working on a different mathlib branch?

[Sophie Morel]

Okay,

Eric Wieser said:

What do you mean by "your local copy of mathlib"? Are you talking about something in the lake-packages directory? Or are you already working on a different mathlib branch?

Yes, my local lacke-packages directory. I haven't actually figured out yet how to push to a mathlib branch (I know that I have been given the necessary permissions).

[Sophie Morel]

I'll figure it out later today, soon I will have to run to catch a train.

[Eric Wieser]

You're not really supposed to modify things in lake-packages, but creating a branch and pushing might work fine anyway

[Sophie Morel]

I just don't know what I was supposed to do ! Obviously I need to go read some documentation...

[Eric Wieser]

https://leanprover-community.github.io/contribute/index.html is that documentation; the expectation is that you clone mathlib directly and work in that clone

[Sophie Morel]

Eric Wieser said:

https://leanprover-community.github.io/contribute/index.html is that documentation; the expectation is that you clone mathlib directly and work in that clone

Thanks, will do ! (Later today hopefully.)

[Eric Wieser]

It sounds like you're exploiting the fact that lake cloned it for you, but what lake giveth lake can also taketh away!

[Sophie Morel]

Okay, I finally figured it out, here is the new branch:
https://github.com/leanprover-community/mathlib4/tree/NontriviallNormedDivisionRing
In the first message of this thread, I explain what I changed so far and why. At first I was scared because CI sent me an email saying "some jobs were not successful", but apparently the thing does build and the problem is trailing whitespace/lines that are too long.

[Johan Commelin]

Yeah, the CI bots can be very angry when you trespass like that (-;

[Sophie Morel]

I feel properly ashamed of my behaviour. :exhausted: