Cohen Macaulay rings

Stream: mathlib4

[Nailin Guan]

This thread is for the announce that we have a project trying to develope Cohen-Macaulay rings in https://github.com/xyzw12345/CohenMacaulay and keep track of it for later developements.
Currently we are proving the equivalence of the vanishing order of Ext functor and length of regular squence. The first stage goal is the rees theorem (Matsumura Commutative Algebra Chapter 6 Theorem 28)

[Nailin Guan]

Currently, the repo is a bit messy and quite a few lemmas needed are in open PRs, so the porting from the repo to the branches of mathlib may take some time.

[Kevin Buzzard]

This is great news! Will you also think about Gorenstein and complete intersection rings? These three definitions in commutative ring theory will really demonstrate that we have become a big player in commutative algebra.

[Nailin Guan]

These are our current works stopping at the Rees theorem.
#23877 and #23935 probably need some break down.
8f4256d8c45b7c28b4270a88e53d1e9.jpg

[Nailin Guan]

Further developements would be:
1 : the definition of depth
2 : depth \le dim (Matsumura Commutative Algebra Chapter 6 Theorem 29)

[Nailin Guan]

Kevin Buzzard said:

This is great news! Will you also think about Gorenstein and complete intersection rings? These three definitions in commutative ring theory will really demonstrate that we have become a big player in commutative algebra.

We currently don't have plans for them for now. As our proffessor is interested in PBW theorem and we would probably work on that in the near future. We can ask him whether if he is intersted in these rings :smile:

[Nailin Guan]

He said he is intersted, however we might not be able to work on it as we don't have enough people working on lean and other projects have existed as mentioned above.
Beside these, we currently don't have well-organized reference and blueprint for the formalizing of the two class of rings you mentioned, do you have ideas about that? Thank you.

[Kevin Buzzard]

I don't want to disrupt your plans! I was just asking to try and find out more about what they were

[Joël Riou]

These are nice results! I have added some comments about #23935.

[Joël Riou]

In general, I would suggest that instead of stating basic "diagram lemmas" about objects in ModuleCat, you phrase them in a general abelian category as much as possible, and as my comments on the PR show, most of these lemmas are already in mathlib. In order to state that an object in an abelian category is zero, the better phrasing is by using IsZero: to ease the relation between properties of types and properties of objects in ModuleCat (or AddCommGrp), it would be good to introduce some isZero_iff_subsingleton lemmas (I did not check if we had these already).

[Joël Riou]

Actually, we have isZero_of_subsingleton.

[Andrew Yang]

I think depth <= dim could be done separately? (If you use the regular sequence def) At least we have that in FLT already.

[Nailin Guan]

Joël Riou said:

In general, I would suggest that instead of stating basic "diagram lemmas" about objects in ModuleCat, you phrase them in a general abelian category as much as possible, and as my comments on the PR show, most of these lemmas are already in mathlib. In order to state that an object in an abelian category is zero, the better phrasing is by using IsZero: to ease the relation between properties of types and properties of objects in ModuleCat (or AddCommGrp), it would be good to introduce some isZero_iff_subsingleton lemmas (I did not check if we had these already).

isZero_of_subsingleton exists, but not the other side.

[Nailin Guan]

There are two supplementary PRs #23876 moving associated prime file into a folder and #23903 defining Submodule.submoduleOf, can anybody have a look so we can move on to the finiteness of associated primes.

[Jz Pan]

Do you have works on finiteness of associated primes? I think I probably duplicated this work in https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/RingTheory/CharacteristicIdeal/Basic.lean. (I'll need to use it very soon so I formalized it by myself.)

[Jz Pan]

Oh found it #23877. (I have a much shorter proof than yours :sunglasses:)

[Jz Pan]

Feel free to copy my proof if you think it's better.

[Nailin Guan]

This PR is a bit messy now, I'll try to clean it up when I have time (as there is still a mid-term test ...)
Maybe you can just help edit that PR (please feel free), or if the current dependency is not good enough you can just open another one and we base on that one.
This part is originally developed for using prime avoidance when proving the case depth = 0, so the overall impact should not be big.
The only thing I want to make sure is whether the by-products we get on the way are really useful?

[Nailin Guan]

I have a glance and discussed a little with @Wang Jingting(the author of our version), the conclusion is that we may try to "merge" your work into the current PR replacing the duplicated parts when we have time, as your proof is more succinct. Hopefully it should be done within this month.

[Jz Pan]

The proof is based on this result https://acmepjz.github.io/lean-iwasawa/blueprint/sect0002.html#noeth-ring-filtration which is in stacks https://stacks.math.columbia.edu/tag/00L0 and is formalized at https://acmepjz.github.io/lean-iwasawa/docs/Iwasawalib/RingTheory/CharacteristicIdeal/Basic.html#IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime. It gives an induction principle for modules #mathlib4 > How to write induction principle for modules , which implies the finiteness of associated primes.

Such induction principle also have other applications which I need to use later, for example in the proof of https://acmepjz.github.io/lean-iwasawa/blueprint/sect0003.html#char-ideal-preliminary.

[Nailin Guan]

I see, I think we are literally doing the same thing. Then the "merge" should focus on unifying the APIs. As we don't have much works based on the intermediate results, we would probably mainly use your APIs.

[Nailin Guan]

I have a more careful look and I think it no longer depend on the induction principle of relseries, so I would probably close the old one and only bring the useful things to the new one.

[Nailin Guan]

Here is a chunk of code that I don't know whether useful:

variable {R : Type u} [Ring R]

theorem fg_induction (P : ModuleCat.{v, u} R → Prop)
    (h_zero : ∀ (N : ModuleCat.{v, u} R), Subsingleton N → P N)
    (h_base : ∀ (N : ModuleCat.{v, u} R), (⊤ : Submodule R N).IsPrincipal → P N)
    (h_ext : ∀ (M : ModuleCat.{v, u} R), ∀ (N : Submodule R M),
      P (ModuleCat.of R N) → P (ModuleCat.of R (M ⧸ N)) → P M)
    (M : ModuleCat.{v, u} R) (hM : Module.Finite R M) : P M := by
  sorry

-- [Stacks 00KZ]
theorem exists_LTSeries_quotient_cyclic:
    ∃ (p : LTSeries (Submodule R M)), p.head = ⊥ ∧ p.last = ⊤ ∧
    ∀ (i : Fin p.length), ∃ P : Ideal R, Nonempty (
    ((p i.succ) ⧸ (Submodule.comap (p i.succ).subtype (p (Fin.castSucc i)))) ≃ₗ[R] (R ⧸ P)) := by
  sorry

(I didn't see the direct dependency relation between these and the associated primes version.)

I think all other different things (only the monotonicity of associated primes left :sweat_smile: )can find their appropriate places.

[Jz Pan]

I didn't use 00KZ, but prove 00L0 directly. On Stacks 00L0 is proved using 00KZ, though.

[Nailin Guan]

I know, I only wonder is this 00KZ really useful?

[Nailin Guan]

#23877 is closed and now replaced with #24242

[Nailin Guan]

Also requesting review for a easy PR #23718 for equiv between S^{-1}Hom(M,N) and Hom(S^{-1}M, S^{-1}N)

[Jz Pan]

Nailin Guan said:

I know, I only wonder is this 00KZ really useful?

I don't know, personally I didn't use it before.

[Jz Pan]

Maybe just keep it somewhere until it is needed in another results.

[Nailin Guan]

@Joël Riou Sorry for disturbing, this question may seem impolite, but do you have a plan to PR the linear structure on Ext?
We are needing some thing like the following and we want to know in what form and where it would go, thanks.

open CategoryTheory.Abelian.Ext DerivedCategory

variable {C : Type u} [Category.{v} C] [Abelian C] [HasExt.{w} C]

section Ring

variable (R : Type*) [Ring R] [Linear R C]

instance {X Y : C} (n : ℕ): Module R (Ext.{w} X Y n) := sorry

noncomputable def homEquiv₀_linearHom {X Y : C} : Ext X Y 0 ≃ₗ[R] (X ⟶ Y) where
  __ := addEquiv₀
  map_smul' := sorry

end Ring

section CommRing

variable (R : Type*) [CommRing R] [Linear R C]

noncomputable def bilinearCompOfLinear (X Y Z : C) (a b c : ℕ) (h : a + b = c) :
    Ext.{w} X Y a →ₗ[R] Ext.{w} Y Z b →ₗ[R] Ext.{w} X Z c where
  toFun α :=
    { toFun := fun β ↦ α.comp β h
      map_add' x y := by simp
      map_smul' := sorry }
  map_add' α β := by
    ext
    simp
  map_smul' := sorry

noncomputable def postcompOfLinear {Y Z : C} {a b n : ℕ} (f : Ext.{w} Y Z n) (X : C)
    (h : a + n = b) : Ext.{w} X Y a →ₗ[R] Ext.{w} X Z b :=
  (bilinearCompOfLinear R X Y Z a n b h).flip f

end CommRing

[Nailin Guan]

After some refactor, the following is the current dependency graph:
4982435f285350165149047e1d313d6.jpg

[Joël Riou]

I already did four prerequisite PRs #23779, #23777, #23815, #24309.

[Joël Riou]

The API should be as in https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/DerivedCategory/Ext/Linear.lean

[Nailin Guan]

Thanks, we will try unify them.

[Riccardo Brasca]

Hi all, I am in Beijing now and I am happy to discuss anything about this. Can you summarize what is your proposed definition of depth?

[Nailin Guan]

As we have rees theorem now, the index of first nontrivial Ext(A/I, M) and maximal length of M-regular sequence in I is equal when A Noetherian and M finitely generated.
So for the definition of depth, which one should we use? As in the case with conditions mentioned above, any of the two won't matter, however in the non-Noetherian case or not finitely generated case (if we really care), which is better?

[Nailin Guan]

To unify with ringKrullDim, depth would also be WithBot ℕ∞, however in which case should be positive/negative infinity is not clear yet, for example when M = IM Subsingleton A

[Nailin Guan]

@Ruiqi Chen found in some books, there is two definitions, one is grad(I,M) the maximal length of regular sequence, depth(I,M) is the first nontrivial Ext(A/I,M), then rees theorem show they are the same when A Noetherian and M finitely generated.

[Riccardo Brasca]

There is a small problem withe first nontrivial Ext: what should be the universe of M? Note that to write Ext(X, Y) X and Y must be in the same category (A-Mod here), but in particular they must be in the same universe.

[Nailin Guan]

He also mentioned we can define depth(N,M) for two modules, in this case should we use ModuleCat R or [AddCommGroup] [Module R]?

[Nailin Guan]

Riccardo Brasca said:

There is a small problem withe first nontrivial Ext: what should be the universe of M? Note that to write Ext(X, Y) X and Y must be in the same category (A-Mod here), but in particular they must be in the same universe.

I think we would align with what we use in rees theorem, M : Type v and Small.{v} R/I then use Shrink.{v} R/I

[Riccardo Brasca]

Nailin Guan said:

He also mentioned we can define depth(N,M) for two modules, in this case should we use ModuleCat R or [AddCommGroup] [Module R]?

I think Module R M, but one can always use Module.of, so this is not extremely important.

[Riccardo Brasca]

Nailin Guan said:

Riccardo Brasca said:

There is a small problem withe first nontrivial Ext: what should be the universe of M? Note that to write Ext(X, Y) X and Y must be in the same category (A-Mod here), but in particular they must be in the same universe.

I think we would align with what we use in rees theorem, M : Type v and Small.{v} R/I then use Shrink.{v} R/I

I agree, but we want the theorem that if the module itself is the local ring then one can compute this without using Shrink.

[Jz Pan]

Nailin Guan said:

Riccardo Brasca said:

There is a small problem withe first nontrivial Ext: what should be the universe of M? Note that to write Ext(X, Y) X and Y must be in the same category (A-Mod here), but in particular they must be in the same universe.

I think we would align with what we use in rees theorem, M : Type v and Small.{v} R/I then use Shrink.{v} R/I

We can define a Module version of Ext which is a wrapper of category version of Ext, i.e. CategoryVersionOfExt (lift of X) (lift of Y)

[Riccardo Brasca]

This should probably be discussed a bit, since we all want a "concrete" version of Ext for modules, but it will probably be something like that. And we still want that if R and M are in the same universe then we can compute it without any lift/shrink.

[Joël Riou]

Ext in the category ModuleCat commutes with the uliftFunctor on both arguments (at least assuming the ring is "small": the reason is that a projective (or injective) module in a small universe stays so in a higher universe), so that in principle, it should be possible to define a heterogeneous universe version of Ext, but I think it would be extremely painful to construct a good API for that (and I certainly do not intend to formalize this anytime soon). Practically speaking, I would think it would be ok to assume that both modules are in the same universe if we want to use Ext.

[Nailin Guan]

Riccardo Brasca said:

Nailin Guan said:

Riccardo Brasca said:

There is a small problem withe first nontrivial Ext: what should be the universe of M? Note that to write Ext(X, Y) X and Y must be in the same category (A-Mod here), but in particular they must be in the same universe.

I think we would align with what we use in rees theorem, M : Type v and Small.{v} R/I then use Shrink.{v} R/I

I agree, but we want the theorem that if the module itself is the local ring then one can compute this without using Shrink.

For local ring R R/IsLocalRing.MaximalIdeal is also in the same universe of R same as R/I, I think we still need some Small.{v} and Shrink.{v}?

[Nailin Guan]

Andrew Yang said:

I think depth <= dim could be done separately? (If you use the regular sequence def) At least we have that in FLT already.

We currently want to prove depth(M) <= dim(R/p) for associated prime p.
I saw in Matsumura, if we use Ext definition, it still need a lot more things.
Thanks.

[Nailin Guan]

Sorry, we found it, but I didn't find it straight forward from the existing result.

[Andrew Yang]

I was referring to https://github.com/ImperialCollegeLondon/FLT/blob/5316b38f25349bcdabc7a257ecc96b31686abf00/FLT/Patching/Utils/Depth.lean#L52 in case you didn't find it.