The radical of a module is the radical of its submodule lattice

Module.jacobson R M is defined as the infimum of the maximal submodules of M, and Order.radical of a lattice is defined as the infimum of its coatoms. For the lattice Submodule R M these are the same infimum, but Mathlib defines the two independently and states no lemma connecting them. This file supplies that bridge, which makes the general Order.radical API — notably Order.radical_nongenerating — available for Module.jacobson.

Main results

• TauCeti.Module.jacobson_eq_radical: Module.jacobson R M = Order.radical (Submodule R M).

theorem TauCeti.Module.jacobson_eq_radical (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : Module.jacobson R M = Order.radical (Submodule R M)

The Jacobson radical of a module is the order radical of its submodule lattice: both are the infimum of the coatoms. Mathlib defines the two independently and states no lemma connecting them.