jacobson_eq_bot — Mathlib

English

If M is a semisimple module over R, then its Jacobson radical is the zero submodule.

Русский

Если M — полупростой модуль над R, то его радикал Якобсона равен нулю.

LaTeX

$$Module.jacobson R M = ⊥$$

Lean4

theorem jacobson_eq_bot [IsSemisimpleModule R M] : Module.jacobson R M = ⊥ :=
  have ⟨s, e, simple⟩ := isSemisimpleModule_iff_exists_linearEquiv_dfinsupp.mp ‹_›
  let f : M →ₗ[R] ∀ m : s, m.1 := (LinearMap.pi DFinsupp.lapply).comp e.toLinearMap
  Module.jacobson_eq_bot_of_injective f (DFinsupp.injective_pi_lapply (R := R).comp e.injective)
    (Module.jacobson_pi_eq_bot _ _ fun i ↦ IsSimpleModule.jacobson_eq_bot R _)

Похожие утверждения