OAI.Lech.dutta_domain

The theorem states that the defined proposition DuttaDomainClaim holds, in universe u. That claim says: let D be a commutative Noetherian local domain (in universe u) that is complete in the adic topology of its maximal ideal, with prime characteristic p, and let F be a cochain complex of D-modules indexed by the integers that is a short complex. Short means every term F^i is free and finitely generated, F^i is zero whenever i < -dim D or i > 0, every homology module of F has finite length, and the homology of F in degree 0 is nonzero. Here dim is the Krull dimension (taken as 0 if it is the bottom value). Let F_n denote F after extending scalars along the n-fold iterate of the Frobenius map of D. The conclusion has three parts. First, every homology module of every F_n has finite length. Second, the sequence a_n = p^(-n dim D) * chi(F_n) converges as n tends to infinity, where chi(G) is the alternating sum, over i from 0 to dim D, of (-1)^i times the length of the homology of G in degree -i; this limit is the Dutta multiplicity of F. Third, the Hilbert-Samuel multiplicity of D, defined as the limit of (dim D)! times the length of D/m^N divided by N^(dim D) as N tends to infinity, is at most the Dutta multiplicity of F. The statement is admitted in Lean without a proof (sorry).