Cayley-Hamilton theorem

Stream: Is there code for X?

[Andrew Yang]

Do we have the following formulation of the Cayley-Hamilton theorem?

Let $A$ be a commutative ring, $M$ be a f.g. $A$-module, $I$ be an ideal of $A$, and $\phi \in \operatorname{End}_A(M)$ such that $\phi(M) \subseteq I M$.
Then there exists some $n \in \mathbb{N}$ and $a_i \in I^i$ such that $\phi^n = a_i \phi^{n-1} + \dots + a_n = 0$.

I see that we have linear_algebra/matrix/charpoly/* that works for all commutative rings, but it is in terms of matrices, and I couldn't find the condition on the coefficients.

I also see that we have linear_algebra/matrix/to_lin that turns a linear map to a matrix, but it seems like it needs a basis rather than merely a spanning set.

[Eric Wieser]

Maybe docs#matrix.pow_eq_aeval_mod_charpoly?

[Eric Wieser]

docs#linear_map.pow_eq_aeval_mod_charpoly

[Andrew Yang]

I'm not sure how to apply them in this scenario? Plus, the latter theorem seems to only apply to free modules.

[Eric Wieser]

It looks like that entire file only covers free modules

[Eric Wieser]

I found your version referenced elsewhere (in "M7210 Lecture 37") as "Generalized Cayley-Hamilton; see Eisenbud, Commutative Algebra, p. 120"

[Riccardo Brasca]

This is more general than the usual Cayley-Hamilton theorem, and I don't think we have it.

[Kevin Buzzard]

This result is used in the Atiyah-Macdonald proof of Nakayama's Lemma so it might be worth checking our proof of that

[Andrew Yang]

The proof of Nakayama's lemma in mathlib doesn't seem to follow Atiyah-Macdonald.

[Andrew Yang]

So I was trying to assign matrices to linear maps, and I ended up with this picture

Given $R$-modules $M$, $M'$, both $\operatorname{End}_R(M')$ and $\operatorname{End}_R(M)$ acts on $\operatorname{Hom}_R(M, M')$.
Now fix an $f \in \operatorname{Hom}_R(M, M')$. We say that an element of $\operatorname{End}_R(M')$ and an element of $\operatorname{End}_R(M)$ are associated if they take $f$ to the same image.
Then the subset of either endomorphism rings that has associates are $R$-subalgebras, and if $f$ is furthermore surjective, we obtain a $R$-algebra homomorphism from the former to the latter, mapping a function to its (unique) associate.

Is there something standard or easier or more general behind this?

[Kevin Buzzard]

This looks to me like a statement in category theory

[Kevin Buzzard]

(that doesn't ring a bell with me)

[Eric Wieser]

Given $R$-modules $M$, $M'$, both $\operatorname{End}_R(M')$ and $\operatorname{End}_R(M)$ acts on $\operatorname{Hom}_R(M, M')$.

Note that only the first of these is safe as a has_smul instance (and indeed, mathlib has it). We can't have both because of ambiguity when $M' = M$

[Kevin Buzzard]

One acts on the left, the other on the right.

[Eric Wieser]

Which would you say is which, mathematically? Currently the action of End R M' has a left-action on M →ₗ[R] M', which sounds like it might be the reverse of what you'd expect

[Kevin Buzzard]

I am confused because mathematically that doesn't look true to me.

[Kevin Buzzard]

If $\phi:M\to M'$ and $e,f:M'\to M'$ then $(\phi\circ e)\circ f=\phi\circ(e\circ f)$. [edit: this doesn't typecheck]

[Kevin Buzzard]

oh oops I'm wrong

[Kevin Buzzard]

I've been doing too much category theory :-( (composition of functions is in the opposite direction there!)

[Kevin Buzzard]

yeah, it's definitely the reverse of what I'd expect before I put pen to paper :-)

[Reid Barton]

You mean you've been doing too much category_theory

[Eric Wieser]

I'm sure there is a reason why an action of mul_opposite (End R M) on M →ₗ[R] M' (aka the right action in question) is a bad idea, but it would at least be consistent with composition when M' = M. I'll see if I can construct the problematic case next week.