Complete Intersection Local Ring

Stream: mathlib4

[Nailin Guan]

Hello, we have a new plan about working on complete intersection ring, here is a small issue here about the definition. For a noetherian local ring R, there are two definitions we currently know.
First is purely self contained by defining \epsilon_1(R) as the dimension of H_1 of Koszul complex of a set of minimal generators of the unique maximal ideal over residue field, and define complete intersection as the ring making \epsilon_1(R) ≥ dimension of cotangent space - dim(R) is equality. The problem with this definition is that it is hard to use and we don't have Koszul complex...
The second is more straight forward, its completion is isomphic to quotient of a regular local ring by regular sequence, however the problem is how to arrange the data, I think either stated as exist such ring or make that ring just a part of the data isn't good enough.

[Nailin Guan]

By the way, with Cohen Macaulay ring developed, we are trying to work on Gorenstein ring. If we have a good definition of complete intersection, we are able to finish the chain of noetherian local ringregular local => complete intersection => Gorestein => Cohen Macaulay => universal catenary.