auslander_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result auslander_conjecture is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Auslander conjecture (1961): Every finite module over a Noetherian regular local ring with finite projective dimension has a resolution of length ≤ dim R. Proved for rings of dimension ≤ 2 and complete intersections. Open in general; related to the homological conjectures.

Why this node was retired

The posted statement is

import Mathlib

theorem auslander_conjecture (R : Type*) [CommRing R] [IsNoetherianRing R]
    (hlocal : ∃ m : Ideal R, m.IsMaximal ∧ ∀ I : Ideal R, I.IsMaximal → I = m) :
    (∀ M : ModuleCat R, Module.Free R M → Module.Finite R M →
      ∀ N : ModuleCat R, Module.Free R N → Module.Finite R N →
        True) → True := by
  sorry

The goal is an implication whose conclusion is True, closed by fun _ => trivial; its antecedent also ends in True, so it too is vacuous. The ring R, the locality hypothesis and the modules play no part.

What a faithful statement would require

The conclusion must state the vanishing condition on Ext (or the corresponding depth/rigidity property) that the conjecture is about.

No corrected replacement node exists yet.