isSimpleModule_iff_of_bijective — Mathlib

English

Let l: M →ₛₗ[σ] N be a semilinear bijection for some surjective σ: R →+* S. Then M is a simple R-module iff N is a simple S-module.

Русский

Пусть l: M →ₛₗ[σ] N --- полносвязное сепролинейное отображение для сюръективного гомоморфизма σ: R →+* S. Тогда M прост как R-модуль тогда и только тогда, когда N прост как S-модуль.

LaTeX

$$$\\text{IsSimpleModule } R M \\;\\iff\\; \\text{IsSimpleModule } S N$$$

Lean4

theorem isSimpleModule_iff_of_bijective [Module S N] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] N)
    (hl : Function.Bijective l) : IsSimpleModule R M ↔ IsSimpleModule S N := by
  simp_rw [isSimpleModule_iff, (Submodule.orderIsoMapComapOfBijective l hl).isSimpleOrder_iff]

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