Commit 2024-06-04 13:17 a7569c03
View on Github →feat: left-Noetherian rings and commutative rings satisfy OrzechProperty
(#13425)
This is part 2 of #12076.
It states that if
R
is a ring (not necessarily commutative) andM
is a NoetherianR
-module (based on the proof in https://math.stackexchange.com/a/1066128), orR
is a commutative ring andM
is a finitely generatedR
-module (based on the proof in https://math.stackexchange.com/a/1066110), ifN
is a submodule ofM
,f : N -> M
is a surjectiveR
-module homomorphism, then it is also injective. These results generalize(IsNoetherian|Module.Finite).injective_of_surjective_endomorphism
. The proof for Noetherian case usesLinearMap.iterateMapComap
which is put intoMathlib/Algebra/Module/Submodule/IterateMapComap.lean
. The changed proof makesLinearMap.tunnel
andLinearMap.tailing
not used in any other parts of mathlib. Remove them or not is leaved for future discussion.