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.

[Nailin Guan]

We settled the definition few days ago, here is an announce of our plan:
1: the definition is based on epsilon_1
2: since we need to deal with completion in ci ring, we found some missing instance about IsNoethrianRing and IsLocalRing, which is not very trivial, this might need a few PRs.
3: Koszul complex is being constructed using exterior power by @Wang Jingting
4: We need a corollary of Cohen Structure Theorem, which says any complete local ring is quotient of regular local ring, do anyone have suggestions about how to proceed? (This part haven't started yet)
Most of our work will be gathered into the following branch in the process
https://github.com/Thmoas-Guan/mathlib4_fork/tree/Complete-Intersection-Ring

[Nailin Guan]

We finished formalizing basic properties of complete intersection local ring. See our draft #34913, depending on some of our previous work on CM ring and regular local ring. The contents follows Commutative Ring Theory Matsumura
We are currently having some sorries in the following areas:
1: Koszul complex and cocomplex.
2: Noetherian/Local of adic completion
3: Cohen structure theorem.

[Nailin Guan]

I met some problems when formalizing Cohen Structure Theorem.
My current approach follows the proof in Stacks Project, if anyone have better idea please let me know, thanks.
The technical problems are two of its lemmas.
1: it is in lemma 10.159.1, for monogenic extension things are trivial, given (R,m,k), K an extension of k, it proceed by giving K a total order then do induction. Things work fine when x in K has predecessor, the problem is I need to take colimit when there isn't one, how should I state the induction hypothesis to make things work? Since I need the morphisms between previously constructed rings, but it involves the way we construct it.
2: for lemma 10.160.7, since I doesn't know in what degree formally smooth is developed, how should I proceed? (This seems to be a well known result used in many proofs I saw).

[Kevin Buzzard]

For 10.159.1 (link) just use Zorn's lemma (this would be valid in Lean, the set-theoretic objection which de Jong has is not a problem in Lean).

[Nailin Guan]

OK, thanks, I'll try to figure it out.

[Kevin Buzzard]

Let me run this through to check it's OK. For my own sanity let's restrict to the case where $R$ and $K$ are in the same universe Type u (you can probably reduce to this case by ULifting). Then the category is "large", so its objects are in Type u but the collection C of all of them has C : Type (u + 1). To apply Zorn to get a maximal element it will not be good enough to show that all chains indexed by J : Type u have an upper bound -- a counterexample would be the class of all ordinals: in set-theoretic speak, any set of ordinals has an upper bound (their union) but there is no largest ordinal. So one would have to allow chains indexed by J : Type (u + 1) and now the problem is that the limit is no longer in C. So I think I am going to have to retract my assertion :-/

[Junyan Xu]

The triples form a category which is not a preorder (there may be multiple morphisms between two objects), so Zorn's lemma isn't immediately applicable and you need categorical Zorn or follow what I did for algebraic closure.

For the transfinite recursion approach, for every element x in the well-ordered set, you need to construct a functor from Set.Iio x to the category of local rings with flat local ring maps, and you do this by induction on x. (You can state this using docs#DirectedSystem, no need of category theory.) You probably want to adjoin a top element to the well-ordered set like I do in #18067.

[Nailin Guan]

(moved)

[Nailin Guan]

Sorry that I haven't solve 10.159.1 yet, but I have in mind how to proceed, I'll try working on it anyway.

[Nailin Guan]

I currently opened some preliminary PRs:
#35337: span rank of M over local ring (R,m) is the dimension of M/mM over R/m
#35347: when ideal fg, adic completion is complete
#35348: span rank of maximal ideal of adic completion

[Nailin Guan]

The next step would be proving Noetherian, I currently follow lemma 10.97.5, however this involves associated graded ring (even though we have it in some PR, this might not be a good idea), any suggestions for this?

Furthermore is another problem here. I want to prove that for Noetherian local ring, dimension of its completion is equal to dimension of itself. I only know the proof via length of m^n/m^(n+1) (named Poincare series?), however this is not how we proceed in mathlib, how should I prove this in the current setup?

[Andrew Yang]

#34936 also proves that adic completion is complete.

[Nailin Guan]

Andrew Yang 发言道：

#34936 also proves that adic completion is complete.

Sorry for not finding it carfully. now what should we do?

[Andrew Yang]

The easiest way is probably if you can help review that PR and we can try to get that into mathlib soon.

[Andrew Yang]

And then you can PR the rest of your results.

[Nailin Guan]

I closed mine for now, most of our approach really over laps.

[Bingyu Xia]

Hi Nailin! I'm sorry that our work overlapped, please do review #34936 when you have a chance! Once that is merged, I’d look forward to seeing the rest of your results PR'd as Andrew mentioned

[Nailin Guan]

Bingyu Xia 发言道：

Hi Nailin! I'm sorry that our work overlapped, please do review #34936 when you have a chance! Once that is merged, I’d look forward to seeing the rest of your results PR'd as Andrew mentioned

There is nothing to be sorry about, since I didn't saw it. But sorry that I am currently busy working on Cohen structure theorem, I'll have a look when I have time.

[Nailin Guan]

Junyan Xu 发言道：

The triples form a category which is not a preorder (there may be multiple morphisms between two objects), so Zorn's lemma isn't immediately applicable and you need categorical Zorn or follow what I did for algebraic closure.

For the transfinite recursion approach, for every element x in the well-ordered set, you need to construct a functor from Set.Iio x to the category of local rings with flat local ring maps, and you do this by induction on x. (You can state this using docs#DirectedSystem, no need of category theory.) You probably want to adjoin a top element to the well-ordered set like I do in #18067.

The only two obstacles left are :
1: separable extension is formally etale hence formally smooth, the problem here is separable here needs to be possibly transcendental, so we may need to refactor IsSeparable?
2: The transfinite recrusion approach in 10.159.1 is still difficult to formalize, since it can do only the following work: we have a functor from Set.Iio x to some CommAlgCat R with flat morphisms and appropriate residue extension, then we can extend it to Set.Ico x. How should I proceed?

[Nailin Guan]

@Junyan Xu Where can I use the categorical Zorn you mentioned?
For the algebraic closure approach, do you mean by construct the corresponding type of ale_extension? Sorry that I didn't understand it very clearly, could you please explain a bit more? Thanks.

[Robin Carlier]

(deleted, misread the problem)

[Joël Riou]

I have not checked the details, but using a suitable category and a suitable SuccStruct the construction in these files may also be useful https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/SmallObject/Iteration/Basic.html https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.html

[Nailin Guan]

Thanks for the suggestion, however in this case, how to define succ might be a problem? Also, how can I make sure there is an element making it reach the whole field? I'll try to have some investigation on this.

[Nailin Guan]

Beside these, for the noetherianess of AdicCompletion, do anyone have idea other than using associated graded ring as in Stacks 05GH? If not, I have to dig out associated graded ring written long ago.

[Joël Riou]

Given a local ring R with residue field k, and an extension K/k, the rough idea would be to introduce a category of local flat R-algebras A equipped with an embedding of the residue field of A into K. The SuccStruct would take such an A, and do nothing when the residue field of A is already the whole K, and otherwise choose a : K not in the residue field of A, take a suitable localization of A[X] or A[X]/(P) depending on whether a is algebraic or not. If you iterate this over an infinite successor cardinal that is bigger than the cardinal of K, we should get an A whose residue field is K. (But as I said, this is only a sketch...)