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.

[Nailin Guan]

A small question here (may be a bit unrelated):
Do we have API for the equiv between Ext^n (N,M) and Ext^n(N,M') for M and M' isomorphic? I want to use this but didn't find it, I want to make sure whether it is there, at least the correct way of proving it, thanks.

[Joël Riou]

It follows from docs#CategoryTheory.Abelian.extFunctor.

[Nailin Guan]

Sorry, one more question : what about Ext^n (N, M) \equiv Ext^n (M,N)? Thanks

[Joël Riou]

This is not true.

[Nailin Guan]

Sorry, my fault, there isn't such thing.

[Jz Pan]

Do you mean balance of Ext?

[Nailin Guan]

Sorry for disturbing, when can we have Ext isomorphic to the homology of projective resolution? As I am needing Ext finitely generated when over noetherian ring, thanks.

[Joël Riou]

The relation with projective resolutions will take a certain time. The finite generation over noetherian rings can be shown easily by induction with the current setup.

[Nailin Guan]

Ok, maybe I should use dimension shifting to solve it. However, what about the linear version Ext.covariantSequence, I think we always need this, thanks.

[Joël Riou]

It will need a few more PRs including #24309 and #24567...

[Nailin Guan]

@Andrew Yang I had a look at your definition of depth and had a small question:
you wrote

def Module.depth : ℕ∞ :=
  sSup { List.length s | (s : List R)  (_ : Sequence.IsWeaklyRegular M s) (_ : ∀ r ∈ s, r ∈ maximalIdeal R) }

but in my computer this is taking sSup in ℕ then coe to ℕ∞, is this really able to reach ∞?

[Nailin Guan]

We current ly decide to have our def like this

noncomputable def moduleDepth (N M : ModuleCat.{v} R) : ℕ∞ :=
  sSup {n : ℕ∞ | ∀ i : ℕ, i < n → Subsingleton (Ext.{max u v} N M i)}

which would reach infinity when M=0, and compatible with regular sequence def when ring noetherian and both finitely generated and nontrivial.

[Nailin Guan]

Another question: do we have dimension of noetherian local ring is finite? As we want depth to be finite, thanks.

[Christian Merten]

Nailin Guan said:

Another question: do we have dimension of noetherian local ring is finite? As we want depth to be finite, thanks.

This follows from Krull's height theorem, which is not completely ported yet I think.

[Wang Jingting]

Well, it's actually ready at #23778, you can review it if you have time now. @Christian Merten

[Yaël Dillies]

Nailin Guan said:

Andrew Yang I had a look at your definition of depth and had a small question:
you wrote

def Module.depth : ℕ∞ :=
  sSup { List.length s | (s : List R) (_ : Sequence.IsWeaklyRegular M s) (_ : ∀ r ∈ s, r ∈ maximalIdeal R) }

but in my computer this is taking sSup in ℕ then coe to ℕ∞, is this really able to reach ∞?

The issue is that sSup isn't currently considered an arithmetic operator, so it doesn't propagate the expected type inside. Do

def Module.depth : ℕ∞ :=
  sSup {(List.length s : ℕ∞) | (s : List R) (_ : Sequence.IsWeaklyRegular M s) (_ : ∀ r ∈ s, r ∈ maximalIdeal R)}

or, much more idiomatically,

def Module.depth : ℕ∞ :=
  ⨆ (s : List R) (_ : Sequence.IsWeaklyRegular M s) (_ : ∀ r ∈ s, r ∈ maximalIdeal R),
    (List.length s : ℕ∞)

[Nailin Guan]

In my proof I used the first one you mentioned. See branch definition-of-depth

[Yaël Dillies]

Could you then please switch to the second? :slight_smile:

[Nailin Guan]

Nailin Guan said:

We current ly decide to have our def like this

noncomputable def moduleDepth (N M : ModuleCat.{v} R) : ℕ∞ :=
  sSup {n : ℕ∞ | ∀ i : ℕ, i < n → Subsingleton (Ext.{max u v} N M i)}

which would reach infinity when M=0, and compatible with regular sequence def when ring noetherian and both finitely generated and nontrivial.

What about this one? Should we change too? What do you think is the proper definition?

[Nailin Guan]

Yaël Dillies said:

Could you then please switch to the second? :slight_smile:

I'll work on it when my current work is finished. However can you tell the advantage of the second one? I am not familiar with these "_Sup"s. Thanks.

[Nailin Guan]

We currently have the following in progress:
1: Definition of depth on branch definition-of-depth including depth(N,M) = depth_I M for supp(N) = V(I) and the equivalence of maximal regular sequence.
2: Ischebeck theorem (Ext^i(N,M) vanish for i < depth M - dim N) on branch Ischebeck-theorem, missing the finitely generation of Ext
3:Auslander Buchsbaum on branch mbkybky/AuslanderBuchsbaum still in progress with very limited parts done.

[Nailin Guan]

I have a question here, how can I prove Ext^i(N,M) = 0 iff Ext^i(Shrink(N), Shrink(M)) = 0? This is met when considering depth for the ring itself, thanks.

[Joël Riou]

If Shrink N is in the same universe as N, etc, this would follow from the fact that there is an isomorphism in ModuleCat between them. Otherwise, as I have explained it above, it is currently out of reach.

[Nailin Guan]

Sorry maybe I didn't make it clear, it is the "Otherwise" case you mentioned.

[Nailin Guan]

There is a solution that is available but not that satisfying: we set every thing to same universe, then fix it when universe invariant APIs are ready.

[Joël Riou]

The best I can consider doing in the future is defining an induced map on Ext-groups induced by an exact functor (e.g. the ulift functor on ModuleCat) and provide lemmas which would assert these maps are bijections under suitable conditions. As I said above, even with these categorical results, it would be extremely painful to develop a good hererogeneous universe API for Ext, and I certainly do not intend to do that part myself.

[Joël Riou]

Then, unless someone volunteers to do a painful work without any reward, the only reasonable solution, when using Ext, is to assume that both modules are in the same universe. Alternatively, it would make sense, when it is possible, to use alternate definitions (e.g. of depth) which do not depend on Ext, and use Ext only in order to prove properties/criteria for these definitions. In the proofs, it would be perfectly fine to use a big enough universe and compute Ext there.

[Nailin Guan]

Thanks for your works!

[Nailin Guan]

Although we just think of a way of going aroud through rees theorem, this at least solve the finitely generated case, which include the case we need.

[Nailin Guan]

We almost finished Auslander Buchsbaum Theorem, but one thing left: Ext(N,-) commute with direct product, especially Ext^n_R(N,M) = 0 iff Ext^n_R(N,R) = 0 for free module M. Do anyone know the correct way of proving it? Thanks

[Joël Riou]

Could you clarify your statement? Are you talking of "products" or "coproducts"? do you assume R is noetherian and N is finite type?

[Nailin Guan]

I think we don't need any condition on N, and we only consider finite direct sum, although infinite should be correct.
I disscussed with another participant, we think it can be done using dimension shifting on N, anyway thanks for your help.

[Joël Riou]

Ah, if you consider only finite (bi)products, this just follows from the fact the Ext bifunctor is additive in both variables (I am not sure the Functor.Additive instances have been set, but the proofs should be found automatically because of the add_comp and comp_add lemmas.).

[Nailin Guan]

Nailin Guan said:

Nailin Guan said:

We current ly decide to have our def like this

noncomputable def moduleDepth (N M : ModuleCat.{v} R) : ℕ∞ :=
  sSup {n : ℕ∞ | ∀ i : ℕ, i < n → Subsingleton (Ext.{max u v} N M i)}

which would reach infinity when M=0, and compatible with regular sequence def when ring noetherian and both finitely generated and nontrivial.

What about this one? Should we change too? What do you think is the proper definition?

Do anyone have further comments on this? (the choice between sSup and iSup)
Should depth be the current one or:

def moduleDepth (N M : ModuleCat.{v} R) : ℕ∞ :=
  ⨆ (n : ℕ ) (_ : ∀ i < n, Subsingleton (Ext.{max u v} N M i)), (n : ℕ∞)

[Nailin Guan]

The latest dependecy graph. The three related to CM is still in progress and quite far from finishing, so PR is not opened yet.
79cc59771b63a10c7c1f7ade605717c.jpg

[Nailin Guan]

I have a question here, do we have the dimension of noetherian local ring is finite in any place? Then we won't need to deal with top in ENat all the time in the local case. Thanks.

[Christian Merten]

Yes, Krull's height theorem was recently merged, so it's here: https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.html#instFiniteRingKrullDimOfIsNoetherianRingOfIsLocalRing

[Kevin Buzzard]

It's great to see commutative algebra moving along like this!

[Nailin Guan]

Some changes in dependency (also the one yesterday isn't very clear):
babea80fe540312ffabb055c5a5a2ba.jpg

[Nailin Guan]

I have a problem here : I have proven the following result

theorem depth_le_ringKrullDim_associatedPrime [IsNoetherianRing R] [IsLocalRing R]
    [Small.{v} (R ⧸ IsLocalRing.maximalIdeal R)] [Small.{v, u} R]
    (M : ModuleCat.{v} R) [Module.Finite R M] [Nontrivial M]
    (P : Ideal R) (ass : P ∈ associatedPrimes R M) [Small.{v, u} (R ⧸ P)] :
    IsLocalRing.depth M ≤ ringKrullDim (R ⧸ P) := by

but sometimes when I take out an arbitrary associated prime I don't have [Small.{v, u} (R ⧸ P)], how can I resolve this?

In particular, I met this problem when using this to prove IsLocalRing.depth M ≤ ringKrullDim R should I port the result in FLT to mathlib or try to use the result above? Thanks

[Yongle Hu]

I think [Small.{v, u} (R ⧸ P)] can be obtained by assuming [UnivLE.{u, v}].

[Andrew Yang]

[Small.{v, u} R] probably implies [Small.{v, u} (R ⧸ P)]. But shouldn't there be a way to get rid of [Small.{v, u} R] by showing IsLocalRing.depth is equal under isomorphisms and ulift M to some big universe?

[Andrew Yang]

I just saw in your WIP PR that Ideal.depth requires [Small.{v} (R ⧸ I)]. I think this is quite bad and we should probably get rid of it.

[Nailin Guan]

Andrew Yang said:

I just saw in your WIP PR that Ideal.depth requires [Small.{v} (R ⧸ I)]. I think this is quite bad and we should probably get rid of it.

So, we should Ulift the module?

[Nailin Guan]

If the module live in max u v where u is the universe of the ring, everything can work well, I don't know Ulift in definition is good enough.

[Nailin Guan]

Andrew Yang said:

[Small.{v, u} R] probably implies [Small.{v, u} (R ⧸ P)]. But shouldn't there be a way to get rid of [Small.{v, u} R] by showing IsLocalRing.depth is equal under isomorphisms and ulift M to some big universe?

There is, but need some extra condition, as we don't have Ext commute with Ulift currently.

[Nailin Guan]

What about "[Small.{v, u} R] probably implies [Small.{v, u} (R ⧸ P)]" you mentioned? This would make all the thing only need [Small.{v, u} R] to ensure Ext exist.

[Nailin Guan]

I have something like this:

instance (I : Ideal R) [Small.{v, u} R] : Small.{v, u} (R ⧸ I) :=
  have : Function.Surjective ((Ideal.Quotient.mk I).comp (Shrink.ringEquiv R).toRingHom) := by
    simpa using Ideal.Quotient.mk_surjective
  Small.mk' (RingHom.quotientKerEquivOfSurjective this).symm.toEquiv

is this safe to be an instance? (I cuently wrote it as a local instance)

[Nailin Guan]

The newly updated dependency graph:
22010fd4c611d366c2b994c0cd8f369.jpg
Sorry first appear in #23937 due to Ext.bilinearCompOfLinear and homEquiv₀_linearHom(the linear version of addEquiv₀)

[Andrew Yang]

Is this suggestion of Joël possible?

Alternatively, it would make sense, when it is possible, to use alternate definitions (e.g. of depth) which do not depend on Ext, and use Ext only in order to prove properties/criteria for these definitions. In the proofs, it would be perfectly fine to use a big enough universe and compute Ext there.

[Nailin Guan]

I think the problem is it is impossible to define grad(N,M) (Matsumura notation) or here depth(N,M) for two modules without Ext. The universe invariant can be proven when appropriate FG and nontrivial condition is added.
At least we only need [Small.{v, u} R] now.

[Andrew Yang]

Nailin Guan said:

is this safe to be an instance? (I cuently wrote it as a local instance)

You should use docs#small_of_surjective and it should be an instance

[Robin Carlier]

It’s been a while since I last did some serious commutative algebra, so forgive me if this is incorrect, but isn’t depth(N, M) equal to the depth of the annihilatorAnn(N) in M? the depth of an ideal in a module is about length of regular sequences IIRC, and that definition should not a priori require Ext.
(Or is the catch that what I say require f.g modules?)

[Nailin Guan]

More precisely depth(N, M) is equal to the depth of the I in M when IM < M and support(N) = V(I) for finitely generated modules over noetherian ring.
But we found some reference really caring these things in non-noetherian and non-finitely-generated case.

[Riccardo Brasca]

What's the situation with #23935? @Joël Riou @Andrew Yang is there anything else that should be done?

[Andrew Yang]

It seems like there are still unaddressed comments.

[Nailin Guan]

Sorry, only because forgot to fix them(

[Nailin Guan]

We finally finished the proof of Theorem 30, Chater 6, Commutative Algebra, Matsumura about the most basic facts about CM module and CM ring.
Here is all the things it depends on. #24697, #24771 are ready for review. #23935 met some small problems when addressing some comments. #25213 is currently the only sorry free PR apart from these.
563b4beef5339d43f738255c3b35d8f.jpg

[Nailin Guan]

I have a small qustion here when trying to prove system of parameters form regular sequence in CM local ring: do we have a standard way to state system of parameters? Should I use maximalIdeal R ∈ (Ideal.ofList rs).minimalPrimes ? (we assume noetherian) Thanks.

[Kenny Lau]

I assume you would want to be using a function from a fintype?

[Nailin Guan]

I don't know both how to state the elements and the relation of the spaned ideal and maximal ideal.
As regular sequence is using List, I think in this case for the former one use Ideal.ofList is OK?

[Nailin Guan]

We are now trying to formalize Theorem 31, Chater 6, Commutative Algebra, Matsumura.
(see branch "CM-local-ring-is-catenary")
We currently finished the following: (main part of Theorem 31 (iii) )
in noetherian local ring
1: for regular sequence a1 ... ar we have ht(span{a1 ... ar}) = r
2: extending a seqence a1 ... ar with ht(span{a1 ... ar}) = r to a system of parameters
in CM local ring
3: system of parameters is regular

Newly updated dependency graph
50bd4c404c8ef3121fa9763aa4df0e1.jpg

Here is a small question: do we have definition of "catenary ring" or somebody is working on it? Thanks

[Christian Merten]

There is a group of students in Utrecht working on a definition of catenary orders, rings and topological spaces. The person to ask is @Edward van de Meent.

[Edward van de Meent]

The next few weeks i'm hoping to work on getting some of our work into Mathlib. This includes a definition of catenary orders, but since there are a bunch of auxilary definitions it might take a bunch of PRs and time before it's in mathlib for you to use

[Nailin Guan]

Thanks! Good enough! I would be taking final exam so won't be active for the few coming weeks, also there is no urgent need, I can always leave the results as relations of height for now :slight_smile:

[Nailin Guan]

Newly updated dependency graph (migrated to fork):
d32c676aefca69781e4a0daf0ed8eaa.jpg

[Nailin Guan]

We currently finished proving Theorem 31 (i),(iii) in #26245 (WIP), should be just one small step from what we have (every proper ideal I have ht I + dim A / I = dim A when A is CM) to catenary when definitions are ready.

[Nailin Guan]

We just finished proving a ring R is CM iff the unmixed theorem holds (Theorem 32, Chapter 6) in PR #26957

[Nailin Guan]

Currently we are trying to prove polynomial ring over CM ring is also CM. However we found we are needing some results about height of ideals in R[X]. Is anybody working on related results? For example dim R[X] = dim R + 1 for noetherian ring R.

[Christian Merten]

Nailin Guan said:

Currently we are trying to prove polynomial ring over CM ring is also CM. However we found we are needing some results about height of ideals in R[X]. Is anybody working on related results? For example dim R[X] = dim R + 1 for noetherian ring R.

This repo (from one of the PKU Workshops) contains this. I believe I have an open PR related to it. I can make more PRs, when I am back from vacation in a week or so. Feel free to take anything from there and make a PR from it in the meantime.

[Riccardo Brasca]

Nailin Guan said:

Currently we are trying to prove polynomial ring over CM ring is also CM. However we found we are needing some results about height of ideals in R[X]. Is anybody working on related results? For example dim R[X] = dim R + 1 for noetherian ring R.

I am almost sure I reviewed (and probably merged) a PR of @Andrew Yang with this.

[Andrew Yang]

What I did is the easy side of the inequality dim R + 1 <= dim R[X]
The other side needs noetherianness and a fair amount of dimension theory (which we mostly already have in mathlib).

[Nailin Guan]

Christian Merten 說：

Nailin Guan said:

Currently we are trying to prove polynomial ring over CM ring is also CM. However we found we are needing some results about height of ideals in R[X]. Is anybody working on related results? For example dim R[X] = dim R + 1 for noetherian ring R.

This repo (from one of the PKU Workshops) contains this. I believe I have an open PR related to it. I can make more PRs, when I am back from vacation in a week or so. Feel free to take anything from there and make a PR from it in the meantime.

I am almost finished with polynomial ring over CM ring is CM in #27131 , except for the following two "sorry" : for local ring (R, m),
1 : ht (m[X]) is not greater than ht(m) = dim R
2 : for a prime ideal pof R[X] and p \cap R = m, ht (p) is not greater than ht(m) + 1
The second should be a straight corrollary from the dimension of R[X], I don't know about the first one. Although I can force it through using height theorem, I can wait for the PRs from that repo.
As I am not that familiar with the structure of the repo, I probably wouldn't be able to open good PRs.

[Nailin Guan]

By the way, this PR depends on #26106 which proves IsWeaklyRegular is preserved under flat base change by @Yongle Hu . It should be ready for review as it is not blocked by other PRs now.

[Nailin Guan]

Newly updated dependency graph:
8b9def0cee1f5a1e1d15479ccc1aaed.jpg
currently #26106, #26210, #26219 are the only sorry free ones, they are independent of each other ready for review.

[Nailin Guan]

As linear structure on Ext is still missing, other ones are all stuck for now :neutral: . This sorry and another about FG of Ext over noetherian ring are the only ones. (the tool of dimension shifting is ready so wouldn't be that difficult)
However is it possible for anyone to check whether the definitions are good enough, as they may affect a lot. Thanks

[Joël Riou]

Nailin Guan said:

As linear structure on Ext is still missing, other ones are all stuck for now :neutral: .

You may push for someone to review #25931 and #26031 in the "PR reviews" channel. (I could PR the followup code where the linear structure on Ext is defined, but I do not like to make dependent PR on top of refactor PR...)

[Robin Carlier]

Will try to have a look at #25931 either tonight or tomorrow.

[Antoine Chambert-Loir]

I had a quick look. Your code is very clean. Up to the possible addition of some more documentation, this looks pretty good to me.

[Christian Merten]

Nailin Guan said:

1 : ht (m[X]) is not greater than ht(m) = dim R
2 : for a prime ideal pof R[X] and p \cap R = m, ht (p) is not greater than ht(m) + 1

These are now both contained in #27542.

[Nailin Guan]

We would like to move forward to formalize regular local ring is CM, I would like to know is anybody still working on it. I would like to unify our definition, thanks.

[Nailin Guan]

@Joël Riou sorry for might being impatient, may I ask for a help in updating your PR #27416? I met some problem when trying to copy that PR in newer version of mathlib, however I would like to test our PRs on the correct instance.
(we currently have the module instance on Ext defined as r • x = x.comp (mk₀ (r • 𝟙 Y)) (add_zero _), which is really to barbaric and cannot dirctly obtain Ext.comp is R-bilinear, but at least there is no sorry in data)
Thank you very much.

[Joël Riou]

There is a chunk of code which had disappeared from some unknown reason. #27416 should work again now.

[Nailin Guan]

I merged the branch of #27416 into my works and rearrage the PRs, now all PRs except polynomial over CM ring is CM is sorry free. (Ignore the ones related to regular local ring)
2b73e2a4381ad2143d0f72cbdfc4b223.jpg