English
If I is two-sided and hM : IsTorsionBySet R M I, then IsSemisimpleModule (R/I) M iff IsSemisimpleModule R M.
Русский
Если I двусторонний и hM имеет IsTorsionBySet, то IsSemisimpleModule (R/I) M эквивалентно IsSemisimpleModule R M.
LaTeX
$$$[I.IsTwoSided]\\; (hM:IsTorsionBySet R M I)\\;\\Rightarrow\\; IsSemisimpleModule (R \\ slash I) M \\iff IsSemisimpleModule R M$$$
Lean4
/-- If a `R`-module `M` is annihilated by a two-sided ideal `I`, then the identity is a semilinear
map from the `R`-module `M` to the `R ⧸ I`-module `M`. -/
def semilinearMap [I.IsTwoSided] (hM : IsTorsionBySet R M I) :
let _ := hM.module;
M →ₛₗ[Ideal.Quotient.mk I] M :=
let _ := hM.module
{ toFun := id
map_add' := fun _ _ ↦ rfl
map_smul' := fun _ _ ↦ rfl }
