Iterated module radicals

This file packages the radical filtration of a module as actual submodules of the original module. The formulation is tailored to the radical-layer argument in Auslander--Reiten, Proposition 1.1(a): a finite radical filtration whose nonzero tops are simple is uniserial.

def MagnitudeConjecture.iteratedModuleJacobson (R : Type u) [Ring R] (M : Type v) [AddCommGroup M] [Module R M] : ℕ → Submodule R M

The nth term of the module radical filtration, retained as a submodule of the original module.

@[simp]

theorem MagnitudeConjecture.iteratedModuleJacobson_zero {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] : iteratedModuleJacobson R M 0 = ⊤

@[simp]

theorem MagnitudeConjecture.iteratedModuleJacobson_succ {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (n : ℕ) : iteratedModuleJacobson R M (n + 1) = Submodule.map (iteratedModuleJacobson R M n).subtype (Module.jacobson R ↥(iteratedModuleJacobson R M n))

theorem MagnitudeConjecture.iteratedModuleJacobson_succ_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (n : ℕ) : iteratedModuleJacobson R M (n + 1) ≤ iteratedModuleJacobson R M n

Consecutive terms of the radical filtration are nested.

theorem MagnitudeConjecture.iteratedModuleJacobson_map_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (n : ℕ) : Submodule.map f (iteratedModuleJacobson R M n) ≤ iteratedModuleJacobson R N n

A linear map carries each term of the radical filtration into the corresponding term.

theorem MagnitudeConjecture.iteratedModuleJacobson_eq_ringJacobson_pow_smul_top {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] (n : ℕ) : iteratedModuleJacobson R M n = Ring.jacobson R ^ n • ⊤

Each iterated radical is the corresponding power of the ring Jacobson radical acting on the module.

theorem MagnitudeConjecture.iteratedModuleJacobson_map_eq_of_surjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] [IsSemiprimaryRing R] (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) (n : ℕ) : Submodule.map f (iteratedModuleJacobson R M n) = iteratedModuleJacobson R N n

A surjective linear map carries each radical-filtration term onto the corresponding term.

theorem MagnitudeConjecture.iteratedModuleJacobson_apply_mem_succ_of_range_le_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] [IsSemiprimaryRing R] (f : M →ₗ[R] N) (hf : f.range ≤ Module.jacobson R N) (n : ℕ) {x : M} (hx : x ∈ iteratedModuleJacobson R M n) : f x ∈ iteratedModuleJacobson R N (n + 1)

If the whole image of a map lies in the target radical, the map shifts the radical filtration by one step.

theorem MagnitudeConjecture.iteratedModuleJacobson_eventually_eq_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] : ∃ (n : ℕ), iteratedModuleJacobson R M n = ⊥

Over a semiprimary ring, the radical filtration terminates.

theorem MagnitudeConjecture.exists_incomparable_submodules_of_semisimple_not_simple {R : Type u} [Ring R] {E : Type v} [AddCommGroup E] [Module R E] [Nontrivial E] [IsSemisimpleModule R E] (hnot : ¬IsSimpleModule R E) : ∃ (P : Submodule R E) (Q : Submodule R E), ¬P ≤ Q ∧ ¬Q ≤ P

A non-simple nonzero semisimple module contains two incomparable submodules.

theorem MagnitudeConjecture.isUniserialModule_of_iteratedJacobson_tops_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] (bound : ℕ) (hbot : iteratedModuleJacobson R M bound = ⊥) (hsimple : ∀ n < bound, iteratedModuleJacobson R M n ≠ ⊥ → IsSimpleModule R (↥(iteratedModuleJacobson R M n) ⧸ Module.jacobson R ↥(iteratedModuleJacobson R M n))) : IsUniserialModule R M

If a finite radical filtration has simple nonzero tops at every stage, then its initial module is uniserial.

theorem MagnitudeConjecture.exists_incomparable_over_jacobson_of_not_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] [IsNoetherian R M] (hM : ¬IsUniserialModule R M) : ∃ (n : ℕ) (K : Submodule R ↥(iteratedModuleJacobson R M n)) (L : Submodule R ↥(iteratedModuleJacobson R M n)), Module.jacobson R ↥(iteratedModuleJacobson R M n) ≤ K ∧ Module.jacobson R ↥(iteratedModuleJacobson R M n) ≤ L ∧ ¬K ≤ L ∧ ¬L ≤ K

A nonuniserial noetherian module over a semiprimary ring has a radical layer containing two incomparable submodules. The returned submodules live in the corresponding term of the radical filtration and contain its intrinsic radical.

theorem MagnitudeConjecture.exists_incomparable_between_iteratedJacobson_of_not_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] [IsNoetherian R M] (hM : ¬IsUniserialModule R M) : ∃ (n : ℕ) (K : Submodule R M) (L : Submodule R M), iteratedModuleJacobson R M (n + 1) ≤ K ∧ iteratedModuleJacobson R M (n + 1) ≤ L ∧ K ≤ iteratedModuleJacobson R M n ∧ L ≤ iteratedModuleJacobson R M n ∧ ¬K ≤ L ∧ ¬L ≤ K

Ambient form of the preceding radical-layer witness.

theorem MagnitudeConjecture.quotientMap_sub_comp_range_not_le_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsSemiprimaryRing R] {n : ℕ} {K L : Submodule R M} (hnextK : iteratedModuleJacobson R M (n + 1) ≤ K) (hLn : L ≤ iteratedModuleJacobson R M n) (hLK : ¬L ≤ K) (t : M ⧸ L →ₗ[R] M ⧸ K) : ¬(K.mkQ - t ∘ₗ L.mkQ).range ≤ Module.jacobson R (M ⧸ K)

For incomparable intermediate submodules in one radical layer, a quotient map cannot differ from a map through the other quotient by a map whose image lies in the target radical.