mul on with_top

Stream: general

[Yakov Pechersky]

I'm working on developing the theory of tropical semirings. It has a lot to do with with_top R where [linear_ordered_semiring R]. Are there reasons why we have lemmas like docs#with_top.add_eq_top but nothing similar for mul? We have a variety of additive structures for with_top R but not mul. Is that because once you hit semiring, you have to make the unfortunate choice of what 0 * ⊤ is?

[Yakov Pechersky]

Relatedly, is there a reasonable definition for module R (with_top R) (lets say assuming [linear_ordered_semiring R])? Is it just

{ smul := λ k x, (k : with_top R) * x, ... }

[Yakov Pechersky]

Nope, module R (with_top R) doesn't work because of add_smul : (r + s) • x = r • x + s • x because one could have r + s = 0but neither r nor s be 0. And if x = ⊤, then it is not true.

[Kevin Buzzard]

You can see there will be a problem if you let R be a finite field of size q. Then all finite R-modules have size q^n for some n but with_top R has size q+1