Simple modules over division rings

This file contains some results about simple modules over division rings.

Main results

• DivisionRing.nonempty_linearEquiv_of_isSimpleModule : There is an unique simple module over a division ring, up to isomorphism.
• isSimpleModule_iff_eq_zero_or_injective : A module is simple if and only if it is nontrivial and every linear map from it is either zero or injective, this is the module analogue of RingHom.injective
• IsSimpleModule.obj_of_isEquivalence : If M is a simple module over a ring R, and e : ModuleCat R ⥤ ModuleCat S is an equivalence of categories, then e(M) is a simple module over S.

Tags

Noncommutative algebra, simple module, division ring

theorem DivisionRing.nonempty_linearEquiv_of_isSimpleModule (S : Type u_2) [DivisionRing S] (N : Type u_3) [AddCommGroup N] [Module S N] [IsSimpleModule S N] : Nonempty (N ≃ₗ[S] S)

theorem isSimpleModule_iff_eq_zero_or_injective (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : IsSimpleModule R M ↔ Nontrivial M ∧ ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f

theorem IsSimpleModule.obj_of_isEquivalence {R : Type u_3} {S : Type u_4} [Ring R] [Ring S] (e : CategoryTheory.Functor (ModuleCat R) (ModuleCat S)) [e.IsEquivalence] (M : ModuleCat R) [IsSimpleModule R ↑M] : IsSimpleModule S ↑(e.obj M)