Biserial modules from a two-summand radical decomposition

An explicit decomposition of the Jacobson radical into two uniserial modules gives the two branches in the definition of a biserial module. This file records the elementary linear-algebra assembly separately from the Auslander--Reiten argument which produces those branches.

def MagnitudeConjecture.HasSeparatedUniserialRadicalObject {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : C) : Prop

Intrinsic form of a radical decomposition into two uniserial branches whose intersection is zero.

theorem MagnitudeConjecture.HasSeparatedUniserialRadicalObject.congrOrderIso {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian D] {X : C} {Y : D} (hX : HasSeparatedUniserialRadicalObject X) (e : CategoryTheory.Subobject X ≃o CategoryTheory.Subobject Y) : HasSeparatedUniserialRadicalObject Y

Separated radical branches are invariant under an order isomorphism of subobject lattices.

theorem MagnitudeConjecture.HasSeparatedUniserialRadicalObject.map_equivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian D] {X : C} (hX : HasSeparatedUniserialRadicalObject X) (E : C ≌ D) : HasSeparatedUniserialRadicalObject (E.functor.obj X)

An equivalence sends separated radical branches to separated radical branches.

theorem MagnitudeConjecture.HasSeparatedUniserialRadicalObject.of_map_equivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Abelian C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Abelian D] {X : C} (E : C ≌ D) (hEX : HasSeparatedUniserialRadicalObject (E.functor.obj X)) : HasSeparatedUniserialRadicalObject X

Separated radical branches of an equivalence image reflect to the source.

theorem MagnitudeConjecture.IsBiserialModule.IsUniserialModule.comap_of_simple_essential_kernel {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) (hker : IsSimpleModule R ↥f.ker) (hessential : ∀ (P : Submodule R M), P ≠ ⊥ → P ⊓ f.ker ≠ ⊥) (U : Submodule R N) (hU : IsUniserialModule R ↥U) : IsUniserialModule R ↥(Submodule.comap f U)

The preimage of a uniserial submodule along a surjection is uniserial when the kernel is simple and essential in the source.

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

The Jacobson radical is the internal direct sum of two uniserial submodules. Zero branches are allowed.

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

Separated uniserial radical branches are invariant under linear equivalence.

theorem MagnitudeConjecture.IsBiserialModule.HasSeparatedUniserialJacobsonBranches.toModuleCatObject {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : HasSeparatedUniserialJacobsonBranches R M) (htop : IsSimpleModule R (M ⧸ Module.jacobson R M)) : HasSeparatedUniserialRadicalObject (ModuleCat.of R M)

Separated module-theoretic branches with simple top give the intrinsic subobject-lattice form.

theorem MagnitudeConjecture.IsBiserialModule.hasSeparatedUniserialJacobsonBranches_of_moduleCatObject {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (hM : HasSeparatedUniserialRadicalObject (ModuleCat.of R M)) : HasSeparatedUniserialJacobsonBranches R M

The intrinsic separated-branch condition on a module object recovers separated module-theoretic Jacobson branches.

theorem MagnitudeConjecture.IsBiserialModule.HasSeparatedUniserialJacobsonBranches.toFGModuleCatObject {R : Type u} [Ring R] [IsNoetherianRing R] (N : FGModuleCat R) (hN : HasSeparatedUniserialJacobsonBranches R ↑N) (htop : IsSimpleModule R (↑N ⧸ Module.jacobson R ↑N)) : HasSeparatedUniserialRadicalObject N

The separated module condition with simple top gives the intrinsic condition in the finitely generated module category.

theorem MagnitudeConjecture.IsBiserialModule.hasSeparatedUniserialJacobsonBranches_of_fgModuleCatObject {R : Type u} [Ring R] [IsNoetherianRing R] (N : FGModuleCat R) (hN : HasSeparatedUniserialRadicalObject N) : HasSeparatedUniserialJacobsonBranches R ↑N

The intrinsic separated condition in the finitely generated module category recovers separated module-theoretic branches.

theorem MagnitudeConjecture.IsBiserialModule.hasSeparatedUniserialJacobsonBranches_of_linearEquiv_prod {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {U : Type w₁} [AddCommGroup U] [Module R U] {V : Type w₂} [AddCommGroup V] [Module R V] (e : ↥(Module.jacobson R M) ≃ₗ[R] U × V) (hU : IsUniserialModule R U) (hV : IsUniserialModule R V) : HasSeparatedUniserialJacobsonBranches R M

A linear equivalence from the Jacobson radical to a product of two uniserial modules supplies separated internal branches.

theorem MagnitudeConjecture.IsBiserialModule.of_jacobson_linearEquiv_prod {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] {U : Type w₁} [AddCommGroup U] [Module R U] {V : Type w₂} [AddCommGroup V] [Module R V] (e : ↥(Module.jacobson R M) ≃ₗ[R] U × V) (hU : IsUniserialModule R U) (hV : IsUniserialModule R V) : IsBiserialModule R M

If the Jacobson radical is linearly equivalent to a product of two uniserial modules, then the ambient module is biserial.

theorem MagnitudeConjecture.IsBiserialModule.of_quotient_moduleSocle_hasSeparatedUniserialJacobsonBranches {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] [IsArtinian R M] (hsocle : IsSimpleModule R ↥(moduleSocle R M)) (hsocleRadical : moduleSocle R M ≤ Module.jacobson R M) (hquot : HasSeparatedUniserialJacobsonBranches R (M ⧸ moduleSocle R M)) : IsBiserialModule R M

If the socle is simple and lies in the radical, separated uniserial branches in the quotient by the socle lift to two uniserial branches whose intersection is precisely that socle.