Common-radical extensions from uniserial branch successors

A maximal nonsimple indecomposable submodule of a branch intersection has exactly the expected intersection in any two immediate uniserial successors. This supplies the cross-kernel equality needed by the common-radical diagonal-cokernel obstruction.

theorem MagnitudeConjecture.crossKernel_eq_jacobson_of_inf_eq {R : Type u} [Ring R] {M : Type v} [AddCommGroup M] [Module R M] (E C D : Submodule R M) (hinf : C ⊓ D = E) (hDrad : Submodule.comap D.subtype E = Module.jacobson R ↥D) : (C.mkQ ∘ₗ D.subtype).ker = Module.jacobson R ↥D

If two ambient submodules meet in E and E is the intrinsic radical of the second, then projection of the second to the quotient by the first has precisely that radical as kernel.

theorem MagnitudeConjecture.RightModule.false_of_nonsimple_indecomposable_intersection_eq_both_jacobson {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) (hL : IsCoordinateThin e L) (P Q : Submodule Aᵐᵒᵖ ↑L) (hPtop : IsSimpleModule Aᵐᵒᵖ (↥P ⧸ Module.jacobson Aᵐᵒᵖ ↥P)) (hQtop : IsSimpleModule Aᵐᵒᵖ (↥Q ⧸ Module.jacobson Aᵐᵒᵖ ↥Q)) (hPjac : (infToLeftLinearMap P Q).range = Module.jacobson Aᵐᵒᵖ ↥P) (hQjac : (infToRightLinearMap P Q).range = Module.jacobson Aᵐᵒᵖ ↥Q) (hIind : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↥(P ⊓ Q)) (hInonsimple : ¬IsSimpleModule Aᵐᵒᵖ ↥(P ⊓ Q)) : False

If a nonsimple indecomposable intersection is the full Jacobson radical of both local branches, gluing the branches along the radical of their intersection gives the forbidden diagonal cokernel. No uniseriality of the intersection is needed in this terminal case.