# Semiprimary rings #

## Main definition #

- `IsSemiprimaryRing R`: a ring `R` is semiprimary if `Ring.jacobson R` is nilpotent and `R ⧸ Ring.jacobson R` is semisimple.

source
theorem IsSimpleModule.jacobson_eq_bot (R : Type u_1) (M : Type u_3) [Ring R] [AddCommGroup M] [Module R M] [IsSimpleModule R M] :
Module.jacobson R M = ⊥
source
theorem IsSemisimpleModule.jacobson_eq_bot (R : Type u_1) (M : Type u_3) [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :
Module.jacobson R M = ⊥
source
theorem IsSemisimpleRing.jacobson_eq_bot (R : Type u_1) [Ring R] [IsSemisimpleRing R] :
Ring.jacobson R = ⊥
source
theorem IsSemisimpleModule.jacobson_le_ker (R : Type u_1) (R₂ : Type u_2) (M : Type u_3) (M₂ : Type u_4) [Ring R] [Ring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_5} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) [IsSemisimpleModule R₂ M₂] :
Module.jacobson R M ≤ LinearMap.ker f
source
theorem IsSemisimpleModule.jacobson_le_annihilator (R : Type u_1) (M : Type u_3) [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :
Ring.jacobson R ≤ Module.annihilator R M

The Jacobson radical of a ring annihilates every semisimple module.

source
@[instance 100]
instance instIsReducedOfIsSemisimpleRing (R : Type u_6) [CommRing R] [IsSemisimpleRing R] :
IsReduced R
source
class IsSemiprimaryRing (R : Type u_1) [Ring R] :
Prop

A ring is semiprimary if its Jacobson radical is nilpotent and its quotient by the Jacobson radical is semisimple.

- isSemisimpleRing : IsSemisimpleRing (R ⧸ Ring.jacobson R)
- isNilpotent : IsNilpotent (Ring.jacobson R)

Instances

source
theorem isSemiprimaryRing_iff (R : Type u_1) [Ring R] :
IsSemiprimaryRing R ↔ IsSemisimpleRing (R ⧸ Ring.jacobson R) ∧ IsNilpotent (Ring.jacobson R)