Small Cohen-Macaulay modules conjecture (Hochster)

### What is the conjecture

Let $(R, \mathfrak m)$ be a Noetherian local ring of Krull dimension $d$. A *system of parameters*
is a sequence $x_1, \dots, x_d$ of elements of $R$ with $\sqrt{(x_1, \dots, x_d)} = \mathfrak m$.
A *small* (or maximal) *Cohen-Macaulay module* is a finitely generated $R$-module $M \ne 0$ such
that some system of parameters is a regular sequence on $M$.

**Conjecture.** If $R$ is complete, then $R$ has a small Cohen-Macaulay module.

This is conjecture 14 in the Wikipedia list of homological conjectures. Hochster conjectured it
for complete local domains in the early 1970s (Conjecture 2.1 of his survey below), and in the
2000s conjectured the opposite, that there are complete local domains with no small
Cohen-Macaulay module (Conjecture 2.2): "one of these conjectures is bound to be correct".

Small Cohen-Macaulay modules are known to exist when $\dim R \le 2$, and in the
$\mathbb N$-graded characteristic $p$ case with an isolated non-Cohen-Macaulay point at the
origin. The question is open in Krull dimension $\ge 3$ in every characteristic. Balanced big
Cohen-Macaulay modules, by contrast, are now known to exist over every Noetherian local ring
(Hochster in equal characteristic, André in mixed characteristic), which is conjecture 8 of the
same list.

**Sources:**
- https://en.wikipedia.org/wiki/Homological_conjectures_in_commutative_algebra (conjectures 8 and 14)
- M. Hochster, *Homological conjectures and lim Cohen-Macaulay sequences*, Springer INdAM Ser. 20,
2017: https://sites.lsa.umich.edu/hochster/wp-content/uploads/sites/1337/2024/08/DSlim2.pdf
- M. Hochster, *Topics in the homological theory of modules over commutative rings*, CBMS 24, 1975
- K. Shimomoto, E. Tavanfar, *Remarks on the Small Cohen-Macaulay conjecture and new instances of
maximal Cohen-Macaulay modules*, J. Algebra 634 (2023), 667-697, https://arxiv.org/abs/2203.10368
- B. Bhatt, *On the non-existence of small Cohen-Macaulay algebras*, J. Algebra 411 (2014), 1-11

### Prerequisites needed

Mathlib has regular sequences (`RingTheory.Sequence.IsRegular`), `ringKrullDim` and adic
completeness, but no systems of parameters and no Cohen-Macaulay modules, so those definitions
have to be added. Systems of parameters are also a prerequisite of the monomial conjecture, #1807.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-13

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reviewing Mathlib's RingTheory.Sequence.IsRegular, ringKrullDim, and adic completeness support. Define systems of parameters and small Cohen–Macaulay modules, then state the conjecture for complete Noetherian local rings; done means the definitions and conjecture compile with appropriate basic properties or examples.

Written by the indexing model from the issue text.