Jacobson radical of modules and rings #
Main definitions #
Module.jacobson R M: the Jacobson radical of a module M over a ring R is defined to be the
intersection of all maximal submodules of M.
Ring.jacobson R: the Jacobson radical of a ring R is the Jacobson radical of R as
an R-module, which is equal to the intersection of all maximal left ideals of R. It turns out
it is in fact a two-sided ideal, and equals the intersection of all maximal right ideals of R.
Reference #
- [F. Lorenz, Algebra: Volume II: Fields with Structure, Algebras and Advanced Topics][Lorenz2008]
theorem
Module.le_comap_jacobson
{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)
:
theorem
Module.map_jacobson_le
{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)
:
theorem
Module.jacobson_eq_bot_of_injective
{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)
(inj : Function.Injective ⇑f)
(h : jacobson R₂ M₂ = ⊥)
:
theorem
Module.map_jacobson_of_ker_le
{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}
(surj : Function.Surjective ⇑f)
(le : LinearMap.ker f ≤ jacobson R M)
:
theorem
Module.comap_jacobson_of_ker_le
{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}
(surj : Function.Surjective ⇑f)
(le : LinearMap.ker f ≤ jacobson R M)
:
theorem
Module.map_jacobson_of_bijective
{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}
(hf : Function.Bijective ⇑f)
:
theorem
Module.comap_jacobson_of_bijective
{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}
(hf : Function.Bijective ⇑f)
:
theorem
Module.jacobson_lt_top
(R : Type u_1)
(M : Type u_3)
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial M]
[IsCoatomic (Submodule R M)]
:
theorem
Module.jacobson_pi_le
(R : Type u_1)
[Ring R]
{ι : Type u_7}
(M : ι → Type u_6)
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
:
theorem
Module.jacobson_pi_eq_bot
(R : Type u_1)
[Ring R]
{ι : Type u_7}
(M : ι → Type u_6)
[(i : ι) → AddCommGroup (M i)]
[(i : ι) → Module R (M i)]
(h : ∀ (i : ι), jacobson R (M i) = ⊥)
:
A product of modules with trivial Jacobson radical (e.g. simple modules) also has trivial Jacobson radical.
@[reducible, inline]
The Jacobson radical of a ring R is the Jacobson radical of R as an R-module.
Equations
- Ring.jacobson R = Module.jacobson R R
Instances For
theorem
Ring.le_comap_jacobson
{R : Type u_1}
{R₂ : Type u_2}
[Ring R]
[Ring R₂]
(f : R →+* R₂)
[RingHomSurjective f]
:
theorem
Ring.map_jacobson_le
{R : Type u_1}
{R₂ : Type u_2}
[Ring R]
[Ring R₂]
(f : R →+* R₂)
[RingHomSurjective f]
:
theorem
Ring.map_jacobson_of_ker_le
{R : Type u_1}
{R₂ : Type u_2}
[Ring R]
[Ring R₂]
{f : R →+* R₂}
[RingHomSurjective f]
(le : RingHom.ker f ≤ jacobson R)
:
theorem
Ring.jacobson_quotient_of_le
{R : Type u_1}
[Ring R]
{I : Ideal R}
[I.IsTwoSided]
(le : I ≤ jacobson R)
:
theorem
Ring.jacobson_smul_top_le
(R : Type u_1)
[Ring R]
(M : Type u_3)
[AddCommGroup M]
[Module R M]
:
theorem
Submodule.jacobson_smul_lt_top
{R : Type u_1}
[Ring R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
[Nontrivial M]
[IsCoatomic (Submodule R M)]
(N : Submodule R M)
:
theorem
Submodule.FG.jacobson_smul_lt
{R : Type u_1}
[Ring R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{N : Submodule R M}
(ne_bot : N ≠ ⊥)
(fg : N.FG)
:
theorem
Submodule.FG.eq_bot_of_le_jacobson_smul
{R : Type u_1}
[Ring R]
{M : Type u_3}
[AddCommGroup M]
[Module R M]
{N : Submodule R M}
(fg : N.FG)
(le : N ≤ Ring.jacobson R • N)
:
A form of Nakayama's lemma for modules over noncommutative rings.