Semiconjugate matrices

Stream: Is there code for X?

[Yaël Dillies]

Do we have the fact that semiconjugate matrices share an eigenvalue?

[Eric Wieser]

Do we even have eigenvalues of matrices?

[Yaël Dillies]

Oh this is really a statement about endomorphisms actually. Note that not all of them have to be of the same type. We can have f : \a -> \a, g : \a -> \b, h : \b -> \b and the hypothesis f • g = g • h.

[Eric Wieser]

Did you mean ∘?

[Eric Wieser]

f • g doesn't typecheck there

[Yaël Dillies]

Yes sorry I'm on my phone

[Yaël Dillies]

Do we have that the transpose of a matrix A has the same eigenvalues as A? or rather the endomorphism version?

[Kevin Buzzard]

Presumably the endomorphism version is a statement about duals. Does it need a finite-dimensionality hypothesis?

[Yaël Dillies]

I think not

[Eric Wieser]

Or would it be a statement about docs#linear_map.adjoint / docs#continuous_linear_map.adjoint?

[Yaël Dillies]

I would finger guess linear_map.adjoint indeed.

[Eric Wieser]

That one _does_ require finite-dimensionality

[Antoine Labelle]

You don't need inner products for the endomorphism version, you can formulate it in terms of docs#module.dual.transpose. I'm pretty sure that we don't have the statement for endomorphisms, given that we didn't even have the fact that the trace is the same until three days ago.

[Anatole Dedecker]

But I don’t think it will work in infinite dimensional spaces

[Anatole Dedecker]

In general you can only prove that an eigenvalue of f is an eigenvalue of its transpose, but I think I have a counterexample for the converse

[Kevin Buzzard]

I think that the k-linear endomorphism of nat ->_0 k sending e_n to e_{n+1} doesn't have any eigenvalues but its dual has loads. What do you think @Yaël Dillies ?

[Anatole Dedecker]

Yes, that’s what I had in mind