surjective endomorphism of a noetherian module is injective?

Stream: Is there code for X?

[Scott Morrison]

Do we have the result that a surjective endomorphism of a Noetherian module is injective?

[Scott Morrison]

For that matter, do we have the "conventional" definition of a Noetherian module (increasing chain of submodules stabilizes), beyond the statement that > on submodules is well-founded? I appreciate that these are "the same", but presumably it's not considered verboten to use the conventional formulation.

[Mario Carneiro]

There is a theorem along those lines for well founded

[Scott Morrison]

But not spelled out for is_noetherian.

[Scott Morrison]

I see there is src#set_has_maximal_iff_noetherian.

[Mario Carneiro]

docs#well_founded.monotone_chain_condition

[Mario Carneiro]

if you combine that with docs#is_noetherian_iff_well_founded you should get the desired statement

[Mario Carneiro]

also docs#rel_embedding.well_founded_iff_no_descending_seq which is a slight variant

[Scott Morrison]

Great, thank you. If anyone can explain to me how to prove the headline result above (surjective endomorphisms of Noetherian modules are injective) without resorting to an ascending chain of submodules, but just directly using the induction principle or well-foundedness, I will have learnt something. :-)

[Scott Morrison]

And in the meantime I'll go off and prove it the low-brow way. :-)

[Scott Morrison]

#7676