Diagonalisation

Stream: maths

[Riccardo Brasca]

Is anyone working of diagonalisable endomorphisms? I would like to give this as a summer projects to some students. I am thinking about algebraic/geometric multiplicity of eigenvalues and stuff like that.

[Moritz Doll]

I would guess that @Heather Macbeth @Jireh Loreaux and @Frédéric Dupuis have opinions on that. the problem is to find the correct generality. finite dimensions are for sure overkill for most things. if you just want to do something with eigenvalues you probably don't need to assume that much, but then there is still the question whether to use linear maps (used in the fin-dim case), continuous linear maps (infinite-dim case for bounded operators) or partial linear maps (infinite case, unbounded operators).
I would say that if you just want some fun projects, then doing finite dimensional theory is probably a good idea, but the students should not expect to contribute to mathlib. for mathlib-ready code I would assume that we need some more discussions with the above mentioned people to figure out how these things should look like.

[Riccardo Brasca]

I will surely do finite dimensional (for the very good reason that the students don't know what Hilbert spaces/something more general are).

[Jireh Loreaux]

I actually think the finite dimensional version is definitely something we want in mathlib. It's more general than its infinite dimensional cousins because the scalar field isn't restricted to IsROrC and there is no need for an inner product space.

I think doing it for endomorphisms (linear maps) as opposed to matrices is the way to go, at least for the initial result. My opinion: go for it.

[Oliver Nash]

Exactly, there are really two theories here: a purely algebraic one (which allows quite general coefficients, at least for statements) and then an analytical theory. I claim that the existence of the latter doesn't really impinge on the former: the algebraic side is its own self-contained thing.

[Oliver Nash]

Probably the first definition to make is the concept of an endomorphism of a module being semi-simple (any invariant submodule has invariant complement).

[Scott Morrison]

One could define that for an endomorphism of an object in any category: we have the lattice of subobjects defined in great generality. :-)

[Johan Commelin]

We already have the structure theorem for f.g. modules over a PID, don't we? That should help.

[Patrick Massot]

I wonder whether the uniqueness part ever got finished.