English
If M has finite length and f: M → N is surjective, then N has finite length.
Русский
Если M имеет конечную длину и отображение f: M → N сюръективно, тогда N имеет конечную длину.
LaTeX
$$$\\displaystyle \\text{IsFiniteLength } R M \\land \\text{Function.Surjective } f \\Rightarrow \\text{IsFiniteLength } R N$$$
Lean4
theorem of_surjective (H : IsFiniteLength R M) (hf : Function.Surjective f) : IsFiniteLength R N :=
by
rw [isFiniteLength_iff_isNoetherian_isArtinian] at H ⊢
cases H
exact
⟨isNoetherian_of_surjective _ f (LinearMap.range_eq_top.mpr hf), isArtinian_of_surjective _ f hf⟩
/- The following instances are now automatic:
example [IsSemisimpleRing R] : IsNoetherianRing R := inferInstance
example [IsSemisimpleRing R] : IsArtinianRing R := inferInstance
-/
