isSemisimpleModule_iff — Mathlib

English

Under the IsTorsionBySet assumption, the semisimple property of M as an R-module equals the semisimple property of M as an R/I-module, via the semilinear map.

Русский

При предположении IsTorsionBySet свойство полносильности M как R-модуля равно полносильности M как модуля над R/I через полус линейное отображение.

LaTeX

$$$IsSemisimpleModule (R/I) M \\iff IsSemisimpleModule R M$$$

Lean4

theorem isSemisimpleModule_iff [I.IsTwoSided] (hM : Module.IsTorsionBySet R M I) :
    let _ := hM.module
    IsSemisimpleModule (R ⧸ I) M ↔ IsSemisimpleModule R M :=
  let _ := hM.module
  (hM.semilinearMap.isSemisimpleModule_iff_of_bijective Function.bijective_id).symm

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