isNoetherian_linearMap — Mathlib

English

An alternative noetherian_pi' instance: if M is Noetherian and ι finite, then the space of linear maps from ι → M is Noetherian.

Русский

Альтернативная версия: если M Noetherian и ι конечен, пространство линейных отображений из ι → R в M — Noetherian.

LaTeX

$$$[IsNoetherian R M] \Rightarrow IsNoetherian R (ι \to M)$$$

Lean4

instance isNoetherian_linearMap : IsNoetherian R (N →ₗ[R] M) :=
  by
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N
  let g : (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M := (LinearMap.llcomp R (Fin n → R) N M).flip f
  exact isNoetherian_of_injective g hf.injective_linearMapComp_right

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