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]

def Module.jacobson (R : Type u_1) (M : Type u_3) [Ring R] [AddCommGroup M] [Module R M] : Submodule R M

The Jacobson radical of an R-module M is the infimum of all maximal submodules in M.

Equations

• Module.jacobson R M = sInf {m : Submodule R M | IsCoatom m}

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

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

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 : M →ₛₗ[τ₁₂] M₂) (inj : Function.Injective ⇑f) (h : jacobson R₂ M₂ = ⊥) : 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 : M →ₛₗ[τ₁₂] M₂} (surj : Function.Surjective ⇑f) (le : f.ker ≤ jacobson R M) : Submodule.map f (jacobson R M) = 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 : M →ₛₗ[τ₁₂] M₂} (surj : Function.Surjective ⇑f) (le : f.ker ≤ jacobson R M) : Submodule.comap f (jacobson R₂ M₂) = 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 : M →ₛₗ[τ₁₂] M₂} (hf : Function.Bijective ⇑f) : Submodule.map f (jacobson R M) = jacobson R₂ M₂

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 : M →ₛₗ[τ₁₂] M₂} (hf : Function.Bijective ⇑f) : Submodule.comap f (jacobson R₂ M₂) = jacobson R M

theorem Module.jacobson_quotient_of_le {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} (le : N ≤ jacobson R M) : jacobson R (M ⧸ N) = Submodule.map N.mkQ (jacobson R M)

theorem Module.jacobson_le_of_eq_bot {R : Type u_1} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {N : Submodule R M} (h : jacobson R (M ⧸ N) = ⊥) : jacobson R M ≤ N

@[simp]

theorem Module.jacobson_quotient_jacobson (R : Type u_1) (M : Type u_3) [Ring R] [AddCommGroup M] [Module R M] : jacobson R (M ⧸ jacobson R M) = ⊥

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)] : jacobson R M < ⊤

theorem Module.jacobson_pi_le (R : Type u_1) [Ring R] {ι : Type u_6} (M : ι → Type u_5) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] : jacobson R ((i : ι) → M i) ≤ Submodule.pi Set.univ fun (x : ι) => jacobson R (M x)

theorem Module.jacobson_pi_eq_bot (R : Type u_1) [Ring R] {ι : Type u_6} (M : ι → Type u_5) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] (h : ∀ (i : ι), jacobson R (M i) = ⊥) : jacobson R ((i : ι) → M i) = ⊥

A product of modules with trivial Jacobson radical (e.g. simple modules) also has trivial Jacobson radical.

@[reducible, inline]

abbrev Ring.jacobson (R : Type u_1) [Ring R] : Ideal R

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

theorem Ring.jacobson_eq_sInf_isMaximal (R : Type u_1) [Ring R] : jacobson R = sInf {I : Ideal R | I.IsMaximal}

instance Ring.instIsTwoSidedJacobson (R : Type u_1) [Ring R] : (jacobson R).IsTwoSided

theorem Ring.jacobson_le_of_isMaximal {R : Type u_1} [Ring R] (m : Ideal R) [m.IsMaximal] : jacobson R ≤ m

theorem Ring.le_comap_jacobson {R : Type u_1} {R₂ : Type u_2} [Ring R] [Ring R₂] (f : R →+* R₂) [RingHomSurjective f] : jacobson R ≤ Ideal.comap f (jacobson R₂)

theorem Ring.map_jacobson_le {R : Type u_1} {R₂ : Type u_2} [Ring R] [Ring R₂] (f : R →+* R₂) [RingHomSurjective f] : Submodule.map f.toSemilinearMap (jacobson R) ≤ jacobson R₂

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) : Submodule.map f.toSemilinearMap (jacobson R) = jacobson R₂

theorem Ring.coe_jacobson_quotient {R : Type u_1} [Ring R] (I : Ideal R) [I.IsTwoSided] : ↑(jacobson (R ⧸ I)) = ↑(Module.jacobson R (R ⧸ I))

theorem Ring.jacobson_quotient_of_le {R : Type u_1} [Ring R] {I : Ideal R} [I.IsTwoSided] (le : I ≤ jacobson R) : jacobson (R ⧸ I) = Submodule.map (Ideal.Quotient.mk I).toSemilinearMap (jacobson R)

theorem Ring.jacobson_le_of_eq_bot {R : Type u_1} [Ring R] {I : Ideal R} [I.IsTwoSided] (h : jacobson (R ⧸ I) = ⊥) : jacobson R ≤ I

@[simp]

theorem Ring.jacobson_quotient_jacobson (R : Type u_1) [Ring R] : jacobson (R ⧸ jacobson R) = ⊥

theorem Ring.jacobson_lt_top (R : Type u_1) [Ring R] [Nontrivial R] : jacobson R < ⊤

theorem Ring.jacobson_smul_top_le (R : Type u_1) [Ring R] (M : Type u_3) [AddCommGroup M] [Module R M] : jacobson R • ⊤ ≤ Module.jacobson 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) : Ring.jacobson R • N < ⊤

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) : Ring.jacobson R • N < N

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) : N = ⊥

A form of Nakayama's lemma for modules over noncommutative rings.