Simple and semisimple modules: multiplication by n, products and endomorphisms

Mathlib closes IsSemisimpleModule under submodules, quotients, Finsupp, and finite dependent products Π i, M i. The dependent product covers a binary product only when both factors lie in the same universe, since the family M : ι → Type u is universe-monomorphic; this file supplies the binary case with the two factors in unrelated universes.

For a simple module it records that multiplication by a natural number is all-or-nothing: multiplication by n is the R-linear endomorphism n • LinearMap.id, so its kernel is an R-submodule, hence ⊥ or ⊤, and n either kills no nonzero element or kills every element.

It also records which elements of a semisimple module an endomorphism can connect: some R-linear endomorphism sends w to x exactly when every scalar killing w kills x. This criterion turns reachability under endomorphisms into a containment between torsion ideals, a form useful in centralizer arguments.

Main results

• Ado.forall_nsmul_eq_zero_of_ne_zero_of_nsmul_eq_zero: in a simple module, a natural number killing one nonzero element kills every element.
• Ado.IsSemisimpleModule.prod: a product of two semisimple modules is semisimple.
• Ado.IsSemisimpleModule.exists_end_apply_eq_iff: in a semisimple module, an endomorphism sends w to x if and only if the torsion ideal of w is contained in that of x.

theorem Ado.forall_nsmul_eq_zero_of_ne_zero_of_nsmul_eq_zero {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSimpleModule R M] {n : ℕ} {m₀ : M} (hm₀ : m₀ ≠ 0) (h : n • m₀ = 0) (m : M) : n • m = 0

In a simple module a natural number that kills one nonzero element kills every element. Multiplication by n is the R-linear endomorphism n • LinearMap.id, so its kernel is an R-submodule; a nonzero element of that kernel keeps it from being ⊥, and in a simple module it is then ⊤.

instance Ado.IsSemisimpleModule.prod {R : Type u_1} {M : Type u_2} {N : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsSemisimpleModule R M] [IsSemisimpleModule R N] : IsSemisimpleModule R (M × N)

A product of two semisimple modules is semisimple.

theorem Ado.IsSemisimpleModule.exists_end_apply_eq_iff {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] {w x : M} : (∃ (f : Module.End R M), f w = x) ↔ Ideal.torsionOf R M w ≤ Ideal.torsionOf R M x

Endomorphisms between two elements of a semisimple module. Some R-linear endomorphism of a semisimple module sends w to x exactly when every scalar annihilating w annihilates x, that is, when Ideal.torsionOf R M w ≤ Ideal.torsionOf R M x.