simple_iff_isSimpleModule
theorem simple_iff_isSimpleModule :
∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
CategoryTheory.Simple (ModuleCat.of R M) ↔ IsSimpleModule R M
The theorem `simple_iff_isSimpleModule` states that, for any ring `R` and any `M` such that `M` forms a commutative addition group and is a module over `R`, a module `M` is simple in the category of `R`-modules if and only if `M` is simple as an `R`-module. Here, a module is considered simple in the category if it is simple as an object in this category, and it is considered simple as an `R`-module if it has only two submodules: the zero submodule (`⊥`) and the entire module itself (`⊤`).
More concisely: A module over a ring is simple in the category of `R`-modules if and only if it is a simple `R`-module.
|
simple_of_finrank_eq_one
theorem simple_of_finrank_eq_one :
∀ {R : Type u_1} [inst : Ring R] {k : Type u_3} [inst_1 : Field k] [inst_2 : Algebra k R] {V : ModuleCat R},
FiniteDimensional.finrank k ↑V = 1 → CategoryTheory.Simple V
This theorem states that for any `k`-algebra module `V`, which is over a ring `R` and a field `k`, if `V` is 1-dimensional over `k` (i.e., the rank of the module `V` over `k` is 1), then `V` is a simple module. In algebra, a module is called simple if it has no non-trivial submodules; here the theorem ensures this property for `V` when it's one-dimensional over the field `k`.
More concisely: A 1-dimensional `k`-algebra module over a ring `R` and a field `k` is a simple module.
|