Zulip Chat Archive

Stream: maths

Topic: eigenvalues and eigenvectors

Alexander Bentkamp (Apr 10 2019 at 17:18):

Hi, I'll start working on a proof that every endomorphism in a vectorspace over an algebraically closed field has an eigenvector. My goal is to formalize the eigendecomposition of a matrix later. That hasn't been formalized yet, right?

Johan Commelin (Apr 10 2019 at 17:20):

Nope, this hasn't been done yet.

Johan Commelin (Apr 10 2019 at 17:20):

Do we have algebraically closed fields ?! [/joke]

Johan Commelin (Apr 10 2019 at 17:21):

Are you identifying endomorphisms with matrices?

Johan Commelin (Apr 10 2019 at 17:22):

Note that we now know that V and dual K V are isomorphic. So you can identify End V with dual K V \tensor V. This might help for some things.

Alexander Bentkamp (Apr 10 2019 at 17:28):

I'll try to stay on the level of endomorphisms as long as possible. The corresponding theorem about matrices should be easy to derive from that.

Alexander Bentkamp (Apr 10 2019 at 17:34):

I planned to use linear_map from vector spaces for the endomorphisms. Do you think using End from category theory would be better?

Johan Commelin (Apr 10 2019 at 17:35):

No, that was just notation.

Johan Commelin (Apr 10 2019 at 17:36):

Atm we don't have a category of modules.

Johan Commelin (Apr 10 2019 at 17:36):

But we certainly want to have that at some point.

Alexander Bentkamp (Apr 10 2019 at 17:36):

and where is dual?

Alexander Bentkamp (Apr 10 2019 at 17:37):

ok, I found it :) Thanks!

Last updated: Dec 20 2023 at 11:08 UTC