English
Let l: M → P be a bijective semilinear map with respect to a surjective ring hom σ: R →+* S between modules M over R and P over S. Then M is Noetherian as an R-module if and only if P is Noetherian as an S-module.
Русский
Пусть l: M → P является биективной полилинейной картой относительно сюръективного гомоморфизма колец σ: R →+* S между модулями M над R и P над S. Тогда M является Ноетеровым как R-модуль тогда и только тогда, когда P является Ноетеровым как S-модуль.
LaTeX
$$$IsNoetherian(R,M) \iff IsNoetherian(S,P)$$$
Lean4
theorem isNoetherian_iff_of_bijective {S P} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S}
[RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective l) : IsNoetherian R M ↔ IsNoetherian S P :=
by
simp_rw [isNoetherian_iff']
let e := Submodule.orderIsoMapComapOfBijective l hl
exact ⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩
