Collaborators for work on (noncommutative) Noetherian rings?

Stream: new members

[Jan Grabowski]

Hi. I'm new to Lean and have been working through the basics over the last few days, using various online notes (thanks to their authors!). I'm keen to contribute to mathlib but am feeling a significant gap between my current abilities and being able to formalize results in my research niche, so would like to contribute some time on more well-known (and potentially useful-to-other-people) things as a way to upskill.

My research area is noncommutative geometry (but very much at the algebraic/categorical end) [http://www.maths.lancs.ac.uk/~grabowsj/] so a natural starting point for me would be to look at fundamentals of (not necessarily commutative) Noetherian rings. In particular, I'd be interested in formalizing the contents of (at least parts of) Goodearl-Warfield's "An Introduction to Noncommutative Noetherian Rings" [https://zbmath.org/1101.16001].

I don't feel very confident in being able to do this by myself, though, so would like to ask if anyone would be interested in collaborating on this as a "small project"? If you would be, that'd be great - I'm contactable via here or various methods on my website.

[Edit:] Thanks,

Jan

[Kevin Buzzard]

The most fun thing to do in Lean is to fill in a sorry so perhaps one way of starting on such a project is attempting to state a theorem which you think we don't have in mathlib already and which you think is of interest (for example an early theorem in the book). Do you think you are up to such a task? Stating theorems is quite a different task from proving them and not always easy, which is why I think it might be a good project -- it might teach you some useful things.

[Kevin Buzzard]

(thanks)

[Kevin Buzzard]

PS if you are a member of staff at a university then one approach is to get students to help you (e.g. by supervising projects); this was a very effective method for me at Imperial because some of the students picked up the software more quickly than I did, and then they taught me things!

[Jan Grabowski]

First things first - I've swapped out my username as requested. :smile:

I don't (yet) know if I am up to it: I can already see that just the statement of things is not trivial (and indeed, for things I've worked on, often the proofs have been very much the human version of rfl, so this is very similar to my research life in general). That makes me nervous but so does the basic set up - from getting a "working" Lean project file up and running, to figuring out what is and isn't in mathlib and beyond, hence on the "problem shared" principle I was hoping someone might be interested in working together on it.

Currently I have time but no students, and at my next opportunity to have students I am likely to have rather less time. But indeed this would have been good. Perhaps someone here might lend me theirs :joy:

[Johan Commelin]

You mention Goodearl-Warfield's "An Introduction to Noncommutative Noetherian Rings" [https://zbmath.org/1101.16001].
Do you have a precise pointer to a result that you would like?

[Jan Grabowski]

Ultimately, I'd like to have a tool to help me work with various classes of nice noncommutative rings (notably, iterated skew-polynomial and skew-Laurent extensions) and their localisations: it's frustratingly easy to make seemingly small but fatal logical errors manipulating expressions, for example.

But to be specific, let's say that I would be very happy to see the definitions of skew-polynomial and skew-Laurent extensions, the skew Hilbert basis theorem (Thm 1.14 and its generalisation Thm 2.6) and(?)* constructions of some (small?) quantum algebras, about which things could be proved. That is, a moderate amount of section 2 of loc. cit. It would make sense to have the fundamental lemmata on Noetherian rings first, cf. section 1 of loc. cit.

[* I can see there might be mixed views on this "and", in that it seems to me that mathlib aims more at general theorems than theorems about specific examples - perhaps I've got the wrong end of this stick, as a newbie, so I'm happy to be corrected. But if that is the case, maybe constructing specific algebras is less appropriate since Lean isn't a computer algebra system.]

[Johan Commelin]

You are mostly right in your impressions about examples and mathlib. But I think have such specific constructions is actually also a good thing. Because it provides evidence that the rest of the definitions and theory have been setup correctly.

[Jan Grabowski]

PS. According to the Library information at ## Mathlib.RingTheory.Noetherian.Defs, what is currently implemented is left Noetherianity, but just named Noetherianity. Goodearl-Warfield (inevitably!) prefer right Noetherianity and developing noncommutative geometry would require separate L, R and 2-sided definitions. This is one thing that felt like it pushed the bar to entry up a notch for me, unfortunately...

[Johan Commelin]

Anyway, my suggestion would be to pick one of those results from section 1, and try to start writing the statement in Lean.
If you get stuck, post partial progress, and we'll help you along. You should be able to iterate quickly that way.

[Johan Commelin]

Yeah, about L/R/2-sides, this is certainly an unfortunate artifact of how mathlib grew in the past few years.

[Johan Commelin]

@Jireh Loreaux and @Junyan Xu have been on a "crusade" to make the library more non-commutative. So they will certainly be able to say useful things about how to proceed here.

[Jan Grabowski]

I should be clear: I'm not attempting to blame anyone. It's perfectly natural that with comm alg and alg geom in mind, someone implemented (left) Noetherian this way. But I'd be very grateful for

1. suggestions on how to go about getting the interface of what you suggest (i.e. basics from section 1) with existing mathlib working well and
2. a (pointer to) a "minimal working workspace" setup for a Lean file, aka I just de-sorry-fied @Kevin Buzzard's worksheets without paying any attention to the header/footer needed to make it function... (One possible answer is presumably "strip out the middle of one of those"?!)

[Jan Grabowski]

Indeed, probably for now I could just prove things from Goodearl-Warfield in the left setting instead. Might not hurt - I am left-handed so always liked left actions etc. better anyway :joy:

[Ruben Van de Velde]

Probably easiest is to create a new project, though the usual instructions are unfortunately broken this week. Start with the fist section in https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency and then add the rev key to the lakefile.toml file like this:

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.15.0"

and then run lake update

[Kevin Buzzard]

Another alternative is that you just wait until the current issues are resolved (which will be in under a week), clone mathlib instead, and just make a new file in Mathlib called experiments.lean and begin hacking in there.

I don't have access to the book -- can you give the maths definitions of skew-polynomial and skew-Laurent extensions, and state the skew Hilbert basis theorem? This site accepts LaTeX but you have to enclose it by double-dollars $$ x=y $$ for some reason.

[Jan Grabowski]

Thanks both, I have a project up and running now (as far as I can tell). I'll post the definitions tomorrow, @Kevin Buzzard , when I'm back in the office (with the book).

[Jan Grabowski]

Fortuitously (or perhaps partly by strategic choice) Goodearl-Warfield use Lean-style definitions and universal properties to define skew-polynomial and skew-Laurent rings:

For a ring $R$ and automorphism $\alpha \colon R \to R$, write $S=R[x;\alpha]$ to mean that (a) $S$ is a ring with $R$ a subring; (b) $x\in S$; (c) $S$ is a free left $R$-module with basis $\{ 1,x,x^{2},\dotsc\}$ and (d) $xr=\alpha(r)x$ for all $r\in R$. Such an $S$ is called a skew-polynomial ring over $R$.

Lemma 1.11: for $R$, $\alpha$, $S$ as above, if $T$ is a ring, $\phi\colon R\to T$ and we have a $y$ such that $y\phi(r)=(\phi\circ \alpha)(r)y$ for all $r\in R$, then there is a unique ring homomorphism $\psi\colon S\to T$ such that $\psi|_{R}=\phi$ and $\psi(x)=y$.

For a ring $R$ and automorphism $\alpha \colon R \to R$, write $S=R[x^{\pm 1};\alpha]$ to mean that (a) $S$ is a ring with $R$ a subring; (b) $x\in S$ is a unit; (c) $S$ is a free left $R$-module with basis $\{ 1,x,x^{-1},x^{2},x^{-2}\dotsc\}$ and (d) $xr=\alpha(r)x$ for all $r\in R$. Such an $S$ is called a skew-Laurent ring over $R$.

Exercise 10D: for $X=\{1,x,x^{2},\dotsc\}\subseteq S=R[x;\alpha]$, $X$ is Ore and a denominator set with the localization $SX^{-1}$ equal to $R[x^{\pm 1};\alpha]$.

Skew Hilbert Basis theorem: with notation as above, if $R$ is right (left) Noetherian, so are $S=R[x;\alpha]$ and $T=R[x^{\pm 1};\alpha]$.

There is a further generalisation of $R[x;\alpha]$, to $R[x;\alpha,\delta]$, where $\delta$ is a derivation and we ask in (d) that $xr=\alpha(r)x+\delta(r)$. The rest of the above also generalises, except possibly the localization claim (it's not explicitly in [GW], but I expect it to still work). Together with iterating the above constructions, we can obtain many rings arising as quantizations of natural geometric objects from Lie theory.

[Jan Grabowski]

@Matteo Cipollina has privately sent me some thoughts on formalising these concepts (thank you, @Matteo Cipollina :big_smile:), so I think we're up and running. Thanks to everyone who has helped in this thread already and if anyone else has any contributions, that would be great. I've set up a repo on my GitHub for this, in particular.

[Junyan Xu]

There are two open PRs on skew monoid algebras: #10541, and #19084

[Jan Grabowski]

Thanks @Junyan Xu. A quick look suggests that (i) what is outlined above would cover skew monoid algebras as a special cases and (ii) those PRs seem to have a lot of complications associated with them, and it's very unclear to me whether with the definitions above we might avoid those, or if we're heading for similar pain. Does anyone have any advice on what's appropriate to do? ( I definitely do not have the skills to refactor any significant parts of existing mathlib...)

My instinct is to worry about it later: although contributing to the whole enterprise is one global motivation, learning Lean is a local one, and so spending a few days on something that might eventually not get merged is not a big deal for me.

[María Inés de Frutos Fernández]

Jan Grabowski said:

For a ring R and automorphism α:R→R, write S=R[x;α] to mean that (a) S is a ring with R a subring; (b) x∈S; (c) S is a free left R-module with basis {1,x,x2,…} and (d) xr=α(r)x for all r∈R. Such an S is called a skew-polynomial ring over R.

@Xavier Généreux and I have formalized the definition of skew polynomial ring (not yet in mathlib) as a special case of docs#SkewMonoidAlgebra.

[Jan Grabowski]

Thank you @María Inés de Frutos Fernández - looking at the link you included I see that the inputs are semirings and monoids, so more general than I'd initially thought (I guessed they were over fields).

There's also something of a terminology overloading issue, already present in Goodearl-Warfield and no doubt elsewhere. Namely, the more general version with derivations is also called "skew polynomial ring" and for later work, I'd like this implemented too. Have I missed something if I claim that your work doesn't handle $R[x;\alpha,\delta]$?

I was always expecting that there would be a point where new stuff had to be patched with existing mathlib and other contributions in progress. As above, I'm inclined to pretend this isn't an issue for the time being, but fully recognise it'll need resolving eventually. At that point, I hope we can discuss in more detail?

[María Inés de Frutos Fernández]

That is right, we did not formalize the generalization $R[x;\alpha,\delta]$. Our motivation for defining skew polynomial rings is that a particular one (which does not involve a derivation) is needed to define Drinfeld modules.

[Jan Grabowski]

Right. So (presumably?) at some point, I'll look to show $R[x;\alpha,0]$ is a skew monoid algebra.

[Kevin Buzzard]

Just to be clear -- is docs#SkewMonoidAlgebra not enough for you @Jan Grabowski ? This already made it into mathlib.

[Jan Grabowski]

Long-term, no - I want the version with non-trivial derivations and its Laurent analogue.

I've also somewhat changed my view on what to do first, having spent some time looking more closely at RingTheory.Noetherian - it seems you and Mario didn't impose commutativity of $R$ in either .Defs or .Basic, so all those results are available in (more than) the generality I was thinking of (given that you use Semiring and AddCommMonoid). So that's very helpful.

[Jan Grabowski]

If I might beg the indulgence of a newbie still getting their head round everything, how would one prove that $\mathbb{Z}$ is Noetherian in Lean? (Is it trivial, easy or hard?!)

[Kevin Buzzard]

Looks like it's very easy:

import Mathlib

example : IsNoetherianRing ℤ := by exact?
-- Try this: exact isNoetherian_of_isNoetherianRing_of_finite ℤ ℤ

More seriously, this question is hard to answer because it's quite ill-defined: in practice it will depend on how much you are allowed to assume about the concept of Noetherianness (for example there are several different definitions). Are we allowed to assume Euclid's algorithm or do we have to implement it from scratch? Can we assume a convenient definition of Noetherian (e.g. all ideals f.g.) or are you asking about an inconvenient definition (e.g. ACC?) Right now we're sitting on 7 years of very hard work so it's easy because it's already there but at some point someone had to join up the dots right down to the axioms of mathematics.

[Kevin Buzzard]

Here's another proof:

example : IsNoetherianRing ℤ := inferInstance

[Kevin Buzzard]

Here's how that proof was found by the system:

#synth IsNoetherianRing ℤ -- IsDedekindDomainDvr.toIsNoetherian
#synth IsDedekindDomainDvr ℤ -- IsDedekindDomain.isDedekindDomainDvr ℤ
#synth IsDedekindDomain ℤ  -- IsPrincipalIdealRing.isDedekindDomain ℤ
#synth IsPrincipalIdealRing ℤ -- EuclideanDomain.to_principal_ideal_domain
#synth EuclideanDomain ℤ -- Int.euclideanDomain

We have the theorem that the integers are a Euclidean domain, that a Euclidean domain is a principal ideal domain, that a principal ideal domain is a Dedekind domain, and that a Dedekind domain is Noetherian, and the result follows from a combination of all of those things; furthermore all of those theorems are known to the typeclass inference system (the "square bracket system") so they are discovered automatically. The assertion that the integers are a Euclidean domain is not actually a theorem because it contains some data (basically the well-founded norm function being used). All the machinery is there to formalize any mathematical proof you want of Noetherianness of Z so you can make it as easy or as hard as you like.

[Jan Grabowski]

So, I'm happy on both counts :smile:

You've explained how to do it in practice (and the point about 7 years' work is not at all lost on me!), but the second one is "the proof I was thinking of". Much appreciated :thumbs_up: