Semiprimary rings

Main definition

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

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 = ⊥

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 = ⊥

theorem IsSemisimpleRing.jacobson_eq_bot (R : Type u_1) [Ring R] [IsSemisimpleRing R] : Ring.jacobson R = ⊥

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 τ₁₂] [IsSemisimpleModule R₂ M₂] (f : M →ₛₗ[τ₁₂] M₂) : Module.jacobson R M ≤ f.ker

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.

@[instance 100]

instance instIsReducedOfIsSemisimpleRing (R : Type u_5) [CommRing R] [IsSemisimpleRing R] : IsReduced R

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)

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