Socles of finite-length modules

This file supplies the intrinsic dual of the simple-top interface used in the Pogorzały--Skowroński induction. The socle is the sum of all simple submodules. In an Artinian module it meets every nonzero submodule, so a simple socle forces indecomposability.

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

The socle of a module, realized as the sum of all its simple submodules.

theorem MagnitudeConjecture.moduleSocle_isSemisimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] : IsSemisimpleModule R ↥(moduleSocle R M)

The socle, being the sum of the simple submodules, is semisimple.

theorem MagnitudeConjecture.le_moduleSocle_of_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (S : Submodule R M) (hS : IsSimpleModule R ↥S) : S ≤ moduleSocle R M

Every simple submodule is contained in the socle.

theorem MagnitudeConjecture.isSimpleModule_map_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (S : Submodule R M) (hS : IsSimpleModule R ↥S) : IsSimpleModule R ↥(Submodule.map f S)

The image of a simple submodule under an injective linear map is simple.

theorem MagnitudeConjecture.map_eq_bot_or_isSimpleModule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (S : Submodule R M) (hS : IsSimpleModule R ↥S) : Submodule.map f S = ⊥ ∨ IsSimpleModule R ↥(Submodule.map f S)

The image of a simple submodule under an arbitrary linear map is either zero or simple.

theorem MagnitudeConjecture.map_moduleSocle_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) : Submodule.map f (moduleSocle R M) ≤ moduleSocle R N

Every linear map sends the source socle into the target socle.

theorem MagnitudeConjecture.map_moduleSocle_le_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (_hf : Function.Injective ⇑f) : Submodule.map f (moduleSocle R M) ≤ moduleSocle R N

An injective linear map sends the source socle into the target socle.

theorem MagnitudeConjecture.comap_moduleSocle_subtype_eq_moduleSocle {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P : Submodule R M) : Submodule.comap P.subtype (moduleSocle R M) = moduleSocle R ↥P

Pulling the ambient socle back to a submodule gives the intrinsic socle of that submodule.

theorem MagnitudeConjecture.map_moduleSocle_eq_of_linearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Submodule.map (↑e) (moduleSocle R M) = moduleSocle R N

A linear equivalence carries the socle onto the socle.

theorem MagnitudeConjecture.simple_moduleSocle_congr {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) (hM : IsSimpleModule R ↥(moduleSocle R M)) : IsSimpleModule R ↥(moduleSocle R N)

Having simple socle is invariant under a linear equivalence.

theorem MagnitudeConjecture.moduleSocle_prod {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] : moduleSocle R (M × N) = (moduleSocle R M).prod (moduleSocle R N)

The socle of a binary product is the product of the two socles.

theorem MagnitudeConjecture.simpleSubmodule_prod_eq_coordinate {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (hM : IsSimpleModule R M) (hN : IsSimpleModule R N) (hnoniso : ¬Nonempty (M ≃ₗ[R] N)) (P : Submodule R (M × N)) (hP : IsSimpleModule R ↥P) : P = (LinearMap.inl R M N).range ∨ P = (LinearMap.inr R M N).range

A simple submodule of the product of two non-isomorphic simple modules is one of the two coordinate submodules.

def MagnitudeConjecture.submoduleProdLinearEquiv {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] (P : Submodule R M) (Q : Submodule R N) : (↥P × ↥Q) ≃ₗ[R] ↥(P.prod Q)

The product of two submodule types is linearly equivalent to the subtype of their product submodule.

noncomputable def MagnitudeConjecture.moduleSocleProdLinearEquivOfIsCompl {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hPQ : IsCompl P Q) : (↥(moduleSocle R ↥P) × ↥(moduleSocle R ↥Q)) ≃ₗ[R] ↥(moduleSocle R M)

A complementary decomposition restricts to a linear equivalence from the product of the two summand socles onto the ambient socle.

noncomputable def MagnitudeConjecture.quotientModuleSocleProdLinearEquivOfIsCompl {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hPQ : IsCompl P Q) : ((↥P ⧸ moduleSocle R ↥P) × ↥Q ⧸ moduleSocle R ↥Q) ≃ₗ[R] M ⧸ moduleSocle R M

Quotienting a complementary decomposition by the socles of its two summands gives the quotient of the ambient module by its socle.

noncomputable def MagnitudeConjecture.quotientModuleSocleLayerProdLinearEquivOfIsCompl {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hPQ : IsCompl P Q) : (↥(moduleSocle R (↥P ⧸ moduleSocle R ↥P)) × ↥(moduleSocle R (↥Q ⧸ moduleSocle R ↥Q))) ≃ₗ[R] ↥(moduleSocle R (M ⧸ moduleSocle R M))

A complementary decomposition restricts, after quotienting by the first socle layer, to a linear equivalence from the product of the two next socle layers onto the ambient next socle layer.

theorem MagnitudeConjecture.length_quotientModuleSocleLayer_eq_add_of_isCompl {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hPQ : IsCompl P Q) : Module.length R ↥(moduleSocle R (M ⧸ moduleSocle R M)) = Module.length R ↥(moduleSocle R (↥P ⧸ moduleSocle R ↥P)) + Module.length R ↥(moduleSocle R (↥Q ⧸ moduleSocle R ↥Q))

The next socle-layer length is additive across a complementary decomposition.

theorem MagnitudeConjecture.length_moduleSocle_eq_add_of_isCompl {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hPQ : IsCompl P Q) : Module.length R ↥(moduleSocle R M) = Module.length R ↥(moduleSocle R ↥P) + Module.length R ↥(moduleSocle R ↥Q)

Composition length of the socle is additive across a complementary decomposition.

theorem MagnitudeConjecture.exists_simple_submodule_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (P : Submodule R M) (hP : P ≠ ⊥) : ∃ (S : Submodule R M), IsSimpleModule R ↥S ∧ S ≤ P

Every nonzero submodule of an Artinian module contains a simple submodule.

theorem MagnitudeConjecture.inf_moduleSocle_ne_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (P : Submodule R M) (hP : P ≠ ⊥) : P ⊓ moduleSocle R M ≠ ⊥

In an Artinian module the socle meets every nonzero submodule nontrivially.

theorem MagnitudeConjecture.moduleSocle_le_ker_of_not_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] {N : Type v} [AddCommGroup N] [Module R N] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) (f : M →ₗ[R] N) (hf : ¬Function.Injective ⇑f) : moduleSocle R M ≤ f.ker

If an Artinian module has simple socle, every noninjective linear map out of it kills that socle.

theorem MagnitudeConjecture.moduleSocle_ne_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [Nontrivial M] : moduleSocle R M ≠ ⊥

The socle of a nonzero Artinian module is nonzero.

theorem MagnitudeConjecture.moduleSocle_isSimple_of_injective {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] [IsArtinian R M] [Nontrivial M] (f : M →ₗ[R] N) (hf : Function.Injective ⇑f) (hN : IsSimpleModule R ↥(moduleSocle R N)) : IsSimpleModule R ↥(moduleSocle R M)

An injective map from a nonzero Artinian module into a module with simple socle forces the source socle to be simple.

theorem MagnitudeConjecture.moduleSocle_le_jacobson_of_simpleTop_of_not_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hnotSimple : ¬IsSimpleModule R M) : moduleSocle R M ≤ Module.jacobson R M

If a noetherian module has simple top but is not itself simple, its socle lies in its Jacobson radical.

theorem MagnitudeConjecture.IsUniserialModule.moduleSocle_isSimple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [Nontrivial M] (hM : IsUniserialModule R M) : IsSimpleModule R ↥(moduleSocle R M)

A nonzero Artinian uniserial module has simple socle.

theorem MagnitudeConjecture.IsUniserialModule.moduleSocle_eq_of_simple_submodule {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsUniserialModule R M) (P : Submodule R M) (hP : IsSimpleModule R ↥P) : moduleSocle R M = P

In a uniserial module, every specified simple submodule is the socle.

theorem MagnitudeConjecture.IsUniserialModule.eq_of_simple_submodules_le {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {U P Q : Submodule R M} (hU : IsUniserialModule R ↥U) (hP : IsSimpleModule R ↥P) (hQ : IsSimpleModule R ↥Q) (hPU : P ≤ U) (hQU : Q ≤ U) : P = Q

Two simple ambient submodules contained in the same uniserial submodule are equal.

theorem MagnitudeConjecture.IsUniserialModule.of_simpleSocle_of_quotient_moduleSocle {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) (hquot : IsUniserialModule R (M ⧸ moduleSocle R M)) : IsUniserialModule R M

An Artinian module is uniserial when its socle is simple and the quotient by that socle is uniserial. The simple socle is essential, so every nonzero submodule is recovered from its image in the quotient.

theorem MagnitudeConjecture.exists_disjoint_simple_submodule_of_simple_quotient_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (I : Submodule R M) (hI : IsSimpleModule R ↥I) (hquot : IsUniserialModule R (M ⧸ I)) (hnotuni : ¬IsUniserialModule R M) : ∃ (S : Submodule R M), IsSimpleModule R ↥S ∧ S ⊓ I = ⊥

If quotienting by a specified simple submodule makes an Artinian module uniserial, then failure of uniseriality is witnessed by a second simple submodule disjoint from the specified one.

theorem MagnitudeConjecture.uniserial_of_simpleSocle_of_length_eq_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) (hlength : Module.length R M = 2) : IsUniserialModule R M

A length-two module with simple socle is uniserial.

theorem MagnitudeConjecture.length_quotient_moduleSocle_eq_two_of_length_eq_three {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) (hlength : Module.length R M = 3) : Module.length R (M ⧸ moduleSocle R M) = 2

Removing a simple socle from a length-three module leaves a module of length two.

theorem MagnitudeConjecture.length_quotient_eq_three_of_length_eq_four_of_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P : Submodule R M) (hMlength : Module.length R M = 4) (hPsimple : IsSimpleModule R ↥P) : Module.length R (M ⧸ P) = 3

Quotienting a length-four module by a simple submodule leaves length three.

theorem MagnitudeConjecture.moduleSocle_le_ker_of_surjective_of_length_eq_two_to_one {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type v} [AddCommGroup N] [Module R N] [IsArtinian R M] (q : M →ₗ[R] N) (hq : Function.Surjective ⇑q) (hMlength : Module.length R M = 2) (hNlength : Module.length R N = 1) (hsocle : IsSimpleModule R ↥(moduleSocle R M)) : moduleSocle R M ≤ q.ker

A surjection from a length-two module onto a length-one module kills the simple socle of its source.

theorem MagnitudeConjecture.uniserial_of_two_simple_socle_layers_of_length_eq_three {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) (hnext : IsSimpleModule R ↥(moduleSocle R (M ⧸ moduleSocle R M))) (hlength : Module.length R M = 3) : IsUniserialModule R M

A length-three module is uniserial when its socle and the socle of its quotient by the socle are both simple.

theorem MagnitudeConjecture.isIndecomposableModule_of_simpleSocle {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M

An Artinian module with simple socle is indecomposable. This is the simple-socle dual of the existing simple-top criterion.