The `Ext` functor

Stream: mathlib4

[Yongle Hu]

We are going to formalize the following proposition: Let R be a Noetherian ring, M a finite R-module, and I an ideal such that IM ≠ M. Then all maximal M-sequences in I have the same length n given by

$$n = \min\{i : \operatorname{Ext}_R^i(R/I, M) \neq 0\}.$$

However I found two Ext functor (docs#CategoryTheory.Abelian.Ext and docs#Ext) in Mathlib. The first Ext docs#CategoryTheory.Abelian.Ext doesn't seem to have the HasExt instance for ModuleCat available, while the second Ext docs#Ext seems to lack the long exact sequence. Are there simple ways to address these missing properties?

[Riccardo Brasca]

cc @Joël Riou

[Joël Riou]

It is better to work with docs#CategoryTheory.Abelian.Ext because docs#Ext is meant to be removed (replaced by Abelian.Ext) in a not so distant future.
In #19591 (which should hopefully be merged soon), I show that HasExt holds when there are enough projectives (and that Ext^0 compares to Hom), which will obviously apply to suitable categories of modules. In between, you may just use HasExt as a variable.
(Also, docs#CategoryTheory.HasProjectiveDimensionLT could be of interest.)

[Notification Bot]

Yongle Hu has marked this topic as resolved.

[Notification Bot]

Yongle Hu has marked this topic as unresolved.

[Yongle Hu]

Thank you very much for your detailed reply! Regarding docs#CategoryTheory.Abelian.Ext, I still have some questions:

1. I found the theorem docs#CategoryTheory.HasExt.standard, but I'm not sure about the meaning of this theorem. Is it saying that Ext can be defined in any Abelian category (even without proving there are enough projectives)?

2. Currently there is the canonical map (X ⟶ Y) → Ext X Y 0. Can it be proven that it is an Abelian group homomorphism? Furthermore, in ModuleCat R, can Ext X Y n be equipped with an R-module structure?

3. Is it now possible to compute Ext X Y n using projective resolutions?

[Joël Riou]

1. Yes, the point of this construction is that it can be defined in any abelian category, but the Ext-groups may be defined only in a higher universe.
2. /3. Not yet in mathlib.

[Yongle Hu]

I think the existing properties of docs#CategoryTheory.Abelian.Ext in Mathlib together with Ext X Y 0 ≃ (X ⟶ Y) should be almost sufficient to complete our proof. Thanks a lot for your patient replies!

[Notification Bot]

Yongle Hu has marked this topic as resolved.

[Nick_adfor]

@Joël Riou

We are going to formalize the following proposition: (Auslander--Buchsbaum) Let R be a Noetherian local ring, M a finite R-module.

If

$$\operatorname{proj\,dim} M < \infty$$

then

$$\operatorname{proj}\dim M + \operatorname{depth} M = \operatorname{depth} R.$$

We'd like to find proj resolution or projective module ext to solve the question. But in docs#CategoryTheory.HasProjectiveDimensionLT we do not find some of good use. We seem to think the definition of Ext in Lean cannot support us to finish the proof.

[Notification Bot]

Nick_adfor has marked this topic as unresolved.

[Nick_adfor]

Is there an algorithm that can be implemented in Lean for the proj resolution of an A/I where the base ring A is a complete intersection?

[Nick_adfor]

We even considered formalizing derived categories or triangulated categories. That's really crazy. We do need some help.

(Since we haven't come up with a suitable method for this part, today our work has shifted to formalizing Koszul complex.)

[Yongle Hu]

The vanishing of higher Ext for projective objects has been proved here.

[Jz Pan]

Nick_adfor said:

We even considered formalizing derived categories or triangulated categories.

Seems that there are triangulated categories in mathlib, but not derived categories.

[Joël Riou]

Jz Pan said:

Seems that there are triangulated categories in mathlib, but not derived categories.

Seems you did not search very thoroughly.

[Jz Pan]

Joël Riou said:

Jz Pan said:

Seems that there are triangulated categories in mathlib, but not derived categories.

Seems you did not search very thoroughly.

You are right :man_facepalming: I only checked files under CategoryTheory directory and found nothing...

[Robin Carlier]

Nick_adfor said:

(Since we haven't come up with a suitable method for this part, today our work has shifted to formalizing Koszul complex.)

I’ll allow myself to chime in this conversation as I thought about this at some point.

The Koszul complex seems like something that has to be formalized at one point or an other anyway, so this might be the right thing to do. It is a fundamental construction, and if you read Serre's book "local algebra" it is clear that it is the backbone of this theory.

I considered ways to formalize it at some point, but to me the most "canonical" way to do it would be to formalize arbitrary n-ary tensor products of objects in a (symmetric) monoidal category, and then apply this to the category of complexes, applied to suitable family of objects (the length 2 "multiplication by -" complexes if I recall correctly). I am currently thinking of a rather roundabout way of having a nice enough n-ary tensors products in arbitrary monoidal categories, but it will take time before this is usable, probably more time than you are willing to wait.

I guess there would then be the issue of comparing it with the "usual" one, defined with exteriors powers (last time I checked, mathlib did not even have the basis of exteriors powers of a free module.)

(Edit: there is of course the option of taking a shortcut and and define it directly the usual way, and that might be more suited for you need, so the above is of course a rather subjective view of the construction.)

Perhaps an unprompted opinion, but I feel like this kind of commutative algebra that relies heavily on homological invariants should wait on more rock-solid homological/derived infrastructure in mathlib, and we’re slowly but surely getting there thanks to @Joël Riou's work.

[Ruben Van de Velde]

On the other hand, having applications can help build solid foundations

[Nick_adfor]

Robin Carlier said:

Nick_adfor said:

(Since we haven't come up with a suitable method for this part, today our work has shifted to formalizing Koszul complex.)

(Edit: there is of course the option of taking a shortcut and and define it directly the usual way, and that might be more suited for you need, so the above is of course a rather subjective view of the construction.)

Perhaps an unprompted opinion, but I feel like this kind of commutative algebra that relies heavily on homological invariants should wait on more rock-solid homological/derived infrastructure in mathlib, and we’re slowly but surely getting there thanks to Joël Riou's work.

Just as you have said, I am also confused about how to choose the optimal (easiest to derive conclusions from) definition to formalize in Lean when encountering equivalent definitions in mathematics.

Not far ago, I was curious of the difference between Dedekind Real Number and Cauchy Real Number. (Lean is based on Cauchy Real Number)

[Kevin Buzzard]

The actual "under the hood" definition of a real number should be of no interest to the general mathlib user, because the API is there enabling you to use real numbers like Euler and Riemann, who neither knew nor cared about what a real number "actually was". More precisely, we have proofs that mathlib's real numbers are a complete ordered Archimedean field and that, up to unique isomorphism, there is only one complete ordered Archimedean field.

The situation with Koszul complexes is different. Here there is a lot of fiddling around with explicit finite complexes and techniques needed which might not be in mathlib in a convenient form.. However I agree with Ruben that having some concrete goals here is a very good way of actually informing the developmrnt of that homological API

[Yongle Hu]

I agree that trying to work on concrete tasks is helpful for building the homological algebra infrastructure in Mathlib. During this we can identify which properties are crucial and which APIs are convenient to use.

Now we have completed the proof for the theorem I initially mentioned (in this repo). Then we will be able to define depth (maybe depthGE?).
Also, we are formalizing the Koszul complex (in this repo) and plan to prove some properties related to the Koszul complex and regular sequences, for example, the relation of Koszul homology and Hom(R/x, M/xM) when x is a weak regular sequence.

During the formalization process, we found that the results in #19591 is critical to our proof. Additionally, since the vanishing of Ext X I (n + 1) for an injective object I hasn't been proven yet, some parts of the proof are slightly more complicated. We also found that the universe levels in many homological algebra results are unsatisfactory, for example, the fact that ModuleCat has enough projectives is currently only proven when the module M's universe level is max u v (I've opened #23690 to address this), and the tensor product functor in ModuleCat is currently only defined when the ring R and the module M share the same universe level.

[Joël Riou]

I would say that generalizing some results for ModuleCat.{v} R under the [Small.{v} R] assumption seems to go in the right direction, including for the monoidal category structure (even though this may break some definitional properties for the unit).
I can add dual results to #19591 for injective objects if there is a need.
In general, I would say that mathlib is almost ready to have more developments for the part of local algebra which involves Ext-groups. For results about Tor, we may have to wait as it may take a certain time to obtain the monoidal category structure on the derived category (even though I have a quite precise plan). However, we already have the tensor product of chain complexes.
For Koszul complexes, the better definition is probably using exterior powers as @Yongle Hu does, but it will also be important to give concrete formulas (case of a finitely generated free module, induction, etc) which will be useful in computations.
(Note: there are some chunks of code like https://github.com/xyzw12345/CohenMacaulay/blob/master/CohenMacaulay/Dependency/CategoryCenter.lean which intersect with code that I have at https://github.com/leanprover-community/mathlib4/pull/4197/files#diff-53530e7726155c41dea96c1f9436ce8e717954dbaaf92306011fe51ab4a39242 and which shall eventually show that the derived category of a R-linear category if R-linear, and then the Ext are also R-modules.)