AuslanderReiten.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 5 contain sorry, 0 declared as axioms

The Auslander-Reiten conjecture

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

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

Auslander and Reiten [AR75] derived this from the generalized Nakayama conjecture. The commutative version, obtained by replacing $\Lambda$ with a commutative Noetherian ring $R$, is also open and is what the commutative algebra literature calls the Auslander-Reiten conjecture. The two hypotheses are together equivalent to $\operatorname{Ext}^i_R(M, R \oplus M) = 0$ for all $i > 0$.

Known cases of the commutative version include: $R$ a locally excellent Cohen-Macaulay normal ring containing $\mathbb Q$ [HL04]; $R$ a Gorenstein normal ring [Ar09]; $R$ a Cohen-Macaulay normal ring [KOT22]; and, most generally, $R$ any normal ring [Ki23]. Auslander, Ding and Solberg [ADS93] proved it for local complete intersections. The conjecture is open in general, already for commutative Noetherian local rings.

References:

[AR75] M. Auslander, I. Reiten, On a generalized version of the Nakayama conjecture, Proc. Amer. Math. Soc. 52 (1975), 69-74. PDF
Wikipedia, Nakayama conjecture, on the generalized Nakayama conjecture of [AR75].
[ADS93] M. Auslander, S. Ding, Ø. Solberg, Liftings and weak liftings of modules, J. Algebra 156 (1993), 273-317.
[HL04] C. Huneke, G. J. Leuschke, On a conjecture of Auslander and Reiten, J. Algebra 275 (2004), no. 2, 781-790. arXiv:math/0305001
[Ar09] T. Araya, The Auslander-Reiten conjecture for Gorenstein rings, Proc. Amer. Math. Soc. 137 (2009), 1941-1944.
[KOT22] K. Kimura, Y. Otake, R. Takahashi, Maximal Cohen-Macaulay tensor products and vanishing of Ext modules, Bull. Lond. Math. Soc. 54 (2022), no. 6, 2456-2468.
[Ki23] K. Kimura, Auslander-Reiten conjecture for normal rings, arXiv:2304.03956. The statements of the conjecture formalised below follow this paper.

Imports (1)

FormalConjecturesUtil

theorem AuslanderReiten.subsingleton_ext_of_projective The converse of the conjecture is elementary: over any ring, all higher Ext out of a projective module vanish line 79 source
Source documentation
The converse of the conjecture is elementary: over any ring, all higher Ext out of a projective module vanish. So the conjecture says that its two Ext vanishing hypotheses characterise the projective modules.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, AddCommGroup, Module, Module.Projective, ModuleCat, Nat, Subsingleton, CategoryTheory.Abelian.Ext, Int, ModuleCat.of, HAdd.hAdd, OfNat.ofNat
Proof uses: CategoryTheory.Abelian.Ext.subsingleton_of_projective
18 instances, coercions and auxiliary constants left out.
```
theorem subsingleton_ext_of_projective [Module.Projective Λ M] (N : ModuleCat.{u} Λ) (i : ℕ) :
    Subsingleton (Abelian.Ext (ModuleCat.of Λ M) N (i + 1)) :=
…
```
theorem AuslanderReiten.auslander_reiten The Auslander-Reiten conjecture [AR75] sorry line 98 source
Source documentation
The Auslander-Reiten conjecture [AR75]. 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.
That $\Lambda$ is an Artin algebra is the hypothesis that it is an algebra over some commutative Artinian ring A and is finitely generated as an A-module.

depends on sorry what this means
Statement uses: Ring, AddCommGroup, Module, Module.Finite, CommRing, IsArtinianRing, Algebra, Nat, GT.gt, OfNat.ofNat, Subsingleton, CategoryTheory.Abelian.Ext, ModuleCat, Int, ModuleCat.of, Module.Projective
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem auslander_reiten (A : Type u) [CommRing A] [IsArtinianRing A] [Algebra A Λ]
    [Module.Finite A Λ]
    (hMΛ : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of Λ M) (ModuleCat.of Λ Λ) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of Λ M) (ModuleCat.of Λ M) i)) :
    Module.Projective Λ M := by
…
```
theorem AuslanderReiten.auslander_reiten.variants.commutative The Auslander-Reiten conjecture for commutative Noetherian rings [Ki23] sorry line 118 source
Source documentation
The Auslander-Reiten conjecture for commutative Noetherian rings [Ki23]. If $R$ is a commutative Noetherian ring and $M$ is a finitely generated $R$-module with $\operatorname{Ext}^i_R(M, R \oplus M) = 0$ for all $i > 0$, then $M$ is projective.

depends on sorry what this means
Statement uses: CommRing, IsNoetherianRing, AddCommGroup, Module, Module.Finite, Nat, GT.gt, OfNat.ofNat, Subsingleton, CategoryTheory.Abelian.Ext, ModuleCat, Int, ModuleCat.of, Module.Projective
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem auslander_reiten.variants.commutative
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R M) i)) :
    Module.Projective R M := by
…
```
theorem AuslanderReiten.auslander_reiten.variants.local_free Over a Noetherian local ring a finitely generated projective module is free, so the conjecture takes the following form there sorry line 129 source
Source documentation
Over a Noetherian local ring a finitely generated projective module is free, so the conjecture takes the following form there. It is open in this case too.

depends on sorry what this means
Statement uses: CommRing, IsNoetherianRing, AddCommGroup, Module, Module.Finite, IsLocalRing, Nat, GT.gt, OfNat.ofNat, Subsingleton, CategoryTheory.Abelian.Ext, ModuleCat, Int, ModuleCat.of, Module.Free
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem auslander_reiten.variants.local_free [IsLocalRing R]
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R M) i)) :
    Module.Free R M := by
…
```
theorem AuslanderReiten.auslander_reiten.variants.normal The conjecture holds for normal rings [Ki23, Corollary 1.2] sorry line 141 source
Source documentation
The conjecture holds for normal rings [Ki23, Corollary 1.2]. Stated here for normal domains, since Mathlib does not currently have a standalone class for normal rings, which are the rings whose localizations at all primes are normal domains.

depends on sorry what this means
Statement uses: CommRing, IsNoetherianRing, AddCommGroup, Module, Module.Finite, IsDomain, IsIntegrallyClosed, Nat, GT.gt, OfNat.ofNat, Subsingleton, CategoryTheory.Abelian.Ext, ModuleCat, Int, ModuleCat.of, Module.Projective
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem auslander_reiten.variants.normal [IsDomain R] [IsIntegrallyClosed R]
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i))
    (hMM : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R M) i)) :
    Module.Projective R M := by
…
```
theorem AuslanderReiten.auslander_reiten.variants.regular_local Over a regular local ring the conjecture is standard: every finitely generated module has finite projective dimension $p$, and if $p > 0$ then $\operatorname{Ext}^p_R(M, R) \ne 0$ sorry line 154 source
Source documentation
Over a regular local ring the conjecture is standard: every finitely generated module has finite projective dimension $p$, and if $p > 0$ then $\operatorname{Ext}^p_R(M, R) \ne 0$. Only the vanishing of $\operatorname{Ext}^i_R(M, R)$ is used, and the conclusion is freeness.

depends on sorry what this means
Statement uses: CommRing, AddCommGroup, Module, Module.Finite, IsRegularLocalRing, Nat, GT.gt, OfNat.ofNat, Subsingleton, CategoryTheory.Abelian.Ext, ModuleCat, Int, ModuleCat.of, Module.Free
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem auslander_reiten.variants.regular_local [IsRegularLocalRing R]
    (hMR : ∀ i > 0, Subsingleton (Abelian.Ext (ModuleCat.of R M) (ModuleCat.of R R) i)) :
    Module.Free R M := by
…
```