isArtinian_of_surjective — Mathlib

English

If f: M → P is surjective and M is Artinian over R, then P is Artinian over R.

Русский

Если отображение сюрьективно и M артин, тогда P артин.

LaTeX

$$$\\mathrm{isArtinian}_R(M) \\to \\mathrm{IsArtinian}_R(P)$ for surjective linear map f.$$

Lean4

theorem isArtinian_of_surjective (f : M →ₗ[R] P) (hf : Function.Surjective f) [IsArtinian R M] : IsArtinian R P :=
  ⟨Subrelation.wf (fun {A B} hAB => show A.comap f < B.comap f from Submodule.comap_strictMono_of_surjective hf hAB)
      (InvImage.wf (Submodule.comap f) IsWellFounded.wf)⟩

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