(Lot and lot of) Context. I am preparing lecture notes for a course on modules I will teach next year, and I was hoping for finding a "not-too-complicated" proof of the fact that an ideal of an ring of integers $\mathcal{O}_K$ is projective ($K$ is a number field). It will be the very first course of module theory for the attending students, and I will only have few hours of lectures; in particular, I am not sure that I will have enough time to prove big theorems.
The only thing coming into mind is to prove that $I$ is locally free, even if I think it is rather complicated, because you need to prove that a finitely presented module is projective if and only if it is locally free, which takes a bit of time already, but anyway.
Of course, it boils down to prove that a local Dedekind domain is a PID. However, all proofs of this result I know are rather intricate. In particular, the use of the fact that $A$ is integrally is crucial, and arrives in the proof after lots of different subtle arguments (at least, a bit too subtle for beginners in module theory).
However, $\mathcal{O}_K$ has an extra feature that a general Dedekind ring does not have: its quotient rings are all finite (except if you take the quotient by the zero ideal).
So I wonder:
Question. Do you know a proof that a local Dedekind ring $A$ with maximal ideal $\mathfrak{m}$ and such that $A/\mathfrak{m}$ is finite is a PID, which is "simpler" that the general one. I will be already happy if $A$ is the localization of $\mathcal{O}_K$ at a maximal ideal.
For example, could we hope finding an argument by contradiction like, if $\mathfrak{m}$ is not principal then $A$ is not integrally closed ?
To precise what could be used in such a proof, if it does exist, the following results will be known:
the structure of finite fields
Local Nakayama lemma
A commutative ring $A$ is a PID if and only if it is an integral domain, Noetherian, and every maximal ideal is principal
the definition of a Dedekind ring, as an integrally closed Noetherian domain in which every nonzero prime ideal is maximal
the fact that $\mathcal{O}_K$ is a Dedekind ring, that every nonzero ideal is a free $\mathbb{Z}$-module of rank $[K:\mathbb{Q}]$ ,and that $\mathcal{O}_K/I$ is finite for any nonzero ideal $I$.
However, no theory of factorization of ideals will be known.
I have very few hope that we could cook such a proof, but I think it is worth asking anyway.