# 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: May 14 2021 at 18:28 UTC