linear maps over semimodule

Stream: maths

[Sebastien Gouezel]

Right now, the identity does not make sense as a linear map from ℕ to ℕ as ℕ is not a ring, only a semiring. Would anyone object to defining linear maps on semimodules over semirings to allow "linear algebra" on ℕ-valued matrices? This shows up on #1883, where it is rightly argued that having the trace of an ℕ-valued matrix makes sense, and still I think it would be better to have the trace as a linear map.

[Chris Hughes]

I don't think there's even a change to the axioms, so this definitely makes sense.

[Kevin Buzzard]

I'm afraid that when I was making a push to get people to do commutative algebra in Lean, I had no idea what a semiring was ;-)

[Sebastien Gouezel]

I had a go at it, and I thought it would also be a good idea to let module be an abbreviation for semimodule. Everything compiles well, but some things become extremely slow, and I have not been able to adjust the instances (Yes, I want Lean 4 !! :)
MWE (with current mathlib):

import analysis.convex

-- attribute [instance, priority 200] add_comm_monoid.to_add_monoid
-- set_option trace.class_instances true

class inner_product_space (α : Type*) extends add_comm_monoid α, semimodule ℝ α

takes 30s on my laptop. With instances tracing on, it does not complete.

[Johan Commelin]

@Sebastien Gouezel Thanks for the attempt!

[Johan Commelin]

Too bad that it blows up

[Reid Barton]

This reminds me a bit of https://github.com/leanprover-community/mathlib/commit/89ece147049fb463f9ff320b73433fcdd32370ce

[Johan Commelin]

Except that this time the compile time is multiplied by 30 instead of divided by 3

[Sebastien Gouezel]

I am still hoping that @Floris van Doorn will tell me that there is an instance trick solving this :-)

[Reid Barton]

Well who hasn't gotten a constant off by a factor of 90 before, am I right?

[Patrick Massot]

If someone can minimize this then it will certainly interest Daniel (who is not reading this stream by the way).

[Daniel Selsam]

In the meantime, how about a non-minimized repro? Do I only need the snippet you posted above on top of current mathlib?

[Sebastien Gouezel]

Yes, the snippet is a minimal working example.

[Daniel Selsam]

Thanks. (I can't check this easily right now because I am currently building a modified mathlib for a different experiment)

[Sebastien Gouezel]

But I expect that you will tell me this problem is already solved by the algorithm you have developed for Lean 4. And I will be extremely happy about it, and extremely sad that I don't have Lean 4 yet :(

[Patrick Massot]

Do you know about the community cache-olean tool? It would allow to clone mathlib and get a compiled version from a few hours ago in about 20 seconds.

[Daniel Selsam]

For my experiments I generally need to rebuild mathlib with a differently-instrumented Lean3 each time.

[Patrick Massot]

Oh I see. Forget about reusing oleans then...

[Daniel Selsam]

(and I am reluctant to start having multiple mathlibs floating around at the same time)

[Patrick Massot]

But don't hesitate to tell us if you have a patched Lean3 that already fixes things :wink:

[Daniel Selsam]

Oh I see. Forget about reusing oleans then...

To clarify: to diagnose the problem discussed in this thread, I can reuse oleans and only run a modified Lean3 on the new file.

[Oliver Nash]

Who knew the trace of a matrix could be so controversial? Thank you all for the thoughts. I will have some time again at the weekend and will take this up again then.

[Sebastien Gouezel]

To clarify: to diagnose the problem discussed in this thread, I can reuse oleans and only run a modified Lean3 on the new file.

@Daniel Selsam , did you finally understand what is going wrong with this snippet?

[Daniel Selsam]

Not yet, I have been swamped with other things. It is on my list.

[Daniel Selsam]

@Sebastien Gouezel Diamonds. It tries to prove discrete_linear_ordered_field 60,000 times.

[Daniel Selsam]

(so should be instantaneous in Lean4)

[Sebastien Gouezel]

Thanks a lot for your investigation. Can you see from this a reasonable priority tweak that would avoid this crazy search? (And do you understand why the situation is so much different with semimodule and with module?)

[Yury G. Kudryashov]

One more reason to have linear maps on semimodules over semirings: I'd like to have convex for semimodules over nnreal to be able to say that the set of invariant measures of an endomorphism is convex.