top_ne_ideal_smul_of_le_jacobson_annihilator

English

If I is contained in the Jacobson radical, then the top submodule is not equal to I·top.

Русский

Если I лежит в Jacobson радикале, то верхний подмодуль не равен I·верхний.

LaTeX

$$$$ \\top \\neq I \\cdot \\top, \\text{ if } I \\le \\operatorname{jacobson} . \\top. $$$$

Lean4

theorem top_ne_ideal_smul_of_le_jacobson_annihilator [Nontrivial M] [Module.Finite R M] {I}
    (h : I ≤ (Module.annihilator R M).jacobson) : (⊤ : Submodule R M) ≠ I • ⊤ := fun H =>
  top_ne_bot <|
    eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator Module.Finite.fg_top H <|
      (congrArg (I ≤ Ideal.jacobson ·) annihilator_top).mpr h

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