Eigenvectors for semirings

Stream: maths

[Kenny Lau]

Module.End.HasEigenvector currently requires Ring because it is defined using generalised eigenspace, which doesn't mean much without subtraction. However, eigenvector itself doesn't really need subtraction, since it just says f x = μ • x ∧ x ≠ 0. Should we change the definition to generalise to semirings?

[Violeta Hernández]

I suspect the answer is the same answer to the question "do we need to talk about eigenvectors on semirings"?

[Kenny Lau]

i'm not an expert in semirings, so i don't want to be biased by this

[Kevin Buzzard]

If you change it then it will make mathlib slightly slower because it will have to work slightly harder to check that your ring is a semiring lots of times. What do we gain by changing this? Is there a mathematical reason?

My position on this has definitely changed from "woo let's do everything in absolutely the maximal generality" to "actually let's be pragmatic here. Does anyone care?"

[Kenny Lau]

Kevin Buzzard said:

work slightly harder to check that your ring is a semiring lots of times

it's already doing that every time you type Module

[Kenny Lau]

also a lot of times we have "shortcut instances"

[Michael Rothgang]

Often, you can literally weaken a definition - but the new definition becomes "wrong" in the more general context. Hence, I'm careful with just generalising definitions without any motivation at all.

[Michael Rothgang]

Do you have any motivating use case in mind? How much of the standard theory dies still work?

[Kenny Lau]

@Michael Rothgang in #29610 @Lawrence Wu (llllvvuu) discovered the following fact: if v is an eigenvector for T1 and T2 with e/val μ1 and μ2 then it is an eigenvector for T1*T2 with e/val μ2*μ1

[Kenny Lau]

(note that the order is reversed)