Uniserial modules

This file supplies the small generic module-lattice layer needed by the multiplicity-one part of the magnitude argument. The definition and proofs are adapted from the uniserial-module reductions in quotient-submodule-equidistribution at commit 20ee4b964a9174b15304ac96485beeb73be113d8; no theorem specific to that project is imported.

theorem MagnitudeConjecture.exists_smul_one_add_eq_of_pow_smul_eq_zero {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (u : R) (b : M) (n : ℕ) (hn : u ^ n • b = 0) : ∃ (e : R), e • (1 + u) • b = b

If a scalar is nilpotent on one vector, then 1 + u is invertible on that vector by a finite geometric sum.

theorem MagnitudeConjecture.basis_sum_repr_support_erase {k : Type u} [Field k] {I : Type v} [DecidableEq I] {V : Type w} [AddCommGroup V] [Module k V] (b : Module.Basis I k V) (g : V) (p : I) (hp : p ∈ (b.repr g).support) : g = (b.repr g) p • b p + ∑ q ∈ (b.repr g).support.erase p, (b.repr g) q • b q

The basis expansion of a vector, split into one nonzero coordinate and the remaining support.

def MagnitudeConjecture.IsUniserialModule (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] : Prop

A module is uniserial when any two of its submodules are comparable.

def MagnitudeConjecture.moduleTopLinearEquiv {R : Type u} [Ring R] {M N : Type v} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M ≃ₗ[R] N) : (M ⧸ Module.jacobson R M) ≃ₗ[R] N ⧸ Module.jacobson R N

A linear equivalence induces an equivalence between module tops.

theorem MagnitudeConjecture.isSimpleModule_top_congr {R : Type u} [Ring R] {M N : Type v} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M ≃ₗ[R] N) (hM : IsSimpleModule R (M ⧸ Module.jacobson R M)) : IsSimpleModule R (N ⧸ Module.jacobson R N)

Simplicity of the module top is invariant under a linear equivalence.

theorem MagnitudeConjecture.isSimpleModule_top_quotient_of_le_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (K : Submodule R M) (hK : K ≤ Module.jacobson R M) (hM : IsSimpleModule R (M ⧸ Module.jacobson R M)) : IsSimpleModule R ((M ⧸ K) ⧸ Module.jacobson R (M ⧸ K))

Quotienting by a submodule of the radical preserves a simple top.

theorem MagnitudeConjecture.IsUniserialModule.quotient {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsUniserialModule R M) (P : Submodule R M) : IsUniserialModule R (M ⧸ P)

Quotients of uniserial modules are uniserial.

theorem MagnitudeConjecture.IsUniserialModule.submodule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsUniserialModule R M) (P : Submodule R M) : IsUniserialModule R ↥P

Submodules of uniserial modules are uniserial.

theorem MagnitudeConjecture.IsUniserialModule.smul_comparable {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsUniserialModule R M) (x y : M) : (∃ (r : R), r • x = y) ∨ ∃ (r : R), r • y = x

In a uniserial module, either of two elements is a scalar multiple of the other. This is cyclic-submodule comparability in element form.

theorem MagnitudeConjecture.IsUniserialModule.of_smul_comparable {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (h : ∀ (x y : M), (∃ (r : R), r • x = y) ∨ ∃ (r : R), r • y = x) : IsUniserialModule R M

Elementwise comparability of cyclic submodules implies uniseriality.

theorem MagnitudeConjecture.IsUniserialModule.of_surjective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (hM : IsUniserialModule R M) (f : M →ₗ[R] N) (hf : Function.Surjective ⇑f) : IsUniserialModule R N

A surjective linear image of a uniserial module is uniserial.

theorem MagnitudeConjecture.IsUniserialModule.of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (hM : IsUniserialModule R M) (f : N →ₗ[R] M) (hf : Function.Injective ⇑f) : IsUniserialModule R N

A module which embeds in a uniserial module is uniserial.

theorem MagnitudeConjecture.IsUniserialModule.congr {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (hM : IsUniserialModule R M) : IsUniserialModule R N

Uniseriality is invariant under a linear equivalence.

theorem MagnitudeConjecture.IsUniserialModule.of_subsingleton {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] : IsUniserialModule R M

Every subsingleton module is uniserial.

theorem MagnitudeConjecture.IsUniserialModule.isIndecomposableModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsUniserialModule R M) [Nontrivial M] : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M

A nonzero uniserial module is indecomposable.

theorem MagnitudeConjecture.IsUniserialModule.isSimpleModule_of_semisimple_of_isIndecomposableModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M) [IsSemisimpleModule R M] : IsSimpleModule R M

A nonzero indecomposable semisimple module is simple.

theorem MagnitudeConjecture.IsUniserialModule.top_isSimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial M] [IsArtinian R M] [IsNoetherian R M] (hM : IsUniserialModule R M) : IsSimpleModule R (M ⧸ Module.jacobson R M)

The top of a nonzero finite-length uniserial module is simple.

theorem MagnitudeConjecture.IsUniserialModule.eq_of_length_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (hM : IsUniserialModule R M) {P Q : Submodule R M} (hlength : Module.length R ↥P = Module.length R ↥Q) : P = Q

In a finite-length uniserial module, submodules of equal composition length coincide.

theorem MagnitudeConjecture.IsUniserialModule.le_jacobson_of_ne_top_of_simple_top {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) {P : Submodule R M} (hP : P ≠ ⊤) : P ≤ Module.jacobson R M

If the top of a noetherian module is simple, every proper submodule lies in its Jacobson radical.

theorem MagnitudeConjecture.IsUniserialModule.isIndecomposableModule_of_simpleTop {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] (hTop : IsSimpleModule R (M ⧸ Module.jacobson R M)) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M

A noetherian module with simple top is indecomposable.

theorem MagnitudeConjecture.IsUniserialModule.of_simpleTop_of_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] (hTop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hRadical : IsUniserialModule R ↥(Module.jacobson R M)) : IsUniserialModule R M

A noetherian module with simple top and uniserial radical is uniserial.

theorem MagnitudeConjecture.IsUniserialModule.exists_covBy_le_with_comap_eq_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (U : Submodule R M) (hU : IsUniserialModule R ↥U) {E : Submodule R M} (hE : E < U) : ∃ (C : Submodule R M), E ⋖ C ∧ C ≤ U ∧ IsUniserialModule R ↥C ∧ Submodule.comap C.subtype E = Module.jacobson R ↥C

A proper submodule of a finite-length uniserial submodule has an immediate successor whose intrinsic radical is exactly the original submodule. This is the one-step extension used in the biserial induction.