Biserial modules

The radical of a biserial module is the sum of at most two uniserial submodules whose intersection is simple or zero. Zero summands are allowed, so the definition also covers uniserial and semisimple local modules without separate edge cases.

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

A module is simple or zero. The Subsingleton branch is the literal zero-module alternative and does not require a chosen zero object.

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

theorem MagnitudeConjecture.IsSimpleOrZeroModule.of_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsSimpleModule R M) : IsSimpleOrZeroModule R M

theorem MagnitudeConjecture.IsSimpleOrZeroModule.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 : IsSimpleOrZeroModule R M) : IsSimpleOrZeroModule R N

Simplicity-or-zero is invariant under a linear equivalence.

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

The radical of M is a sum of at most two uniserial submodules with simple or zero intersection.

theorem MagnitudeConjecture.IsBiserialModule.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 : IsBiserialModule R M) : IsBiserialModule R N

Biseriality is invariant under a linear equivalence.

theorem MagnitudeConjecture.IsBiserialModule.of_uniserial_jacobson {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hJ : IsUniserialModule R ↥(Module.jacobson R M)) : IsBiserialModule R M

A module with uniserial radical is biserial, using the zero module as the second branch.

theorem MagnitudeConjecture.IsBiserialModule.of_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsUniserialModule R M) : IsBiserialModule R M

Every uniserial module is biserial.

theorem MagnitudeConjecture.IsBiserialModule.of_jacobson_eq_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hJ : Module.jacobson R M = ⊥) : IsBiserialModule R M

A module with zero radical is biserial.

def MagnitudeConjecture.IsBiserialModule.submoduleToQuotientLinearMap {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) : ↥P →ₗ[R] M ⧸ Q

The canonical map from a submodule P to the quotient by another submodule Q.

theorem MagnitudeConjecture.IsBiserialModule.submoduleToQuotientLinearMap_injective_of_inf_eq_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hinf : P ⊓ Q = ⊥) : Function.Injective ⇑(submoduleToQuotientLinearMap P Q)

If two submodules meet trivially, the canonical map from either one to the quotient by the other is injective.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_submodule_of_uniserial_quotient_of_inf_eq_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hinf : P ⊓ Q = ⊥) (hquot : IsUniserialModule R (M ⧸ Q)) : IsUniserialModule R ↥P

A branch disjoint from Q is uniserial whenever the ambient quotient by Q is uniserial.

theorem MagnitudeConjecture.IsBiserialModule.of_jacobson_eq_sup_of_inf_eq_bot_of_quotients_uniserial {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (P Q : Submodule R M) (hsup : P ⊔ Q = Module.jacobson R M) (hinf : P ⊓ Q = ⊥) (hquotQ : IsUniserialModule R (M ⧸ Q)) (hquotP : IsUniserialModule R (M ⧸ P)) : IsBiserialModule R M

Zero-intersection branch of the local biserial induction. If the radical is the sum of two disjoint branches and both cross-quotients are uniserial, then the module is biserial.

theorem MagnitudeConjecture.IsBiserialModule.jacobson_quotient_eq_map_of_jacobson_eq_sup {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (P Q : Submodule R M) (hsup : P ⊔ Q = Module.jacobson R M) : Module.jacobson R (M ⧸ Q) = Submodule.map Q.mkQ P

If the radical is P + Q, quotienting by Q leaves precisely the image of P as the radical.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_quotient_of_jacobson_eq_sup_of_inf_eq_bot {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (P Q : Submodule R M) (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hsup : P ⊔ Q = Module.jacobson R M) (hinf : P ⊓ Q = ⊥) (hP : IsUniserialModule R ↥P) : IsUniserialModule R (M ⧸ Q)

A simple-top module whose radical is P + Q has a uniserial quotient by Q when P is uniserial and the two branches are disjoint. The image of P is then the full radical of the quotient.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_of_biserial_of_simple_top_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)) (hbis : IsBiserialModule R M) (hJacTop : IsSimpleModule R (↥(Module.jacobson R M) ⧸ Module.jacobson R ↥(Module.jacobson R M))) : IsUniserialModule R M

If a simple-top module is biserial and its radical again has simple top, then it is uniserial. Indeed, the two biserial branches cannot both be proper in the radical, since every proper submodule of a simple-top module lies in its Jacobson radical.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_of_simple {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : IsSimpleModule R M) : IsUniserialModule R M

A simple module is uniserial.

theorem MagnitudeConjecture.IsBiserialModule.simple_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) (P : Submodule R M) (hP : IsSimpleModule R ↥P) : IsSimpleModule R ↥(Submodule.map f P)

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

theorem MagnitudeConjecture.IsBiserialModule.uniserial_of_length_eq_one {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : Module.length R M = 1) : IsUniserialModule R M

A finite-length module of composition length one is uniserial.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_of_simple_top_of_length_eq_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hlength : Module.length R M = 2) : IsUniserialModule R M

A finite-length module with simple top and composition length two is uniserial.

theorem MagnitudeConjecture.IsBiserialModule.simple_isCompl_of_length_eq_two_of_incomparable {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (hlength : Module.length R M = 2) {P Q : Submodule R M} (hPQ : ¬P ≤ Q) (hQP : ¬Q ≤ P) : IsSimpleModule R ↥P ∧ IsSimpleModule R ↥Q ∧ IsCompl P Q

Two incomparable submodules of a finite-length module of composition length two are complementary simple submodules.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_of_indec_of_length_eq_two {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (hindec : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R M) (hlength : Module.length R M = 2) : IsUniserialModule R M

An indecomposable finite-length module of composition length two is uniserial.

theorem MagnitudeConjecture.IsBiserialModule.jacobson_length_eq_two_of_simple_top_of_length_eq_three {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hlength : Module.length R M = 3) : Module.length R ↥(Module.jacobson R M) = 2

A composition-length-three module with simple top has radical of composition length two.

theorem MagnitudeConjecture.IsBiserialModule.uniserial_of_simple_top_of_length_eq_three_of_jacobson_indec {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hlength : Module.length R M = 3) (hradIndec : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↥(Module.jacobson R M)) : IsUniserialModule R M

A composition-length-three module with simple top and indecomposable radical is uniserial.

theorem MagnitudeConjecture.IsBiserialModule.of_simple_top_of_length_eq_three {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherian R M] [IsArtinian R M] (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) (hlength : Module.length R M = 3) : IsBiserialModule R M

A finite-length module of composition length three with simple top is biserial. If its radical is not already uniserial, its two incomparable submodules are complementary simples.