## Stream: maths

### Topic: linear maps over semimodule

#### 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.

#### 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.

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

#### 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

-- 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 (Jan 16 2020 at 15:45):

@Sebastien Gouezel Thanks for the attempt!

#### Johan Commelin (Jan 16 2020 at 15:45):

Too bad that it blows up

#### Reid Barton (Jan 16 2020 at 15:57):

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

#### Johan Commelin (Jan 16 2020 at 15:58):

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

#### 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 :-)

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

#### 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).

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

#### Sebastien Gouezel (Jan 16 2020 at 16:34):

Yes, the snippet is a minimal working example.

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

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

#### 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.

#### Daniel Selsam (Jan 16 2020 at 16:36):

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

#### Patrick Massot (Jan 16 2020 at 16:37):

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

#### Daniel Selsam (Jan 16 2020 at 16:37):

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

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

#### 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.

#### 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.

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

#### Daniel Selsam (Jan 17 2020 at 13:08):

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

#### Daniel Selsam (Jan 17 2020 at 18:56):

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

#### Daniel Selsam (Jan 17 2020 at 19:01):

(so should be instantaneous in Lean4)

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

#### 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