All rings are assumed to be commutative with 1. We say a module over a ring is strictly noetherian if every nonempty set of submodules has a maximal member. We say a ring is strictly noetherian if it is strictly noetherian as a mododle over itself. Let M be a finite module over a strictly noetherian ring. Can we prove it is strictlty noetherian without using Axiom of Choice?

$\begingroup$ Do you really mean, "finite module?" $\endgroup$ – Noah Schweber Feb 26 '15 at 1:21

$\begingroup$ @NoahS It doesn't mean "finite cardinality", if that's what you're asking. en.wikipedia.org/wiki/Finitelygenerated_module $\endgroup$ – Todd Trimble♦ Feb 26 '15 at 1:45

1$\begingroup$ Ah, thank you, I'd actually never seen that usage before  I've always seen it spelled out. $\endgroup$ – Noah Schweber Feb 26 '15 at 2:31
Doesn't the standard proof work, simply replacing the word "ascending chain" by "maximal element" everywhere? Let $\mathcal{X}$ be a collection of submodules of $M$. Let $\phi: R^n \to M$ be a surjection (since $M$ is finitely generated). If $\phi^{1}(N)$ is maximal in $\phi^{1}(\mathcal{X})$ then $N$ is maximal in $\mathcal{X}$. So we are reduced to $M$ of the form $R^n$. Let $\mathcal{X}$ be a collection of submodules of $R^n$.
Now we work by induction on $n$. The base case $n=0$ is trivial.
Let $\pi : R^n \to R^{n1}$ be the projection that discards the first summand and let $\iota: R \to R^n$ be the inclusion of the first summand. By induction, there is some $C$ which is maximal in $\pi(\mathcal{X})$. Let $\mathcal{Y}$ be $\{ B \in \mathcal{X} : \pi(B) = C \}$. Let $\mathcal{Z} = \{ B \cap \iota(R ): B \in \mathcal{XY} \}$. Let $A$ be maximal in $\mathcal{Z}$, which exists by the Noetherian hypotheses. Let $B$ be in $\mathcal{Y}$ with $\iota(R ) \cap B = A$.
We claim that $B$ is maximal in $\mathcal{X}$. Suppose that $B' \in \mathcal{X}$ contains $B$. Then $\pi(B') \supseteq \pi(B)=C$ and, by maximality of $C$, we have $\pi(B') = C$. So $B' \in \mathcal{Y}$. Also, $B' \cap \iota(R ) \supseteq B \cap \iota(R )= A$ so, by maximality of $A$, we have $B' \cap \iota(R ) = A$.
So we have a commutative diagram with exact columns: $$\begin{matrix} 0 & & 0 \\ \downarrow & & \downarrow \\ A & = & A \\ \downarrow & & \downarrow \\ B & \subseteq & B' \\ \downarrow & & \downarrow \\ C & = & C \\ \downarrow & & \downarrow \\ 0& & 0 \\ \end{matrix}$$
So, by the snake lemma (or the five lemma, or whatever) the inclusion $B \subseteq B'$ is an equality.
In response to Noah S's challenge below, here is an explicit argument for the last bit. Let $b' \in B'$. Then $\pi(b') \in C = \pi(B)$, so there is a $b \in B$ with $\pi(b) = \pi(b')$. Since $\pi(b) = \pi(b')$, we have $bb' \in \mathrm{Ker}(\pi: B' \to C)$. So $b  b' \in A$. We have $b \in B$ and $bb' \in A \subset B$, so $b' \in B$.

$\begingroup$ Maybe I'm being silly, but is the snake lemma provable without some choice? $\endgroup$ – Noah Schweber Feb 26 '15 at 2:32

1$\begingroup$ Sure. Think of any proof you know, I bet it won't use choice. (Remember, you don't need choice to make finitely many choices.) $\endgroup$ – David E Speyer Feb 26 '15 at 2:37
