Regular sequences

Stream: mathlib4

[Brendan Seamas Murphy]

I've started working on an implementation of regular sequences, see https://github.com/leanprover-community/mathlib4/commit/1f37e06e117daae45861d056de1d08c73acdcddf for some very early stages work. I don't have a particular roadmap in mind yet. Next steps after cleaning up and merging what I've done so far are to define depth and the koszul complex, and to prove depth sensitivity of the koszul complex. I'd welcome any comments on the commit above or general thoughts on how this cluster of commutative algebra should be implemented.

One thing I want to note is that mathlib generally tries to work in high generality, but regular sequences are really not well behaved outside of noetherian local rings. While regularity is defined in mathlib for just a monoid, I couldn't find anything satisfying in the literature about regular sequences even over commutative semirings, and so have elected to define it only for commutative rings. In the non local and non Noetherian cases there's a chain of notions of regularity: regular sequence => weakly regular sequence => koszul-regular sequence => H1-regular sequence => quasi-regular sequence. These all coincide for a sequence in the maximal ideal of a Noetherian local ring. At the moment I've defined the first two of these. I don't know if it's worth spending time defining the rest of them at the moment. But I'll certainly be using the notion of a Koszul-regular sequence even in the Noetherian local case, and probably quasi-regular sequences, even if unnamed. So it's maybe worth defining all these regularity conditions now? But I'm worried about getting bogged down in this and not doing any of the fun commutative algebra :)

Edit: Also, a lot of stuff about depth and regular sequences have a graded analogue which is also quite useful. I'm not sure if it makes sense to do this in parallel, delay it until it's needed, or use some common abstraction that's been worked out (which I'm not familiar with).

Again, I'd love to hear others' input on this stuff

[Andrew Yang]

First of all, great work!
First thought: I think the following definition is easier to use?

import Mathlib

variable {R} [CommRing R]

open scoped Pointwise in
def IsWeaklyRegular (M) [AddCommGroup M] [Module R M] : (rs : List R) → Prop
| [] => True
| r :: rs => IsSMulRegular M r ∧ IsWeaklyRegular (M ⧸ (r • (⊤ : Submodule R M))) rs

[Brendan Seamas Murphy]

Initially I defined it as an inductive prop, which is basically the same as what you've written. But then I realized there's more than one induction principle we're going to want to use for (weakly) regular sequences and so it didn't seem worth it to start with one over the other. Anything you want to do with the defintion you've given there can be done with IsWeaklyRegular.rec

[Brendan Seamas Murphy]

Also, when I used that original defintion I needed something like IsWeaklyRegular.isWeaklyRegular_cons_iff anyways to establish the equivalence with the "non-inductive" definition. So I'm not sure there's much to simplify in the "bootstrapping" stage, and once we're past that it doesn't really matter which definition we start with

[Andrew Yang]

Isn't IsWeaklyRegular.isWeaklyRegular_cons_iff an Iff.rfl under this definition?

[Andrew Yang]

(Note that this is a recursive function, rather than an inductive Prop)

[Brendan Seamas Murphy]

Ah sorry, what I said wasn't very clear. I needed the content of that lemma as it currently stands in the inductive step of the proof that the inductive definition of IsWeaklyRegular is equivalent to the non-inductive(/non-recursive) defintion

[Brendan Seamas Murphy]

(the proof of IsWeaklyRegular.isWeaklyRegular_cons_iff under the inductive defintion isn't an Iff.rfl but it's still trivial, both directions are one liners where you pattern match and shuffle around data)

[Andrew Yang]

I guess my question is then "where did you use the non-inductive definition?" It doesn't seem easy to use.

[Brendan Seamas Murphy]

Well it hasn't been used anywhere, because I haven't proven anything yet except comparing definitions. I picked this one because I didn't want to prefer one of the possible two inductive definitions (one changing the ring and one not), because any use of the others can be done using the induction principles, and because it's the one in the stacks project, on Wikipedia, and in Bruns & Herzog

[Andrew Yang]

Yeah and the point I'm trying to make is that it probably won't be used anywhere.
Though I don't have much to backup this claim other than my instinct / experience.
And even if you really want such a characterization, Fin n -> R would work better than List R IMO.

[Andrew Yang]

Maybe I just find it awkward to random access a linked list.

[Johan Commelin]

@Amelia Livingston you also worked on the Koszul complex, right? Or am I misremembering something?

[Andrew Yang]

Ah I guess I see what you meant now. These are different definitions and you want to formalize both. However the "non-inductive definition" should still be an inductive definition so that it gives good defeqs IMHO. Something like

import Mathlib

variable {R} [CommRing R] (M) [AddCommGroup M] [Module R M]

open scoped Pointwise

instance smulSubmodule : SMul (List R) (Submodule R M) where
  smul rs N := rs.foldr (fun r N' => r • N ⊔ N') ⊥

def IsWeaklyRegular (rs : List R) : Prop :=
  List.foldr (· ∧ ·) True <| rs.inits.zip rs |>.map
    fun (rs, r) ↦ IsSMulRegular (M ⧸ rs • (⊤ : Submodule R M)) r

example {r : R} : IsWeaklyRegular M [r] ↔ IsSMulRegular (M ⧸ (⊥ : Submodule R M)) r ∧ True := Iff.rfl

[Brendan Seamas Murphy]

Johan Commelin said:

Amelia Livingston you also worked on the Koszul complex, right? Or am I misremembering something?

I'd love to see this code! One thing I've been wavering on is whether we need the CDGA structure on the koszul complex from the start. DGAs are one of those things that have stayed out of mathlib for a long time, so I'm not sure it's worth diving into right now...

I have been wondering whether the answer to the DGA type theory woes is to work with internally graded differential modules instead of (co)chain complexes. But this would basically require duplicating the chain complex API. Maybe it's worth it if we want both in the end?

[Kevin Buzzard]

(Note that this was a Lean 3 project which Amelia did with me years ago)

[Amelia Livingston]

Indeed I do have some old Lean 3 code about Koszul complexes but I very much doubt it's useful - homological algebra in mathlib has changed & progressed a lot since then. But I can double-check tomorrow

[Brendan Seamas Murphy]

An instance where I found the non-inductive characterization easier to work with was when proving this lemma:

lemma AddEquiv.isWeaklyRegular_congr [Module S M'] {e : M ≃+ M'} {as bs}
    (h : List.Forall₂ (fun (r : R) (s : S) => ∀ x, e (r • x) = s • e x) as bs) :
    IsWeaklyRegular M as ↔ IsWeaklyRegular M' bs :=

[Brendan Seamas Murphy]

I'm sure it's possible to do this using the induction principle for Forall₂ or for IsWeaklyRegular directly, but I found it more straightforward to extract out the inductive-ness to a lemma saying essentially the image of as.take i • ⊤ under e is bs.take i • ⊤ and use this to define e' : (M ⧸ List.take i as • (⊤ : Submodule R M)) ≃+ (M' ⧸ List.take i bs • (⊤ : Submodule S M'))

[Brendan Seamas Murphy]

Fyi I'm still working on this. I'm reaching a cutoff point (permutation of regular sequences over Noetherian local rings) and will start breaking things up into a bunch of smaller commits after that. I'm almost there, I have a general lemma about permutability of regular sequences (which looks a little tortured but will also apply in e.g. the graded case eventually) and just need to write some glue code
8bc3d8c7-fb00-4685-b205-e65b591e2331.png

[Brendan Seamas Murphy]

I've created a flood of PRs for all the excess stuff I needed when working on this. After this I just need to merge three files: Algebra/Module/Torsion, RingTheory/Regular/IsSMulRegular, and RingTheory/Regular/RegularSequence. I should be able to separately PR in the changes to that first file, while the latter two are completely new. I'm trying to decide whether the ModSMulBy abstraction is a good idea right now, and will probably try a refactor without it before I start a PR for the bulk of the work on regular sequences

[Johan Commelin]

@Brendan Seamas Murphy would you mind linking to the PRs in question that you want to have reviewed?

[Johan Commelin]

(Just write down the number, with a # in front, an zulip will auto-linkify them.)

[Brendan Seamas Murphy]

#13100 #13102 #13116 #13117 #13118 #13119 #13120 #13121 #13122 #13123 #13126 #13127

[Brendan Seamas Murphy]

#13127 depends on #13119, all others are independent. All of them are (imo) small, most are very small

[Brendan Seamas Murphy]

and #13130, which depends on #13102

[Johan Commelin]

@Brendan Seamas Murphy That's a very nice list!

[Johan Commelin]

I've reviewed most of them.

[Andrew Yang]

These PRs looks suspiciously like the ingredients for "Let $\Gamma : M \to N \to P \to 0$ be an exact sequence of modules over a local ring $R$ with $N$ finite free and $M$ finite, then $\Gamma$ is split exact iff $\Gamma \otimes k$ is" which I happen to need. Maybe you also have this result somewhere?

[Brendan Seamas Murphy]

Nope, don't think I've got anything like that sorry

[Johan Commelin]

@Brendan Seamas Murphy Please post updated lists of PRs that you want to have reviewed.

(I really hope that in the future we will have better tooling to track such PRs. Atm the #queue is too overwhelming...)

[Brendan Seamas Murphy]

#13130 is the only one no one's touched yet

[Kevin Buzzard]

There's a digit missing in that one...

[Brendan Seamas Murphy]

Oops, fixed

[Ruben Van de Velde]

Maybe @Oliver Nash

[Johan Commelin]

@Brendan Seamas Murphy can you please merge master into that pr?

[Brendan Seamas Murphy]

Sure, I'll get around to it later today (~1 hour from now?). I'll remove the awaiting-review tag now and readd it when I get to it

[Brendan Seamas Murphy]

Done

[Johan Commelin]

Thanks! I'll take a look now

[Johan Commelin]

@Brendan Seamas Murphy I left a few minor comments.

[Brendan Seamas Murphy]

Okay, currently left to merge are #13121 #13122 #13126 #13127 and #13130. Of these #13121 has been reviewed by 2 people and has no comments left on it, #13122 has an ongoing conversation between me and @Andrew Yang, #13126 and #13127 have been reviewed by @Andrew Yang and (I think?) are both ready to merge, and #13130 has had a quick review but might need another pair of eyes on it

[Brendan Seamas Murphy]

All of them currently build and except for #13122 have no outstanding comments

[Brendan Seamas Murphy]

#13122 should be ready to merge, #13130 could still use some review, all the others are tagged maintainer merge

[Brendan Seamas Murphy]

#13130 has had two sets of eyes on it and currently builds, everything else is on the queue

[Brendan Seamas Murphy]

Okay, the last two files were a mess and I had to change how I did some stuff. The penultimate PR is at a place where I'm happy with it, at #13360. I could break this up further but I think I need to get some momentum going again and finish this off

[Brendan Seamas Murphy]

@Johan Commelin you suggested I ping

[Johan Commelin]

@Brendan Seamas Murphy Thanks for the ping. Merged. And, thanks @Andrew Yang for the reviews.

[Brendan Seamas Murphy]

Great. Assuming there's no issues with bors, next PR is at #12544. I think it's at a good state but it'll be easier to review once I can merge master-with-13360 into it

[Brendan Seamas Murphy]

yep, ready for review now. The PR adds a single file with 645 lines

[Yongle Hu]

What is the current status of the formalization of Koszul complex? I think we need the Koszul resolution for our project of formalizing Lie algebra cohomology.