Auslander-Reiten conjecture

### What is the conjecture

An *Artin algebra* is a ring $\Lambda$ that is an algebra over a commutative Artinian ring and is
finitely generated as a module over it.

**Conjecture (Auslander-Reiten).** Let $\Lambda$ be an Artin algebra and $M$ a finitely generated
$\Lambda$-module with $\operatorname{Ext}^i_\Lambda(M, \Lambda) = 0$ and
$\operatorname{Ext}^i_\Lambda(M, M) = 0$ for all $i > 0$. Then $M$ is projective.

Auslander and Reiten derived this from the generalized Nakayama conjecture in 1975. The
commutative version, with $\Lambda$ replaced by a commutative Noetherian ring $R$, is what the
commutative algebra literature calls the Auslander-Reiten conjecture; the two hypotheses there
read $\operatorname{Ext}^i_R(M, R \oplus M) = 0$ for all $i > 0$. The converse is elementary, so
the conjecture says that this Ext vanishing characterises the projective modules.

Both forms are open, the commutative one already for Noetherian local rings. Known cases of the
commutative version include: local complete intersections (Auslander-Ding-Solberg); locally
excellent Cohen-Macaulay normal rings containing $\mathbb Q$ (Huneke-Leuschke); Gorenstein normal
rings (Araya); Cohen-Macaulay normal rings (Kimura-Otake-Takahashi); and normal rings in general
(Kimura, 2023).

**Sources:**
- M. Auslander, I. Reiten, *On a generalized version of the Nakayama conjecture*, Proc. Amer.
Math. Soc. 52 (1975), 69-74:
https://www.ams.org/journals/proc/1975-052-01/S0002-9939-1975-0389977-6/S0002-9939-1975-0389977-6.pdf
- https://en.wikipedia.org/wiki/Nakayama_conjecture (the generalized Nakayama conjecture)
- K. Kimura, *Auslander-Reiten conjecture for normal rings*, https://arxiv.org/abs/2304.03956
(statement of the conjecture and a survey of known cases in the introduction)
- C. Huneke, G. J. Leuschke, *On a conjecture of Auslander and Reiten*, J. Algebra 275 (2004),
no. 2, 781-790: https://arxiv.org/abs/math/0305001
- T. Araya, *The Auslander-Reiten conjecture for Gorenstein rings*, Proc. Amer. Math. Soc. 137
(2009), no. 6, 1941-1944
- M. Auslander, S. Ding, Ø. Solberg, *Liftings and weak liftings of modules*, J. Algebra 156
(1993), 273-317

### Prerequisites needed

None beyond Mathlib: `CategoryTheory.Abelian.Ext` on `ModuleCat R` (with the
`HasExt` instance for module categories), `Module.Projective`, `Module.Free`, `IsArtinianRing`,
`IsNoetherianRing`, `IsIntegrallyClosed` and `IsRegularLocalRing` all exist.

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

* ams-13
* ams-16
* ams-18

### 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 reading the stated prerequisites in CategoryTheory.Abelian.Ext and the listed module-theory interfaces, including Module.Projective, Module.Free, IsArtinianRing, IsNoetherianRing, IsIntegrallyClosed, and IsRegularLocalRing. Determine the repository entry point for conjecture statements and formalize the Auslander-Reiten conjecture there, with the completed statement typechecking in Lean.

Written by the indexing model from the issue text.