Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’d like to tentatively suggest replacing the current statement of Nakayama’s lemma on the relevant page with the following (non-local) version:
Nakayama’s lemma (proposed version): Let be a commutative ring and be a finitely generated -module. Then:
.
If moreover is an ideal with inhabited, then is nonzero.
(Recall that , , and . The first claim is not usually considered part of Nakayama’s lemma but will be useful here and can be proved with a closely related argument to that which we will use for the main result.)
The proof uses relatively little pre-existing commutative algebraic theory (i.e., just some basic facts about , nonzeroness in short exact sequences, localization, tensoring, and localizing/tensoring cyclic modules) as follows:
Proof of Nakayama’s lemma: The argument proceeds in the following four steps:
As is finitely generated, it admits a filtration with cyclic cokernels. To be explicit, if the -tuple of elements generates , then it begets an -tuple of short exact sequences
where is the submodule of spanned by and in particular and . (Here the maps are the evident inclusions; as the cokernel is generated by the image of , it is in particular isomorphic to for some ideal .) The basic idea is that the process of extension by which is built up from these s interacts sufficiently nicely with the operations of localization/taking fibers that the properties of the latter determine those of the former.
For instance, it is clear that any must descend to on all the s; on the other hand, for all we have that . We conclude that , whence .
Let us now show that ; this will complete the proof of our first claim. Recall that for any the functor is exact; we therefore in any case obtain an -tuple of short exact sequences
If , then each vanishes, so the above SESs collapse to isomorphisms
and thus
Conversely, if , then there is a maximal index such that and in particular an epimorphism
with nonzero. But there are also, as before, isomorphisms
whence
is epic onto a nonzero module and thus itself nonzero.
The proof of the second claim is in the same vein, requiring just a little bit more delicacy. Suppose that inhabits ; by the above this means that and that there exists some index for which . Again consider the maximal index for which . As before, there is an epimorphism
and isomorphisms
By the right-exactness of the functor , we obtain from the former an epimorphism
(implicitly using that ). By its functoriality, there are likewise isomorphisms
Now,
is nonzero (here we use that ). It follows that
is epic onto a nonzero module and thus itself nonzero. But
(here we use that ), so the latter must itself be nonzero, as claimed.
It is now straightforward to recover more familiar forms of Nakayama’s lemma as a corollary of the above. For instance, the nLab’s current version states:
Nakayama’s lemma (nLab’s version): Let be a local ring with maximal ideal and be a finitely generated -module. Then if is nonzero, so too is .
Indeed, is practically tautologically in (and so practically tautologically intersects) the support of any nonzero -module; the conditions of our version of the lemma apply, and we conclude that is nonzero as advertised.
Sometimes (for instance in the Stacks Project), Nakayama’s lemma is stated instead as follows:
Nakayama’s lemma (Stacks Project’s version): Let be a commutative ring, be a finitely generated -module, and be an ideal with . Then there exists such that and .
Of course, ; it follows from our version of the lemma that is comaximal with . The Chinese Remainder theorem then asserts the existence of such that and ; the desired .
(I could not find a discussion page linked to the Nakayama’s Lemma entry; I’m not sure if this is the proper way to discuss pages without linked nForum threads. Please advise if not!)
Thanks for this, this looks like great material. I think you should feel invited to add this to the entry.
(The dedicated discussion page for the entry will appear once you make the first edit there, together with a log-message. The page has probably been created so long ago (and left essentially untouched since) that it was before this announcement mechanism was in place.)
I would be glad that you add this to the entry, because it looks very helpful to me, especially the clear and detailled proof.
I agree, very nice, and I wonder what a constructive version of statement 2 looks like. If I should venture a guess, it would be:
If is zero, then the geometric theory of a prime filter with for proves, for every , that .
I arrived at this formulation as follows. First let’s take the original formulation:
(1) If is inhabited, then is nonzero.
This looks like the contrapositive of a more direct statement:
(2) If is zero, then .
The set is the set of models of a geometric theory, and also is; but is not. So let’s rewrite as follows:
(3) If is zero, then .
The inclusion states that all models of the first geometric theory are also models of the second. So let’s do the leap to the theories themselves instead of their models (equivalently, referring to models in all toposes, not just the standard topos). In this way we arrive at the proposed constructivization.
To check that the proposed constructivization is indeed constructively provable, we can either appeal to Barr’s theorem or use the direct description of provability modulo the theory of prime filters. I’m guessing that I’m talking mostly to myself right now, thank you for the nice nudge, but if anyone wants details I’m happy to fill them in. :-)
In modern algebra, Nakayama’s lemma is often presented in generality of noncommutative rings. See for example http://alpha.math.uga.edu/~pete/noncommutativealgebra.pdf.
I have now merged the contribution from #1 into the entry Nakayama’s lemma (as announced there).
1 to 7 of 7