SerreMultiplicityConjectures.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

7 declarations, 7 contain sorry, 0 declared as axioms

Serre's multiplicity conjectures

Let $R$ be a regular local ring and let $M$, $N$ be finitely generated $R$-modules such that $M \otimes_R N$ has finite length. Serre defined the intersection multiplicity $$\chi(M, N) = \sum_{i \ge 0} (-1)^i \ell_R(\operatorname{Tor}_i^R(M, N)).$$ He proved the dimension inequality $\dim M + \dim N \le \dim R$ for every regular local ring, and conjectured the following three properties:

Non-negativity: $\chi(M, N) \ge 0$.
Vanishing: if $\dim M + \dim N < \dim R$, then $\chi(M, N) = 0$.
Positivity: if $\dim M + \dim N = \dim R$, then $\chi(M, N) > 0$.

Serre proved all three when $R$ is of equal characteristic, or of mixed characteristic and unramified. Vanishing was proved in general by Roberts and, independently, by Gillet and Soulé. Non-negativity was proved in general by Gabber. Positivity is open in general. For Serre's two special cases, this file states only positivity, since non-negativity and vanishing are now known in general.

The intersection multiplicity is Module.intersectionMultiplicity, defined in FormalConjecturesForMathlib.RingTheory.IntersectionMultiplicity.

References:

Wikipedia
[Se00] J.-P. Serre, Local algebra, Springer Monographs in Mathematics, Springer, 2000, Chapter V, Part B.
[Ro85] P. Roberts, The vanishing of intersection multiplicities of perfect complexes, Bull. Amer. Math. Soc. 13 (1985), 127–130.
[GS87] H. Gillet, C. Soulé, Intersection theory using Adams operations, Invent. Math. 90 (1987), 243–277.
[Ro98] P. Roberts, Recent developments on Serre's multiplicity conjectures: Gabber's proof of the nonnegativity conjecture, Enseign. Math. 44 (1998), 305–324.
[Sk19] C. Skalit, Positivity of intersection multiplicity over a two-dimensional base, J. Pure Appl. Algebra 223 (2019), 1801–1816. arXiv:1510.05146

Imports (1)

FormalConjecturesUtil

theorem SerreMultiplicityConjectures.supportDim_add_supportDim_le_ringKrullDim Dimension inequality sorry line 75 source
Source documentation
Dimension inequality. Let $R$ be a regular local ring and let $M$, $N$ be finitely generated $R$-modules such that $M \otimes_R N$ has finite length. Then $\dim M + \dim N \le \dim R$. Proved by Serre for every regular local ring [Se00].

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, AddCommGroup, Module, Module.Finite, IsFiniteLength, TensorProduct, LE.le, WithBot, ENat, HAdd.hAdd, Module.supportDim, ringKrullDim
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem supportDim_add_supportDim_le_ringKrullDim (h : IsFiniteLength R (M ⊗[R] N)) :
    Module.supportDim R M + Module.supportDim R N ≤ ringKrullDim R := by
…
```
theorem SerreMultiplicityConjectures.intersectionMultiplicity_nonneg Non-negativity sorry line 85 source
Source documentation
Non-negativity. Let $R$ be a regular local ring and let $M$, $N$ be finitely generated $R$-modules such that $M \otimes_R N$ has finite length. Then $\chi(M, N) \ge 0$. Conjectured by Serre and proved by Gabber in 1995 [Ro98].

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, AddCommGroup, Module, Module.Finite, IsFiniteLength, TensorProduct, LE.le, Int, OfNat.ofNat, Module.intersectionMultiplicity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem intersectionMultiplicity_nonneg (h : IsFiniteLength R (M ⊗[R] N)) :
    0 ≤ intersectionMultiplicity R M N := by
…
```
theorem SerreMultiplicityConjectures.intersectionMultiplicity_eq_zero_of_lt Vanishing sorry line 96 source
Source documentation
Vanishing. Let $R$ be a regular local ring and let $M$, $N$ be finitely generated $R$-modules such that $M \otimes_R N$ has finite length. If $\dim M + \dim N < \dim R$, then $\chi(M, N) = 0$. Conjectured by Serre and proved by Roberts [Ro85] and, independently, by Gillet and Soulé [GS87].

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, AddCommGroup, Module, Module.Finite, IsFiniteLength, TensorProduct, LT.lt, WithBot, ENat, HAdd.hAdd, Module.supportDim, ringKrullDim, Eq, Int, Module.intersectionMultiplicity, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem intersectionMultiplicity_eq_zero_of_lt (h : IsFiniteLength R (M ⊗[R] N))
    (hdim : Module.supportDim R M + Module.supportDim R N < ringKrullDim R) :
    intersectionMultiplicity R M N = 0 := by
…
```
theorem SerreMultiplicityConjectures.intersectionMultiplicity_pos Positivity conjecture sorry line 110 source
Source documentation
Positivity conjecture. Let $R$ be a regular local ring and let $M$, $N$ be finitely generated $R$-modules such that $M \otimes_R N$ has finite length. If $\dim M + \dim N = \dim R$, then $\chi(M, N) > 0$.
The hypothesis on dimensions forces $M$ and $N$ to be nonzero, since the dimension of the zero module is $\bot$.

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, AddCommGroup, Module, Module.Finite, IsFiniteLength, TensorProduct, Eq, WithBot, ENat, HAdd.hAdd, Module.supportDim, ringKrullDim, LT.lt, Int, OfNat.ofNat, Module.intersectionMultiplicity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem intersectionMultiplicity_pos (h : IsFiniteLength R (M ⊗[R] N))
    (hdim : Module.supportDim R M + Module.supportDim R N = ringKrullDim R) :
    0 < intersectionMultiplicity R M N := by
…
```
theorem SerreMultiplicityConjectures.intersectionMultiplicity_pos_quotient Positivity conjecture, in the form stated on Wikipedia sorry line 121 source
Source documentation
Positivity conjecture, in the form stated on Wikipedia. Let $R$ be a regular local ring and let $P$, $Q$ be prime ideals of $R$ such that $R/P \otimes_R R/Q$ has finite length. If $\dim R/P + \dim R/Q = \dim R$, then $\chi(R/P, R/Q) > 0$.

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, Ideal, Ideal.IsPrime, IsFiniteLength, TensorProduct, HasQuotient.Quotient, Eq, WithBot, ENat, HAdd.hAdd, ringKrullDim, LT.lt, Int, OfNat.ofNat, Module.intersectionMultiplicity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem intersectionMultiplicity_pos_quotient (P Q : Ideal R) [P.IsPrime] [Q.IsPrime]
    (h : IsFiniteLength R ((R ⧸ P) ⊗[R] (R ⧸ Q)))
    (hdim : ringKrullDim (R ⧸ P) + ringKrullDim (R ⧸ Q) = ringKrullDim R) :
    0 < intersectionMultiplicity R (R ⧸ P) (R ⧸ Q) := by
…
```
theorem SerreMultiplicityConjectures.intersectionMultiplicity_pos_of_equalCharacteristic Serre proved the positivity conjecture when $R$ is of equal characteristic, that is, when $R$ contains a field [Se00] sorry line 132 source
Source documentation
Serre proved the positivity conjecture when $R$ is of equal characteristic, that is, when $R$ contains a field [Se00].

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, AddCommGroup, Module, Module.Finite, Field, Algebra, IsFiniteLength, TensorProduct, Eq, WithBot, ENat, HAdd.hAdd, Module.supportDim, ringKrullDim, LT.lt, Int, OfNat.ofNat, Module.intersectionMultiplicity
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem intersectionMultiplicity_pos_of_equalCharacteristic (k : Type*) [Field k] [Algebra k R]
    (h : IsFiniteLength R (M ⊗[R] N))
    (hdim : Module.supportDim R M + Module.supportDim R N = ringKrullDim R) :
    0 < intersectionMultiplicity R M N := by
…
```
theorem SerreMultiplicityConjectures.intersectionMultiplicity_pos_of_unramified Documented declaration: intersectionMultiplicity_pos_of_unramified sorry line 145 source
Source documentation
Serre proved the positivity conjecture when $R$ is of mixed characteristic and unramified, that is, when the characteristic $p$ of the residue field is not in the square of the maximal ideal of $R$ [Se00]. The hypothesis $p \notin \mathfrak m^2$ excludes $p = 0$ and the equal characteristic case, where $p = 0$ in $R$.

depends on sorry what this means
Statement uses: CommRing, IsRegularLocalRing, AddCommGroup, Module, Module.Finite, Nat, CharP, IsLocalRing.ResidueField, Not, Membership.mem, Ideal, HPow.hPow, IsLocalRing.maximalIdeal, OfNat.ofNat, IsFiniteLength, TensorProduct, Eq, WithBot, ENat, HAdd.hAdd and 5 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
62 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem intersectionMultiplicity_pos_of_unramified (p : ℕ) [CharP (ResidueField R) p]
    (hp : (p : R) ∉ maximalIdeal R ^ 2) (h : IsFiniteLength R (M ⊗[R] N))
    (hdim : Module.supportDim R M + Module.supportDim R N = ringKrullDim R) :
    0 < intersectionMultiplicity R M N := by
…
```