isNoetherian_of_surjective, of_exact (and artin of exact)

Stream: Is there code for X?

[Jz Pan]

Seems that isNoetherian_of_surjective is missing from mathlib. The other three combinations are in mathlib. Both of Noetherian and Artinian have no exact version.

[Joël Riou]

In the categorical context (Noetherian objects in abelian categories), mathlib shall soon know that noetherian objects form a Serre class #22367.

[Jz Pan]

Oh I see.

[Jz Pan]

By the way, personally I am a little bit against the idea that resort everything to category theory even for most basic things in Lean. It's perfectly OK for informal math, but in Lean there will be larger import problem, and universe level problem (every object in a category must be in the same universe level, whereas if the result is writing manually, then each module could live in different universes).