Zulip Chat Archive

Stream: maths

Topic: linear maps over semimodule


view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 12:15):

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.

view this post on Zulip Chris Hughes (Jan 16 2020 at 13:31):

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

view this post on Zulip Kevin Buzzard (Jan 16 2020 at 14:21):

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 ;-)

view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 15:27):

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.

view this post on Zulip Johan Commelin (Jan 16 2020 at 15:45):

@Sebastien Gouezel Thanks for the attempt!

view this post on Zulip Johan Commelin (Jan 16 2020 at 15:45):

Too bad that it blows up

view this post on Zulip Reid Barton (Jan 16 2020 at 15:57):

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

view this post on Zulip Johan Commelin (Jan 16 2020 at 15:58):

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

view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 16:00):

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

view this post on Zulip Reid Barton (Jan 16 2020 at 16:07):

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

view this post on Zulip Patrick Massot (Jan 16 2020 at 16:26):

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

view this post on Zulip Daniel Selsam (Jan 16 2020 at 16:32):

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

view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 16:34):

Yes, the snippet is a minimal working example.

view this post on Zulip Daniel Selsam (Jan 16 2020 at 16:34):

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

view this post on Zulip Sebastien Gouezel (Jan 16 2020 at 16:35):

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 :(

view this post on Zulip Patrick Massot (Jan 16 2020 at 16:35):

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.

view this post on Zulip Daniel Selsam (Jan 16 2020 at 16:36):

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

view this post on Zulip Patrick Massot (Jan 16 2020 at 16:37):

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

view this post on Zulip Daniel Selsam (Jan 16 2020 at 16:37):

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

view this post on Zulip Patrick Massot (Jan 16 2020 at 16:38):

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

view this post on Zulip Daniel Selsam (Jan 16 2020 at 16:38):

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.

view this post on Zulip Oliver Nash (Jan 16 2020 at 22:41):

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.

view this post on Zulip Sebastien Gouezel (Jan 17 2020 at 09:41):

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?

view this post on Zulip Daniel Selsam (Jan 17 2020 at 13:08):

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

view this post on Zulip Daniel Selsam (Jan 17 2020 at 18:56):

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

view this post on Zulip Daniel Selsam (Jan 17 2020 at 19:01):

(so should be instantaneous in Lean4)

view this post on Zulip Sebastien Gouezel (Jan 17 2020 at 20:03):

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?)

view this post on Zulip Yury G. Kudryashov (Jan 23 2020 at 04:27):

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.


Last updated: May 11 2021 at 00:31 UTC