Formalising Commutative Algebra

Stream: Is there code for X?

[Suryansh Shrivastava]

I have been planning to formalize Hartshorne exercises, which require many theorems from Atiyah Macdonald and Matsumura. So, I was wondering grossly how much theory from Matsumura has been formalized?

[Johan Commelin]

I don't know Matsumura by heart... but concerning Atiyah-Macdonald: I think we have basically everything except for dimension theory and may some things on primary decompositions. Flatness seems to be done, but maybe hasn't landed in mathlib yet.

[Suryansh Shrivastava]

Okay, maybe I'll first try to formalize the exercises from Atiyah - Macdonald. Is that doable?

[Riccardo Brasca]

Those are surely doable. I have students working on units/nilpotent/zero divisors of polynomials/power series

[Suryansh Shrivastava]

A while back, I saw you guys were working on the fact that an A-module M is flat

$$\iff I \tensor M \equiv IM $$

[Suryansh Shrivastava]

That's a result of Matsumura right? and assumes many facts from homological algebra like the preservation of tensor product in direct limits and so on... How is that working out?

[Suryansh Shrivastava]

Riccardo Brasca said:

Those are surely doable. I have students working on units/nilpotent/zero divisors of polynomials/power series

Is there a public repository available for the same?

[Kevin Buzzard]

I think @Jujian Zhang has the flatness result above, not sure if it's PRed though

[Kevin Buzzard]

He spoke about it in London learning lean but I didn't put this term's videos up on YouTube yet