Endomorphism eigen values

Stream: new members

[Maxime Darrin]

Hi,

I'm trying to express that "0 \not \in sp(f) <-> f surjective" where f is an endomorphism. I wrote the following:

import algebra.module.linear_map
import linear_algebra.basic
import linear_algebra.eigenspace

example
(R : Type*) (E : Type*)
[semiring R]
[add_comm_group E] [module R E]
(f : module.End R E):

(¬ (f.has_eigenvalue 0)) <-> (⊤ : submodule R E).map f = ⊤
:= sorry

I get an error about the type of f that I do not understand. What am i doing wrong?

[Adam Topaz]

What's the error?

[Kevin Buzzard]

One thing you're doing wrong is that I very much doubt that this is true without some finiteness hypotheses

[Kevin Buzzard]

Eg consider the abelian group hom $E:=\Z[X]\to\Z[X]$ sending X to 2X

[Maxime Darrin]

The error

type mismatch at application
  f.has_eigenvalue
term
  f
has type
  module.End R E : Type ?
but is expected to have type
  module.End ?m_1 ?m_2 : Type ?

And yeah, ok I forgot the finiteness

[Eric Wieser]

Probably you need R to be a ring

[Adam Topaz]

So this should suggest to you that the has_eigenvalue function requires some typeclass which you don't have. I suggest starting there

[Eric Wieser]

docs#module.End.has_eigenvalue

[Eric Wieser]

comm_ring R

[Kevin Buzzard]

Hover over has_eigenvalue in your code and you'll see what assumptions it needs

[Kevin Buzzard]

Or do what Eric did and then click on the link

[Maxime Darrin]

Thanks i got it

example
(R : Type*) (E : Type*)
[field R]
[add_comm_group E] [module R E]
(f : module.End R E):
finite_dimensional R E -> ((¬ (f.has_eigenvalue 0)) <-> (⊤ : submodule R E).map f = ⊤)
:= sorry

Is this the correct way to add the finite dimensionality hypothesis ?

[Johan Commelin]

Just add [finite_dimensional R E] before you introduce f

[Kevin Buzzard]

But this looks good now