Theorems · Theorem · commutative algebra

IsNoetherian.injective_of_surjective_of_injective

∀ {R : Type u_1} {M : Type u_2} {N : Type w} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsNoetherian R M] (i f : N →ₗ[R] M),
  Function.Injective ⇑i → Function.Surjective ⇑f → Function.Injective ⇑f

Orzech's theorem for Noetherian modules: if R is a ring (not necessarily commutative), M and N are R-modules, M is Noetherian, i : N →ₗ[R] M is injective, f : N →ₗ[R] M is surjective, then f is also injective. The proof here is adapted from Djoković's paper Epimorphisms of modules which must be isomorphisms [djokovic1973], utilizing LinearMap.iterateMapComap. See also Orzech's original paper: Onto endomorphisms are isomorphisms [orzech1971].

Defined in

Mathlib.RingTheory.Noetherian.Orzech

Cited by

3 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModuleIsNoetherian