isArtinian_iff_of_bijective — Mathlib

English

If a linear map between modules is bijective and the target is Artinian, then the source is Artinian, and vice versa.

Русский

Если линейное отображение между модулями биективно, и целевой модуль артинан, тогда источник артинан, и наоборот.

LaTeX

$$$\\mathrm{IsArtinian}_R M \\leftrightarrow \\mathrm{IsArtinian}_S P$ for a bijective linear map $l:M\\to P$ with suitable base change.$$

Lean4

theorem isArtinian_iff_of_bijective {S P} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S}
    [RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective l) : IsArtinian R M ↔ IsArtinian S P :=
  let e := Submodule.orderIsoMapComapOfBijective l hl
  ⟨fun _ ↦ e.symm.strictMono.wellFoundedLT, fun _ ↦ e.strictMono.wellFoundedLT⟩

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