The radical-square-zero obstruction in the biserial induction

A local coordinate-thin module cannot have three independent simple summands in its square-zero radical. From such summands one forms two quotient branches with two-simple radicals, glues their common simple summand diagonally, and obtains the highest-root D₄ module: its top occurs twice, but the cross-map criterion makes it indecomposable.

theorem MagnitudeConjecture.RightModule.submoduleToQuotientLinearMap_range {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) (P K : Submodule Aᵐᵒᵖ ↑L) : (IsBiserialModule.submoduleToQuotientLinearMap P K).range = Submodule.map K.mkQ P

The range of the canonical map from a submodule to an ambient quotient is its ordinary mapped submodule.

theorem MagnitudeConjecture.RightModule.map_quotientMk_eq_bot_of_le {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) (P K : Submodule Aᵐᵒᵖ ↑L) (hPK : P ≤ K) : Submodule.map K.mkQ P = ⊥

Every submodule of a quotient denominator maps to zero.

def MagnitudeConjecture.RightModule.quotientByMappedSubmoduleLinearEquiv {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) (P K : Submodule Aᵐᵒᵖ ↑L) : ((↑L ⧸ K) ⧸ Submodule.map K.mkQ P) ≃ₗ[Aᵐᵒᵖ] ↑L ⧸ K ⊔ P

A nested quotient by the image of a disjoint submodule is the quotient by the sum of the two ambient denominators.

theorem MagnitudeConjecture.RightModule.false_of_three_simple_squareZero_radical_summands {k A : Type u} {ι : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (Hthin : AllIndecomposablesCoordinateThin e) (L : FinitelyGeneratedCategory A) (hLtop : IsSimpleModule Aᵐᵒᵖ (↑L ⧸ Module.jacobson Aᵐᵒᵖ ↑L)) (S C T D U V : Submodule Aᵐᵒᵖ ↑L) (hSsimple : IsSimpleModule Aᵐᵒᵖ ↥S) (hTsimple : IsSimpleModule Aᵐᵒᵖ ↥T) (hUsimple : IsSimpleModule Aᵐᵒᵖ ↥U) (hSCsup : S ⊔ C = Module.jacobson Aᵐᵒᵖ ↑L) (hSCinf : S ⊓ C = ⊥) (hTDsup : T ⊔ D = C) (hTDinf : T ⊓ D = ⊥) (hUVsup : U ⊔ V = D) (hUVinf : U ⊓ V = ⊥) : False

A four-summand radical configuration gives the forbidden D₄ diagonal cokernel. The hypotheses are an ordered direct decomposition rad L = S ⊕ (T ⊕ (U ⊕ V)); only S, T, and U are required to be simple.

theorem MagnitudeConjecture.RightModule.jacobson_length_le_two_of_semisimple_of_all_coordinateThin {k A : Type u} {ι : Type w} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (Hthin : AllIndecomposablesCoordinateThin e) (L : FinitelyGeneratedCategory A) (hLtop : IsSimpleModule Aᵐᵒᵖ (↑L ⧸ Module.jacobson Aᵐᵒᵖ ↑L)) [IsArtinian Aᵐᵒᵖ ↑L] [IsSemisimpleModule Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑L)] : Module.length Aᵐᵒᵖ ↥(Module.jacobson Aᵐᵒᵖ ↑L) ≤ 2

A semisimple radical of a coordinate-thin local module has composition length at most two. If its length were larger, three successive simple summands and their residual complement would instantiate the preceding D₄ obstruction.