surjective_of_injective_endomorphism

English

If f is a linear equivalence, Artinian property is preserved in both directions.

Русский

Если f — линейное эквивалентное отображение, тогда артинановость сохраняется и наоборот.

LaTeX

$$$IsArtinian\\ R\\ M \\iff IsArtinian\\ R\\ P$$$

Lean4

/-- Any injective endomorphism of an Artinian module is surjective. -/
theorem surjective_of_injective_endomorphism (f : M →ₗ[R] M) (s : Injective f) : Surjective f :=
  by
  have h := ‹IsArtinian R M›; contrapose! h
  rw [IsArtinian, WellFoundedLT, isWellFounded_iff]
  refine (RelEmbedding.natGT (LinearMap.range <| f ^ ·) ?_).not_wellFounded
  intro n
  simp_rw [pow_succ, Module.End.mul_eq_comp, LinearMap.range_comp, ← Submodule.map_top (f ^ n)]
  refine Submodule.map_strictMono_of_injective (Module.End.iterate_injective s n) (Ne.lt_top ?_)
  rwa [Ne, LinearMap.range_eq_top]

Похожие утверждения