Noetherian hom

Stream: Is there code for X?

[Oliver Nash]

I don't suppose anyone has proved these facts anywhere:

import Mathlib.RingTheory.Noetherian

variable (R : Type*) [CommRing R]

-- Does anyone have this anywhere?
instance (M : Type*) [AddCommGroup M] [Module R M] [IsNoetherian R M] :
    IsNoetherian R (Module.End R M) :=
  sorry

-- Or better yet, this?
instance (M N : Type*) [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N]
    [IsNoetherian R N] [Module.Finite R M] :
    IsNoetherian R (M →ₗ[R] N) :=
  sorry

[Jireh Loreaux]

Are you trying to nerd snipe someone? :laughing:

[Antoine Chambert-Loir]

Is it true? IIRC, you need M to have finite presentation.

[Oliver Nash]

Perhaps I've not added enough assumptions!

The proof I had in my head (for the second instance which implies the first) is "Since $M$ is finitely-generated I have a surjection $R^k \to M$ for some natural $k$, and thus an injection $Hom(M, N) \to Hom(R^k, N) \simeq Hom(R, N)^k \simeq N^k$. And then $N^k$ is Noetherian etc.

I'm focused on other things for now but I'll think about this again later on if nobody points out my error first!

[Antoine Chambert-Loir]

Sorry, I had missed that the hypothesis that N was Noetherian.

[Oliver Nash]

Ah so maybe I'm OK then --- in your defence it doesn't help that I sort-of rename M to N as I move from one instance to the next.

[Antoine Chambert-Loir]

My feeling is that some people here (I count myself in them) should take the time to take some books such as Bourbaki's Algebra and Commutative Algebra and patiently and consistently add everything that is there. Possibly simultaneously writing that stuff in comprehensive form. And the more we wait for it, the more painful it will be.

[Riccardo Brasca]

This is one of the reasons we have students, isn't it? :)

[Antoine Chambert-Loir]

I don't think so: we have to give students something they will be credited for outside of our community.
(I checked with colleagues outside of the formalization business. They can't understand how right exactness of tensor product could be missing, nor why it took me several days to formalize it…)

[Riccardo Brasca]

I was more or less joking, but this shows we are not doing a good job (and I count myself in of course) in explaining to our colleagues why sometimes formalization is hard.

[Antoine Chambert-Loir]

It is actually hard to explain why it is hard… (and sometimes, I really don't know why it is so hard…)

[Johan Commelin]

Right exactness of the tensor product was done in the categorical language in a universe monomorphic setting, right? So now your colleagues will be even more confused... why did you need to do it again? :rofl:

[Oliver Nash]

IMHO, part of the reason formalisation is slow is that any quality mathematical exposition is slow. See "Step 3" in this MO answer and bear in mind this claim is made when a detailed set of notes have already been created.

[Oliver Nash]

Oliver Nash said:

I don't suppose anyone has proved these facts anywhere:

I caved in and did this myself #7276

[Riccardo Brasca]

Having a look.

[Anatole Dedecker]

Antoine Chambert-Loir said:

My feeling is that some people here (I count myself in them) should take the time to take some books such as Bourbaki's Algebra and Commutative Algebra and patiently and consistently add everything that is there. Possibly simultaneously writing that stuff in comprehensive form. And the more we wait for it, the more painful it will be.

I completely agree that would be a nice thing to do, and I think the first step is to have some webpage tracking the progress on that like we have for the undergrad curriculum. I just want to add the slight nuance that we shouldn't be enforcing too much the result to be in a similar form as they are in the source material, and usability in Lean should still be the main concern when stating theorems (for example we probably do not want any theorem explicitly manipulating module structures on a fixed type).

[Kevin Buzzard]

The current model ("don't do this, but add lemmas when you need them") has been working fine for years...

[Anatole Dedecker]

Well I think it's been working fine except for people who want to work in a more general setting. I think the other thread about non-commutative and non-unital rings and algebras is the prefect example of that, and I don't believe that Jireh and Eric duplicating everything that was developped in the commutative and unital case is the most efficient way we could have done that. Of course I don't blame anyone for not doing non unital rings earlier, that was absolutely a sensible thing to do, but now that we have much more experience as well as more diverse needs, I don't think we want to do the same thing again.

[Antoine Chambert-Loir]

Kevin, what you mean by “for years” is roughly 5 years, and that success is indeed remarkable. In comparison, the mathematics we grasp are sometimes 2500 years old, but have been reworked along time, sometimes massively, especially at the end of 19th century and beginning of 20th century.
What I fear, envision, or predict, is that the library will soon become too heavy to easily modify basic material. There is a parallel with what had been done at the beginning of the 20th century: at some point, it may be easier (maybe only psychologically) to start again from scratch.