Zulip Chat Archive

Stream: maths

Topic: eigenvalues and eigenvectors


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 10 2019 at 17:20):

Nope, this hasn't been done yet.

view this post on Zulip Johan Commelin (Apr 10 2019 at 17:20):

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

view this post on Zulip Johan Commelin (Apr 10 2019 at 17:21):

Are you identifying endomorphisms with matrices?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 10 2019 at 17:35):

No, that was just notation.

view this post on Zulip Johan Commelin (Apr 10 2019 at 17:36):

Atm we don't have a category of modules.

view this post on Zulip Johan Commelin (Apr 10 2019 at 17:36):

But we certainly want to have that at some point.

view this post on Zulip Alexander Bentkamp (Apr 10 2019 at 17:36):

and where is dual?

view this post on Zulip Alexander Bentkamp (Apr 10 2019 at 17:37):

ok, I found it :) Thanks!


Last updated: May 14 2021 at 18:28 UTC