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) and M is a Noetherian R-module (based on the proof in https://math.stackexchange.com/a/1066128), or
  • R is a commutative ring and M is a finitely generated R-module (based on the proof in https://math.stackexchange.com/a/1066110), if N is a submodule of M, f : N -> M is a surjective R-module homomorphism, then it is also injective. These results generalize (IsNoetherian|Module.Finite).injective_of_surjective_endomorphism. The proof for Noetherian case uses LinearMap.iterateMapComap which is put into Mathlib/Algebra/Module/Submodule/IterateMapComap.lean. The changed proof makes LinearMap.tunnel and LinearMap.tailing not used in any other parts of mathlib. Remove them or not is leaved for future discussion.

Estimated changes