Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: mathematics

Topic: Nakayama's lemma

John Baez (Aug 30 2023 at 08:31):

I never took a course on commutative algebra because in grad school I was mainly interested in mathematical physics, so I'm just finally now learning Nakayama's lemma - because I need it for something.

John Baez (Aug 30 2023 at 08:34):

There are many alternative formulations, some perhaps easier to remember than others. MathOverflow someone gave this nice mnemonic for it which happens to match what I actually need:

$I M = M \implies i m = m$

What does this mean? It means:

Nakayama's Lemma. Let $I$ be an ideal in a commutative ring $R$ and let $M$ be a finitely generated $R$-module. If $IM=M$ then there exists $i \in I$ such that $im = m$ for all $m \in M$.

John Baez (Aug 30 2023 at 08:37):

This instantly implies something I wanted to know: if $I$ is an ideal in a commutative ring $R$ with $I^2 = I$, then $I = p R$ for some $p \in R$ with $p^2 = p$.

John Baez (Aug 30 2023 at 08:43):

Starting from this simple formulation I'm finally getting more interested in the many alternative formulations and consequences, some of which sound more conceptual, like

If $f: M \to M$ is a surjective endomorphism of a finitely generated $R$-module, then $f$ is an isomorphism.

John Baez (Aug 30 2023 at 08:44):

or

Any basis of the fiber of a coherent sheaf at a point extends to a minimal generating set of local sections.

John Baez (Aug 30 2023 at 08:46):

or

A finitely generated module over a local ring is projective only if it is free.

Jean-Baptiste Vienney (Aug 30 2023 at 11:44):

John Baez said:

This instantly implies something I wanted to know: if $I$ is an ideal in a commutative ring $R$ with $I^2 = I$, then $I = p R$ for some $p \in R$ with $p^2 = p$.

I don't understand how you get this instantly. And is it even true? I've seen it written on the internet with the additional hypothesis that $I$ is finitely generated.

James Deikun (Aug 30 2023 at 11:51):

The ideal does have to be finitely generated to apply Nakayama's Lemma, indeed. But otherwise it's immediate, as:

• an ideal inherits the structure of a module,
• therefore there exists $p \in I$ with $pi = i$ for all $i \in I$,
• in particular, $p^2 = p$,
• $pR \subseteq I$ since $p \in I$; $I \subseteq pR$ since $pI = I$.

Todd Trimble (Aug 30 2023 at 12:19):

John Baez said:

Starting from this simple formulation I'm finally getting more interested in the many alternative formulations and consequences, some of which sound more conceptual, like

If $f: M \to M$ is a surjective endomorphism of a finitely generated $R$-module, then $f$ is an isomorphism.

Yes, this is a good one. Nakayama's lemma seems to be like Yoneda's lemma, being one of these simple results that people in the know use all the time and is coincidentally named after a Japanese mathematician.

I'm not particularly in the know, but over a decade ago I wrote at the nLab, "Nakayama’s lemma is a simple but fundamental result of commutative algebra frequently used to lift information from the fiber of a sheaf over a point (as for example a coherent sheaf over a scheme) to give information on the stalk at that point".

I began writing the article after getting some glimmers of what it was really about (in the minds of people who really use the stuff) from this MathOverflow thread, I think especially the answer by Roy Smith. I especially like the application to the algebraic geometry form of the inverse function theorem.

John Baez (Aug 30 2023 at 12:34):

James Deikun said:

The ideal does have to be finitely generated to apply Nakayama's Lemma, indeed.

Yes, I meant to say "finitely generated ideal".

Here's a nice counterexample when your ideal is not finitely generated. Let $R$ be the ring of continuous complex-valued functions on $[0,1]$ and let $I$ be the ideal consisting of functions that vanish at $0$. Then $I^2 = I$ but $I$ is not of the form $p R$ for any idempotent $p \in R$ (which would need to be a continuous function that only takes the values $0$ and/or $1$).

John Baez (Aug 30 2023 at 12:38):

Todd Trimble said:

Nakayama's lemma seems to be like Yoneda's lemma, being one of these simple results that people in the know use all the time and is coincidentally named after a Japanese mathematician.

I was thinking about that. But what I'd really like to do is derive Nakayama's lemma from the Yoneda lemma! Then I could annoy people by saying "Nakayama's lemma? That's just a corollary of the Yoneda lemma."

John Baez (Aug 30 2023 at 12:41):

Now, it may be hopeless to derive the Nakayama lemma from the Yoneda lemma. But the Nakayama lemma does follow from ideas connected to the Cayley-Hamilton theorem, and that theorem has a vaguely Yoneda-ish feel, at least in my fevered brain.

John Baez (Aug 30 2023 at 12:42):

Remember, it says that if you take a square matrix $A$ and define its characteristic polynomial $p$ by

$p(\lambda) = \mathrm{det}(\lambda I - A)$

then you get

$p(A) = 0$

John Baez (Aug 30 2023 at 12:44):

There's some sort of weird self-reference here, like "$A$ is the walking root of its own characteristic polynomial".

John Baez (Aug 30 2023 at 12:45):

And that "walking" business feels vaguely Yoneda-esque (to my fevered brain).

John Baez (Aug 30 2023 at 12:45):

Here's a fake one-line proof of the Cayley-Hamilton theorem:

$p(A) = \mathrm{det}(A I - A) = 0$

John Baez (Aug 30 2023 at 12:46):

Puzzle for beginners: spot why this proof is fake.

Puzzle for experts: try to morph it into a real proof!

Steve Huntsman (Aug 30 2023 at 12:54):

John Baez said:

Puzzle for beginners: spot why this proof is fake.

Puzzle for experts: try to morph it into a real proof!

Jean-Baptiste Vienney (Aug 30 2023 at 13:37):

I'd be glad to see (or better find) a proof which use modern tools, ie. that I could understand easily (in my head, the more there is structure and the less there are tricks, the easier it is to understand). A modern definition of the determinant is like this:

• For every $k$-vector space $E$ of dimension $n$, and for every $1 \le k \le n$, there is the $k^{th}$ exterior power $\Lambda^k(E)$ of $E$ which is the quotient of the $k^{th}$ tensor power $E^{\otimes k}$ by the equalities $v_{\sigma(1)} \otimes ... \otimes v_{\sigma(k)} = \epsilon(\sigma).v_{1} \otimes ... \otimes v_{k}$ for every permutation $\sigma \in \mathfrak{S}_{k}$ and where $\epsilon(\sigma)$ is the signature of $\sigma$ (the next exterior powers are not very interesting because they are equal to $0$)

• If $(e_{1},...,e_{n})$ is a basis of $E$, then the $e_{i_{1}} \wedge ... \wedge e_{i_{k}}$ where $1 \le i_{1} < ... < i_{k} \le n$ form a basis of $\Lambda^k(E)$. It follows that $dim(\Lambda^k(E))=\binom{n}{k}$. In particular $(e_{1} \wedge ... \wedge e_{n})$ is a basis of $\Lambda^n(E)$ which is then of dimension $1$.

• As for tensor powers, you can take the exterior power of a map. If $u:E \rightarrow E$ is an endomorphism, then $\Lambda^n(u):\Lambda^n(V) \rightarrow \Lambda^n(V)$ sends $e_{1}\wedge ... \wedge e_{n}$ to $\lambda.e_{1}\wedge ... \wedge e_{n}$ for a unique $\lambda \in k$.

The definition of $det(u)$ is then:

• $det(u)$ is the unique scalar such that $\Lambda^n(u)=det(u).1_{\Lambda^n(E)}$ ie. such that $\Lambda^n(u)(e_1 \wedge ... \wedge e_n)=det(u).e_{1} \wedge ... \wedge e_n$

Jean-Baptiste Vienney (Aug 30 2023 at 13:52):

By definition, the characteristic polynomial $p(u)$ of $u$ is then given by:

• $p(u)(\lambda)$ is the unique scalar such that $\Lambda^{n}(\lambda.1_E-u)=p(u).1_{\Lambda^n(E)}$

Jean-Baptiste Vienney (Aug 30 2023 at 13:56):

Let's verify that $p(u)$ is really a polynomial (map) first.

Jean-Baptiste Vienney (Aug 30 2023 at 13:59):

$\Lambda^{n}(\lambda.1_E-u)$ is the map from $\Lambda^n(E)$ to $\Lambda^n(E)$ which acts like this on the basis

$(1)\quad$ $e_{1}\wedge ... \wedge e_n \mapsto$
$(\lambda.1_E-u)(e_1)\wedge ... \wedge (\lambda.1_E-u)(e_n) = (\lambda.e_1-u(e_1)) \wedge ... \wedge (\lambda.e_n-u(e_n))$

Jean-Baptiste Vienney (Aug 30 2023 at 14:09):

The matrix $(a_{k,l})_{1 \le k,l \le n}$ of $u$ is defined by the equations
$(2)\quad u(e_k) = \underset{1 \le l \le n}{\sum}a_{k,l}.e_{l}\quad\forall 1 \le k \le n$

Jean-Baptiste Vienney (Aug 30 2023 at 14:11):

Let me use $(2)$ into $(1)$. Now I get that $\Lambda^{n}(\lambda.1_E-u)$ is the map from $\Lambda^n(E)$ to $\Lambda^n(E)$ which acts like this on the basis:

Jean-Baptiste Vienney (Aug 30 2023 at 14:12):

$e_{1}\wedge ... \wedge e_n \mapsto$
$(\lambda.e_1-\underset{1 \le l \le n}{\sum}a_{1,l}.e_{l}) \wedge ... \wedge (\lambda.e_n-\underset{1 \le l \le n}{\sum}a_{n,l}.e_{l})$

Jean-Baptiste Vienney (Aug 30 2023 at 14:15):

ie. $\Lambda^{n}(\lambda.1_E-u)(e_1 \wedge ... \wedge e_n)$
$= (\lambda.e_1-\underset{1 \le l \le n}{\sum}a_{1,l}.e_{l}) \wedge ... \wedge (\lambda.e_n-\underset{1 \le l \le n}{\sum}a_{n,l}.e_{l})$

Jean-Baptiste Vienney (Aug 30 2023 at 14:29):

$= ((\lambda-a_{1,1}).e_1- a_{1,2}.e_{2}-...-a_{1,n}e_n) \wedge ... \wedge (-a_{n,1}.e_{1}-...-a_{n,n-1}e_{n-1}+(\lambda-a_{n,n}).e_n)$

Jean-Baptiste Vienney (Aug 30 2023 at 14:37):

$= \underset{1 \le i_1,...,i_n \le n}{\sum}c_{i_1,...,i_n}.e_{i_1}\wedge...\wedge e_{i_n}$

Jean-Baptiste Vienney (Aug 30 2023 at 14:38):

where $c_{i_1,...,i_n}$ is a uniquely determined scalar.

Jean-Baptiste Vienney (Aug 30 2023 at 14:52):

$(*)\quad$ Remember that $v_{\sigma(1)} \wedge ... \wedge v_{\sigma(n)} = \epsilon(\sigma).v_{1}\wedge...\wedge v_{n}$ which gives in particular that $v_{1} \wedge ... \wedge v_{n}=0$ when there is a couple $1 \le i < j \le n$ such that $v_{i}=v_{j}$.

Todd Trimble (Aug 30 2023 at 14:55):

For what it's worth, the Cayley-Hamilton theorem is proved in the nLab here, as a relatively easy consequence of Cramer's rule. By the way, Cayley-Hamilton holds over any commutative ring.

Jean-Baptiste Vienney (Aug 30 2023 at 14:55):

Yeah, thanks. I'm just trying to do my proof (I do the puzzle).

Jean-Baptiste Vienney (Aug 30 2023 at 14:57):

I prefer if there is no use of something like the Cramer's rule and if it follows from a direct computation by applying the definitions (that's probably a matter of taste). But I can't guarantee that it is not going to take me the whole day -- if it works.

Jean-Baptiste Vienney (Aug 30 2023 at 15:02):

So, I continue my computation.

Jean-Baptiste Vienney (Aug 30 2023 at 15:05):

Let me rewrite slightly differently what I wrote before (I deleted all the terms which are equal to $0$ using $(*)$ and enumerated the other ones using the symmetric group):

Jean-Baptiste Vienney (Aug 30 2023 at 15:13):

$\Lambda^{n}(\lambda.1_E-u)(e_1 \wedge ... \wedge e_n)$
$=\underset{\sigma \in \mathfrak{S_n}}{\sum}c_{\sigma(1),...,\sigma(n)}.e_{\sigma(1)}\wedge ... \wedge e_{\sigma(n)}$

Todd Trimble (Aug 30 2023 at 15:15):

John Baez said:

Todd Trimble said:

Nakayama's lemma seems to be like Yoneda's lemma, being one of these simple results that people in the know use all the time and is coincidentally named after a Japanese mathematician.

I was thinking about that. But what I'd really like to do is derive Nakayama's lemma from the Yoneda lemma! Then I could annoy people by saying "Nakayama's lemma? That's just a corollary of the Yoneda lemma."

That's a fun motivation: finding a new way to annoy people using the Yoneda lemma. JK

I don't have a lot to say at the moment about a connection between the two, but it does remind me of stuff that Andre Scedrov said near the beginning of his AMS Memoir Forcing and Classifying Topoi. On page 11, he cites one of the standard approaches to proving the Cayley-Hamilton theorem as an example of universal thinking: "one always takes only the bare essentials needed to satisfy the hypothesis". So here, he says, "If ... $P_M(t) = \det(tI - M)$, then showing $P_M(M) = 0$ at once is too hard. Rather, think of $tI - M$ as a matrix over $k[t]$, $E$ as a module over $k[t]$, and show $P_M(t)E = 0$ in this setting."

Where is he going with this? He's making an analogy with the process also described by Lawvere in his Variable Sets, Etendu, and Variable Structures in Topoi: just as one goes from a ring of constants $k$ to $k[t]$ by adjoining a variable, so one can move from "constant sets" to more "variable sets" (e.g., presheaf toposes), and then the forcing process (localizing with respect to forcing conditions) is analogous to taking a quotient modulo an ideal, tailor-made to fit the hypotheses one is after.

So there is the idea of using generic elements. In the Yoneda lemma, one considers an identity morphism as a "generic generalized element".

That's all I got at the moment... wish I had more.

Todd Trimble (Aug 30 2023 at 15:17):

Jean-Baptiste Vienney said:

Yeah, thanks. I'm just trying to do my proof (I do the puzzle).

No, I know, and sorry to interrupt -- I thought you were done for the moment. Actually, I wasn't mainly talking to you, I was talking to everybody. Carry on...

Jean-Baptiste Vienney (Aug 30 2023 at 15:18):

Todd Trimble said:

Jean-Baptiste Vienney said:

Yeah, thanks. I'm just trying to do my proof (I do the puzzle).

No, I know, and sorry to interrupt -- I thought you were done for the moment. Actually, I wasn't mainly talking to you, I was talking to everybody. Carry on...

Ok :sweat_smile: . I wasn't sure if you were annoyed by my try or not. I take pauses.

Jean-Baptiste Vienney (Aug 30 2023 at 15:19):

Actually, I've never had a good understanding of this theorem and I didn't know exterior powers or even the tensor product when I learned it so I'm trying to see what I can do today using these tools (by the way I haven't used the hypothesis that the scalars are in a field, maybe the one that $r+r\neq 0$ if $r \neq 0$, not sure)

Jean-Baptiste Vienney (Aug 30 2023 at 15:24):

I use again $(*)$ to get:
$\Lambda^{n}(\lambda.1_E-u)(e_1 \wedge ... \wedge e_n)$
$=\underset{\sigma \in \mathfrak{S_n}}{\sum}\epsilon(\sigma).c_{\sigma(1),...,\sigma(n)}.e_{1}\wedge ... \wedge e_{n}$

Jean-Baptiste Vienney (Aug 30 2023 at 15:26):

So, we have:
$(3) \quad p(u)(\lambda)=\underset{\sigma \in \mathfrak{S_n}}{\sum}\epsilon(\sigma).c_{\sigma(1),...,\sigma(n)}$

Jean-Baptiste Vienney (Aug 30 2023 at 15:30):

The $c_{i_{1},...,i_{n}}$ are polynomials in $\lambda$ (of degree $\le n$), which depend on the matrix of $u$, although I don't want to write down the expression explicitely...

Jean-Baptiste Vienney (Aug 30 2023 at 15:32):

So $p(u)(\lambda)$ is really a polynomial (of degree $n$) in $\lambda$.

Jean-Baptiste Vienney (Aug 30 2023 at 15:33):

Now, we want to prove that $p(u)(u)=0$

Jean-Baptiste Vienney (Aug 30 2023 at 15:43):

Well, I can't make any further progress if I don't work on the coefficients $c_{\sigma(1),...,\sigma(n)}$

Jean-Baptiste Vienney (Aug 30 2023 at 15:54):

I can decompose
$(4) \quad c_{\sigma(1),...,\sigma(n)}=d^{\sigma}_1...d^{\sigma}_n$

Jean-Baptiste Vienney (Aug 30 2023 at 16:04):

Jean-Baptiste Vienney said:

$= ((\lambda-a_{1,1}).e_1- a_{1,2}.e_{2}-...-a_{1,n}e_n) \wedge ... \wedge (-a_{n,1}.e_{1}-...-a_{n,n-1}e_{n-1}+(\lambda-a_{n,n}).e_n)$

I'm gonna try to compute some coefficients here to get an idea

Jean-Baptiste Vienney (Aug 30 2023 at 16:06):

The coeff before $e_{1}\wedge...\wedge e_n$ is $(\lambda-a_{1,1})(\lambda-a_{2,2})...(\lambda-a_{n,n})$

Jean-Baptiste Vienney (Aug 30 2023 at 16:08):

The coeff before $e_{1} \wedge e_{3} \wedge e_{2}$ (if we had $n=3$) would be $(\lambda-a_{1,1})(-a_{2,3})(-a_{3,2})$

Jean-Baptiste Vienney (Aug 30 2023 at 16:10):

The coeff before $e_{3}\wedge e_{2} \wedge e_{1}$ would be $(-a_{1,3})(\lambda-a_{2,2})(-a_{3,1})$

Jean-Baptiste Vienney (Aug 30 2023 at 16:10):

So, there is a pattern

Jean-Baptiste Vienney (Aug 30 2023 at 16:12):

The coeff before $e_{\sigma(1)} \wedge ...\wedge e_{\sigma(n)}$ is my $c_{\sigma(1),...,\sigma(n)}=d_{1}^{\sigma}...d_{n}^{\sigma}$ where for every $1 \le i \le n$:

Jean-Baptiste Vienney (Aug 30 2023 at 16:14):

$(5a)\quad d_{i}^{\sigma}=(-a_{i,\sigma(i)})$ if $i \neq \sigma(i)$

Jean-Baptiste Vienney (Aug 30 2023 at 16:14):

$(5b) \quad d_{i}^{\sigma}=(\lambda-a_{i,\sigma(i)})$ if $i = \sigma(i)$

Jean-Baptiste Vienney (Aug 30 2023 at 16:31):

Let's combine $(3),(4),(5)$:

Jean-Baptiste Vienney (Aug 30 2023 at 16:35):

$(6) \quad p(u)(\lambda) = \underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}) \underset{1 \le i \le n,~ i = \sigma(i)}{\prod}(\lambda-a_{i,\sigma(i)})$

Jean-Baptiste Vienney (Aug 30 2023 at 16:36):

Now, it's very clear that $p(u)(\lambda)$ is a polynomial!

Jean-Baptiste Vienney (Aug 30 2023 at 16:39):

We thus want to prove that:
$(7)\quad \underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}) \underset{1 \le i \le n,~ i = \sigma(i)}{\prod}(u-a_{i,\sigma(i)}.1_E)=0$

Jean-Baptiste Vienney (Aug 30 2023 at 17:09):

Be aware that the second product must be interpreted as a composite...

Jean-Baptiste Vienney (Aug 30 2023 at 17:14):

Let's note $(e_{1}^*,...,e_{n}^*)$ the dual basis of $(e_1,...,e_n)$

Jean-Baptiste Vienney (Aug 30 2023 at 17:31):

I'm going to use the natural isomorphism $End(E) \cong E \otimes E^*$

Jean-Baptiste Vienney (Aug 30 2023 at 17:33):

which sends an endomorphism $v$ to $\underset{1 \le k,l \le n}{\sum}e_l^*(v(e_k)).e_{l}\otimes e_k^*$

Jean-Baptiste Vienney (Aug 30 2023 at 17:39):

(Note that $e_{l}^*(v(e_k)))$ is just the coefficients $(k,l)$ in the matrix of $v$)

Jean-Baptiste Vienney (Aug 30 2023 at 17:39):

In fact it is also an isomorphism of $k$-algebras

Jean-Baptiste Vienney (Aug 30 2023 at 17:44):

The product in $E \otimes E^*$ is given by $(v \otimes \phi) \otimes (w \otimes \psi) \mapsto \phi(w).v \otimes \psi$

Jean-Baptiste Vienney (Aug 30 2023 at 17:46):

(The idea is that $\psi$ absorbs the initial entry, $w$ is an intermediate output, $\phi$ absorbs this intermediate output, and then $v$ is a final output, that's why you get the coefficient $\phi(w)$)

Jean-Baptiste Vienney (Aug 30 2023 at 17:50):

I'm going to rewrite the LHS of $(7)$ as the $n$-ary product applied to an element of $(E \otimes E^*)^{\otimes n}$ ie. I will explicit an element $y \in (E \otimes E^*)^{\otimes n}$ such that if we consider the $n$-ary product $\nabla^n:(E \otimes E^*)^{\otimes n} \rightarrow (E \otimes E^*)$, then the LHS of $(7)$ is equal to $\nabla^n(y)$

Jean-Baptiste Vienney (Aug 30 2023 at 17:54):

I do that because it feels too hard to compute the composite/product directly

Jean-Baptiste Vienney (Aug 30 2023 at 17:57):

but it will still replace $u$ by coefficients of its matrix + basis and dual basis elements in this LHS, so it should be better

Jean-Baptiste Vienney (Aug 30 2023 at 18:03):

Yeah, @James Deikun help me!! (or if you have something else in the same vein)

Jean-Baptiste Vienney (Aug 30 2023 at 18:04):

I changed the product because in $(7)$ you compose with $\circ$

James Deikun (Aug 30 2023 at 18:06):

Let's see:

• we have $R$ a commutative ring, and $V$ an $R$-module.
• $\mathrm{det'} : V^V \to {V^{\wedge n}}^{V^{\wedge n}}$ is the function that extends endomaps to the "last" exterior power.
• It is polynomial because [reasons to be determined later].
• We can compose this with the inverse of $-I : R \to {V^{\wedge n}}^{V^{\wedge n}}$ to get $\mathrm{det} : V^V \to R$.
• We can compose this with the affine map $-I - A :: R \to V^V$ to get $\mathrm{char} : R \to R$ which is polynomial because we composed some polynomials.
• We extend all this to be over $V^V$ by extension of scalars.
• In particular, we extend the determinant from $V^V$ to $V^V \otimes V^V$ and take $\mathrm{det}(A \otimes I - I \otimes A)$.

Jean-Baptiste Vienney (Aug 30 2023 at 18:10):

Under my isomorphism of $k$-algebras, the fact $(7)$ that I want to prove is now equivalent to proving that this vector is equal to $0$:
$(8)$
$\nabla^n\bigg(\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}) \underset{1 \le i \le n,~ i = \sigma(i)}{\bigotimes}(\underset{1 \le k,l \le n}{\sum}e_l^*(u(e_k)).e_{l}\otimes e_k^*-a_{i,\sigma(i)}.\underset{1 \le m \le n}{\sum}e_{m}\otimes e_{m}^*)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 18:11):

but recall that the $e_{l}^*(u(ek))=a_{k,l}$ are just the coefficients of the matrix of $u$

Jean-Baptiste Vienney (Aug 30 2023 at 18:14):

so this vector is equal to:

Jean-Baptiste Vienney (Aug 30 2023 at 18:14):

$(9)$

Jean-Baptiste Vienney (Aug 30 2023 at 18:14):

$\nabla^n\bigg(\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}) \underset{1 \le i \le n,~ i = \sigma(i)}{\bigotimes}(\underset{1 \le k,l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*-a_{i,\sigma(i)}.\underset{1 \le m \le n}{\sum}e_{m}\otimes e_{m}^*)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 18:18):

Bceause everything is linear, I can move all the coefficients out of the product $\nabla^n$. Let's do it in several steps.

Jean-Baptiste Vienney (Aug 30 2023 at 18:19):

First, $(9)$ is equal to:

Jean-Baptiste Vienney (Aug 30 2023 at 18:20):

$(10)$
$\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}).\nabla^n\bigg( \underset{1 \le i \le n,~ i = \sigma(i)}{\bigotimes}(\underset{1 \le k,l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*-a_{i,\sigma(i)}.\underset{1 \le m \le n}{\sum}e_{m}\otimes e_{m}^*)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 18:27):

I'm going to put all the coefficients before vectors of the type $e_{m}\otimes e_{m}^*$ together in the above expression. I obtain:

Jean-Baptiste Vienney (Aug 30 2023 at 18:31):

$\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}).\nabla^n\bigg( \underset{1 \le i \le n,~ i = \sigma(i)}{\bigotimes}(\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*+\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,\sigma(i)}).e_{m}\otimes e_{m}^*)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 18:32):

I just do a tiny simplification by replacing $\sigma(i)$ by $i$ when they are equal. I obtain:

Jean-Baptiste Vienney (Aug 30 2023 at 18:32):

$\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}).\nabla^n\bigg( \underset{1 \le i \le n,~ i = \sigma(i)}{\bigotimes}\Big(\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*+\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*\Big)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 18:38):

Clearly, the thing to do now is to develop the big tensor product inside the $\nabla^n$

Jean-Baptiste Vienney (Aug 30 2023 at 18:48):

I want to apply a distributivity like this (where $I$ is a finite set):
$\underset{i \in I}{\bigotimes} (y_i^1 + y_i^2) = \underset{\alpha:I \rightarrow \{1,2\}}{\sum}~~\underset{i \in I}{\bigotimes}~y_{i}^{\alpha(i)}$

Jean-Baptiste Vienney (Aug 30 2023 at 18:50):

Here $I$ is $\{1 \le i \le n, ~i = \sigma(i)\}$

Jean-Baptiste Vienney (Aug 30 2023 at 18:53):

$y_{i}^{1}$ is $\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*$

Jean-Baptiste Vienney (Aug 30 2023 at 18:54):

$y_i^2$ is $\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*$

Jean-Baptiste Vienney (Aug 30 2023 at 18:56):

I want to find, given a function $\alpha:I \rightarrow \{1,2\}$, how I can write $\underset{i \in I}{\bigotimes}~y_{i}^{\alpha(i)}$ in a good way (with $I$, $y_{i}^{1}$, $y_{i}^{2}$ as above)

Jean-Baptiste Vienney (Aug 30 2023 at 19:01):

$y_{i}^{1} =: y^1$ doesn't depend on $i$ here

Jean-Baptiste Vienney (Aug 30 2023 at 19:02):

so that $\underset{i \in I}{\bigotimes}~y_{i}^{\alpha(i)} = (y^1)^{\otimes |\alpha^{-1}(1)|} \otimes \underset{i \in \alpha^{-1}(2)}{\bigotimes}~y_{i}^{2}$

Jean-Baptiste Vienney (Aug 30 2023 at 19:04):

ie. by replacing $y^1$ and $y_i^2$ by their respective expression:

Jean-Baptiste Vienney (Aug 30 2023 at 19:05):

$\underset{i \in I}{\bigotimes}~y_{i}^{\alpha(i)} = (\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*)^{\otimes |\alpha^{-1}(1)|} \otimes \underset{i \in \alpha^{-1}(2)}{\bigotimes}~(\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*)$

Jean-Baptiste Vienney (Aug 30 2023 at 19:06):

So that I get
$\underset{i \in I}{\bigotimes} (y_i^1 + y_i^2) = \underset{\alpha:I \rightarrow \{1,2\}}{\sum}~(\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*)^{\otimes |\alpha^{-1}(1)|} \otimes \underset{i \in \alpha^{-1}(2)}{\bigotimes}~(\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*)$

Jean-Baptiste Vienney (Aug 30 2023 at 19:08):

I just replace the $I$ by its expression:

Jean-Baptiste Vienney (Aug 30 2023 at 19:08):

$\underset{i \in I}{\bigotimes} (y_i^1 + y_i^2) = \underset{\alpha:\{1 \le i \le n, ~i = \sigma(i)\} \rightarrow \{1,2\}}{\sum}~(\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*)^{\otimes |\alpha^{-1}(1)|} \otimes \underset{i \in \alpha^{-1}(2)}{\bigotimes}~(\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*)$

Jean-Baptiste Vienney (Aug 30 2023 at 19:09):

And I put this in $(10)$ to get:

Jean-Baptiste Vienney (Aug 30 2023 at 19:09):

$(11)$
$\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)}).\nabla^n\bigg(\underset{\alpha:\{1 \le i \le n, ~i = \sigma(i)\} \rightarrow \{1,2\}}{\sum}~(\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*)^{\otimes |\alpha^{-1}(1)|} \otimes \underset{i \in \alpha^{-1}(2)}{\bigotimes}~(\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 19:09):

Ouch

Jean-Baptiste Vienney (Aug 30 2023 at 19:11):

I recall that the Cayley-Hamilton theorem is equivalent to: for every $u:E \rightarrow E$, if $(e_{1},...,e_{n})$ is a basis of $E$, and $(a_{k,l})_{1 \le k,l \le n}$ the matrix of $u$ then $(11)$ is equal to $0$...

Jean-Baptiste Vienney (Aug 30 2023 at 19:15):

I can move the first sum out of $\nabla^n$ to get:

Jean-Baptiste Vienney (Aug 30 2023 at 19:16):

$(12)$
$\underset{\sigma \in \mathfrak{S}_n}{\sum}\epsilon(\sigma)\underset{1 \le i \le n, ~i \neq \sigma(i)}{\prod}(-a_{i,\sigma(i)})\underset{\alpha:\{1 \le i \le n, ~i = \sigma(i)\} \rightarrow \{1,2\}}{\sum}~\nabla^n\bigg((\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*)^{\otimes |\alpha^{-1}(1)|} \otimes \underset{i \in \alpha^{-1}(2)}{\bigotimes}~(\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*)\bigg)$

Jean-Baptiste Vienney (Aug 30 2023 at 19:18):

I still must use distributivities to move stuff outside of $\nabla^n$ and finally be able to perform the multiplication

Jean-Baptiste Vienney (Aug 30 2023 at 19:30):

I must distribute here:

Jean-Baptiste Vienney (Aug 30 2023 at 19:30):

$(\underset{1 \le k \neq l \le n}{\sum}a_{k,l}.e_{l}\otimes e_k^*)^{\otimes |\alpha^{-1}(1)|}$

Jean-Baptiste Vienney (Aug 30 2023 at 19:31):

and here:

Jean-Baptiste Vienney (Aug 30 2023 at 19:31):

$\underset{i \in \alpha^{-1}(2)}{\bigotimes}~(\underset{1 \le m \le n}{\sum}(a_{m,m}-a_{i,i}).e_{m}\otimes e_{m}^*\big)$

Jean-Baptiste Vienney (Aug 30 2023 at 19:37):

In the first expression, I must use the multinomial theorem:

Simon Burton (Aug 30 2023 at 19:40):

image.png
This is the reference @Todd Trimble gave above. So now I'm thinking of $k[t]$ as "the walking endomorphism" ring...

Jean-Baptiste Vienney (Aug 30 2023 at 19:44):

Sorry, you can discuss. I still hope that that my infinite calculation can terminate (if ever)

Todd Trimble (Aug 30 2023 at 19:45):

Jean-Baptiste Vienney said:

I prefer if there is no use of something like the Cramer's rule and if it follows from a direct computation by applying the definitions (that's probably a matter of taste). But I can't guarantee that it is not going to take me the whole day -- if it works.

With regard to Cramer's rule: it's an easy consequence of the fact that the determinant is an alternating multilinear map $V^n = V \times \ldots \times V \to k$. In other words, a direct computation by applying the definition of determinant.

But the only reason for mentioning it is that it leads directly to the adjugate matrix of a matrix $A$, viz. a matrix $\widetilde{A}$ such that $A \widetilde{A} = \widetilde{A} A = \det(A) \cdot I$. The presence of such a matrix $\widetilde{A}$ is the key thing used in the nLab to prove Cayley-Hamilton, which has a nice short conceptual proof (essentially the same proof as in Lang's Algebra, if I remember correctly).

Jean-Baptiste Vienney (Aug 30 2023 at 19:51):

It looks more intelligent. I'm still intrigued to know if my brute-force calculation can finish

Todd Trimble (Aug 30 2023 at 19:55):

I'm all for experimentation, but I think it would be better to work these things out by yourself and not go through a long public calculation. I think the main problem may be that not many people here would be willing to read through all of it, and besides, people were beginning to have a conversation about Nakayama's lemma.

Jean-Baptiste Vienney (Aug 30 2023 at 19:56):

Mhh I agree

Jean-Baptiste Vienney (Aug 30 2023 at 19:57):

I'll try to finish this outside of this conversation

Jean-Baptiste Vienney (Aug 30 2023 at 20:05):

Sorry for the spam with gigantic tensors

Patrick Nicodemus (Aug 30 2023 at 20:12):

Paul Garrett has a proof of Cayley Hamilton at the end of his algebra book which I find pretty interesting.

James Deikun (Aug 30 2023 at 20:14):

Is there any good proof that doesn't make use of adjugates?

Jean-Baptiste Vienney (Aug 30 2023 at 20:17):

Patrick Nicodemus said:

Paul Garrett has a proof of Cayley Hamilton at the end of his algebra book which I find pretty interesting.

I think I would like it because he uses exterior powers, the adjugate, but with an endomorphism and not a matrix, and also modules over $k[x]$ like mentionned above

Patrick Nicodemus (Aug 30 2023 at 20:20):

James Deikun said:

Is there any good proof that doesn't make use of adjugates?

Adjugates can be motivated pretty well from a more abstract algebraic point of view, they don't have to be defined purely in terms of some formula that acts on a matrix. I can elaborate on this

Jean-Baptiste Vienney (Aug 30 2023 at 20:21):

Can you say more?

Todd Trimble (Aug 30 2023 at 20:26):

James Deikun said:

Is there any good proof that doesn't make use of adjugates?

There's a kind of "dirty" proof where one sees that diagonal matrices $D$ solve the characteristic polynomial equation (since $p(D)$ for a polynomial $p$ is a diagonal matrix whose diagonal entries are $p(d_i)$, where $d_i$ are the entries for $D$). Since the determinant is invariant under conjugation, we can then extend Cayley-Hamilton to the set of all diagonalizable matrices. Then, since diagonalizable matrices are dense in the set of all matrices, and since the set of matrices that satisfy CH is a closed set (even in the Zariski topology), the Cayley-Hamilton holds for all matrices.

One has to think a bit carefully though how well this holds up for all commutative rings. I'm not sure that density assertion does.

Todd Trimble (Aug 30 2023 at 20:53):

Ack, diagonalizable matrices are not dense of course. I guess I had in mind the classical case where the commutative ring is a field, and apply the idea that the statement of CH is insensitive to whether we stick with that field or pass to an extension field, and use this to pass to an algebraic closure and argue there. So, yeah, it's looking dirtier by the moment.

Patrick Nicodemus (Aug 30 2023 at 21:50):

I consider free modules of finite rank over a given ring $R$.

Fix a rank 1 free module $A$ (not necessarily with a given choice of isomorphism with $R$) and let $(-) ^\ast$ abbreviate the functor $Hom(-, A)$.
A perfect pairing $V\otimes W\to A$ is a map such that both ways of currying give isomorphisms, so $V\cong W^\ast$ and $W\cong V^\ast$.
For any perfect pairing $\sigma:V\cong W^\ast$, and for $T$ an endomorphism of $V$, construct a map

$(\sigma T\sigma^{-1})^{\ast} :W^{\ast\ast} \to W^{\ast\ast}$
and by virtue of the natural isomorphism $W\cong W^{\ast\ast}$ i can regard this as a map $T^\sharp:W\to W$.

This map is called the adjoint of $T$ and is uniquely defined by $\left\langle Tv, w\right\rangle=\left\langle v, T^\sharp w\right\rangle$. Similarly if $F$ is an endomorphism of $W$ its adjoint is an endomorphism of $V$.

Now take $V$ to be a free module of rank $n$, let $W=\Lambda^{n-1}(V)$
and take $A$ to be $\Lambda^{n}(V)$. The wedge product is a perfect pairing.

If $T$ is any endomorphism of $V$ then because the exterior algebra is a functor $F=\Lambda^{n-1}(T)$ is an endomorphism of $W=\Lambda^{n-1}(V)$. So it has an adjoint $F^\sharp$ which is an endomorphism of $V$. I call this endomorphism the adjugate of $T$.

Its defining property is that it satisfies
$F^\sharp(v) \land v_2\land \dots\land v_n=v\land T(v_2)\land\dots\land T(v_n)$.

For any basis of $V$ there are standard bases for $W$ and $A$. Moreover as soon as a basis is fixed $V$ is isomorphic to its dual space and so are $W$ and $A$. I can describe the computation of the matrices arising from these but it will be a bit tedious, i will leave it as an exercise

Patrick Nicodemus (Aug 30 2023 at 21:55):

it's helpful here to know that if $T$ is an endomorphism of $V$ then its determinant can be defined as the unique scalar $r$ in $R$ such that $\Lambda^n(T)$ is equal to $r\cdot -$ as endomorphisms of $\Lambda^n(V)$.

Patrick Nicodemus (Aug 30 2023 at 21:55):

that's why the adjugate is closely connected to the determinant.

James Deikun (Aug 30 2023 at 21:58):

From this perspective is there a way to make the adjugate still work for modules that are not free? Apparently the Cayley-Hamilton theorem itself still works in this situation, just as long as the ring is commutative.

James Deikun (Aug 30 2023 at 21:59):

(This is much nicer than picking a basis and manipulating a bunch of formulas though.)

Patrick Nicodemus (Aug 30 2023 at 22:04):

i don't know of a reformulation of the proof where you get it for free but it's a corollary. If $M$ is fg take a surjection $\phi:R^n\to M$, then $T:M\to M$ lifts to $T':R^n\to R^n$ such that the square commutes. then you apply the theorem to $T'$ and use this to get it for $T$

John Baez (Aug 30 2023 at 22:29):

Todd Trimble said:

There's a kind of "dirty" proof where one sees that diagonal matrices $D$ solve the characteristic polynomial equation (since $p(D)$ for a polynomial $p$ is a diagonal matrix whose diagonal entries are $p(d_i)$, where $d_i$ are the entries for $D$). Since the determinant is invariant under conjugation, we can then extend Cayley-Hamilton to the set of all diagonalizable matrices. Then, since diagonalizable matrices are dense in the set of all matrices, and since the set of matrices that satisfy CH is a closed set (even in the Zariski topology), the Cayley-Hamilton holds for all matrices.

I kind of like dirty arguments where you prove something on a dense set and then use continuity to handle the rest. Maybe it's my background in analysis: these arguments come very naturally to me. For example, that's one of my favorite proofs of

$\exp(\mathrm{tr}(A)) = \det(\exp(A))$

But you know this better than anyone, Todd - in our recent work I've been reaching for Zariski density arguments like a drunk reaches for his bottle. :upside_down:

John Baez (Aug 30 2023 at 22:33):

I do however agree that there's something unsatisfying about proving an equation between algebraic functions by proving it at just enough points to let a density argument do the rest: in doing so one may be missing the deeper insights required to prove it more directly.

David Michael Roberts (Aug 31 2023 at 02:06):

Todd Trimble said:

Ack, diagonalizable matrices are not dense of course. I guess I had in mind the classical case where the commutative ring is a field, and apply the idea that the statement of CH is insensitive to whether we stick with that field or pass to an extension field, and use this to pass to an algebraic closure and argue there. So, yeah, it's looking dirtier by the moment.

I'm wondering if there is an analogue of Smith normal form/Jordan canonical form for say PID entries (not like SNF, where you can pick different bases on either side, though), and then prove Cayley–Hamilton for that special form.

David Michael Roberts (Aug 31 2023 at 02:07):

Or even just the pedestrian step of reducing to the case from a block diagonal matrix to the blocks separately, and then thinking about what happens with a single Jordan block, say (or the analogue not over a field).

David Michael Roberts (Aug 31 2023 at 02:11):

Obviously when working over a more general commutative ring you almost surely have problems in finding invariant submodules and more options for what submodules can be. Checking now, I see that "hereditary" rings are those where submodules of free modules are projective, so things can get pretty weird, and this is probably not a path all the way to a general proof.

James Deikun (Aug 31 2023 at 06:27):

In general I don't find any of the proofs of Cayley-Hamilton very conceptual, and none of them seem to prove it in the full generality where it holds. In particular, any proof based on the adjugate doesn't seem like it would work for the case of quaternionic or split-quaternionic matrices. (How do you actually define determinant of quaternionic matrices anyway, BTW?)

John Baez (Aug 31 2023 at 07:58):

Does Cayley-Hamilton even hold for quaternionic matrices?

I don't think there's a quaternion-valued determinant of quaternionic matrices obeying det(gh) = det(g) det(h). (It would take more conditions to turn this thought into a theorem.)

The good determinants for quaternionic matrices are the Dieudonne determinant and the Study determinant, which works out to be the square of the Dieudonne determinant. I wrote a bunch about these for the nLab.

John Baez (Aug 31 2023 at 07:59):

The Dieudonne determinant is an idea that works for matrices valued in any division ring.

James Deikun (Aug 31 2023 at 11:42):

According to https://www.sciencedirect.com/science/article/pii/0024379595005439 it's a little more complicated than the paradigm case; the "characteristic polynomial" here detects right eigenvalues ($Ax = x\lambda$) and is obtained by intervening in the process of obtaining the Study determinant by doing the $I\lambda - A$ manipulation just before taking the complex determinant. It is a polynomial of degree $2n$ with real coefficients, and its complex roots come in conjugate pairs, even the real ones, corresponding to $n$ "conjugate 3-spheres" of right eigenvalues, counting multiplicity. As a real polynomial, it is pretty clear how to evaluate it even on a quaternionic matrix and the evaluation on $A$ turns out to be 0.

Patrick Nicodemus (Aug 31 2023 at 11:47):

@Jean-Baptiste Vienney pinging you as you requested this longer explanation.

James Deikun (Aug 31 2023 at 12:49):

Garibaldi in https://arxiv.org/pdf/math/0203276.pdf constructs the characteristic polynomial as basically the "stable minimal polynomial", encoding the linear dependencies among powers of $A$ that are not "coincidental". In this setting Cayley-Hamilton is basically trivial; the interesting thing is proving that the characteristic polynomial detects eigenvalues and obeys the conventional formula.

Aaron David Fairbanks (Sep 01 2023 at 03:12):

Here are string diagrams based on @Patrick Nicodemus's description of adjugates, in case this helps anyone else too.
adj1.png
adj2.png
adj3.png

Jean-Baptiste Vienney (Sep 01 2023 at 03:43):

Lovely! We can easily draw the identity defining the characteristic polynomial by an equality between 2 string diagrams too. $p(\lambda) = det(\lambda.1_E - u)$ so $p(\lambda)$ is the unique scalar such that:
$\Lambda^n(\lambda.1_E - u) = p(\lambda). 1_{\Lambda^n(E)}$

Jean-Baptiste Vienney (Sep 01 2023 at 03:44):

Now, I'm wondering how you can draw the identity which is named "Cayley-Hamilton theorem"

Jean-Baptiste Vienney (Sep 01 2023 at 03:45):

And if we can somehow draw the proof with equalities of string diagrams

James Deikun (Sep 02 2023 at 04:16):

From the above-referenced Garibaldi:

Let $a_1, . . . , a_m$ be an $F$ -basis for $A$. Let $R = F [t_1, . . . , t_m]$ for $t_1, . . . , t_m$ (commuting) indeterminates, and let $K$ be the quotient field of $R$. We call $γ = \sum_i t_i a_i \in A \otimes_F K$ a generic element. The $K$-span of $1, γ, γ^2, . . .$ is a subspace of $A \otimes K$, so it must be finite-dimensional over $K$. Hence there is a nonzero monic polynomial $\mathrm{min. poly.}_{γ/K}$ in $K[x]$ of smallest degree such that $\mathrm{min. poly.}_{γ/K} (γ) = 0$, called the minimal polynomial for $γ$ over $K$.

I like his general approach but I would really like it better if things like this were manifestly basis-independent ... I don't really know how to make a generic element of $A$ in a basis-independent way, when $A$ is a general associative algebra, though, much less one that will actually work in this kind of construction ...

John Baez (Sep 02 2023 at 09:47):

What's $A$? A free $F$-module? Is $F$ a field here?

James Deikun (Sep 02 2023 at 11:26):

$A$ is an $F$-algebra, and $F$ is a field; he says most of this also works for $F$ a commutative ring, though quite some of his proofs would need to be revised.

James Deikun (Sep 02 2023 at 11:44):

I guess the interesting fact that should prove the existence of the characteristic polynomial is that the power maps $-^k$ on $A$ generate a finite-dimensional subspace of $A[A]$ (the module of endomorphisms of $A$ as an affine scheme) as a module over the coordinate ring $F[A]$ of $A$ when $A$ is finitely generated. But I'm not sure how to prove that; proving it by pigeonholing as above only works for individual points and then you have to do a bunch of other proofs to show the points act coherently together.

Patrick Nicodemus (Sep 02 2023 at 15:25):

I think that searching for basis-free proofs is great but I also think that at some point you will run up against the wall that if a theorem only holds for finite dimensional vector spaces or finitely generated modules you will inevitably run into a point in the proof that invokes that hypothesis in some way or another. Maybe you're looking for some kind of HoTT style proof where you assume the propositional truncation of "there exists a basis of length $n$", I have no idea what the theory of such "finite dimensional" vector spaces is.

James Deikun (Sep 02 2023 at 16:55):

Hm, actually I guess $A[A]$ is finitely generated over $F[A]$ when $A$ is finitely generated over $F$ ... so the same sort of counting argument does work after all. Proving that the coefficients are actually polynomials and not rational functions seems more difficult though ... makes me wonder if it's even true for general algebras $A$ when, e.g., $F$ is a non-noetherian commutative ring ...