Serre's multiplicity conjectures

The question

intersectionMultiplicity_pos. 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 $\perp$.

intersectionMultiplicity_pos_quotient. 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$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.SerreMultiplicityConjectures (2 statements).

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

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)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

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

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.