Diagonal cokernels from common radical extensions

Two one-step extensions of the same nonsimple uniserial module give the diagonal cokernel used to exclude a nonsemisimple biserial branch intersection. This file packages its layer identifications and discharges its indecomposability criterion from ambient coordinate thinness.

def MagnitudeConjecture.RightModule.moduleTopQuotientLinearEquiv {A : Type u} [Ring A] (M : FinitelyGeneratedCategory A) (K : Submodule Aᵐᵒᵖ ↑M) (hK : K ≤ Module.jacobson Aᵐᵒᵖ ↑M) : ((↑M ⧸ K) ⧸ Module.jacobson Aᵐᵒᵖ (↑M ⧸ K)) ≃ₗ[Aᵐᵒᵖ] ↑M ⧸ Module.jacobson Aᵐᵒᵖ ↑M

Quotienting below the radical canonically preserves the module top.

noncomputable def MagnitudeConjecture.RightModule.commonRadicalQuotientRadicalLinearEquiv {A : Type u} [Ring A] (E D : FinitelyGeneratedCategory A) (iD : ↑E →ₗ[Aᵐᵒᵖ] ↑D) (hiD : Function.Injective ⇑iD) (hiDrange : iD.range = Module.jacobson Aᵐᵒᵖ ↑D) : have K := Module.jacobson Aᵐᵒᵖ ↑E; have sD := iD ∘ₗ K.subtype; (↑E ⧸ K) ≃ₗ[Aᵐᵒᵖ] ↥(Module.jacobson Aᵐᵒᵖ (↑D ⧸ sD.range))

When E is identified with the radical of D, quotienting D by the image of rad E leaves a radical canonically equivalent to top E.

theorem MagnitudeConjecture.RightModule.moduleTop_nonisomorphic_commonRadicalTop_of_coordinateThin {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type u_1} [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (E C : FinitelyGeneratedCategory A) (iC : ↑E →ₗ[Aᵐᵒᵖ] ↑C) (hiC : Function.Injective ⇑iC) (hiCrange : iC.range = Module.jacobson Aᵐᵒᵖ ↑C) (hCthin : IsCoordinateThin e C) (hEtop : IsSimpleModule Aᵐᵒᵖ (↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)) : ¬Nonempty ((↑C ⧸ Module.jacobson Aᵐᵒᵖ ↑C) ≃ₗ[Aᵐᵒᵖ] ↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)

If E is the radical of a coordinate-thin module C, the top of C cannot be isomorphic to the top of E.

theorem MagnitudeConjecture.RightModule.crossSubmoduleToQuotient_ker {A : Type u} [Ring A] (L : FinitelyGeneratedCategory A) (C D : Submodule Aᵐᵒᵖ ↑L) : (C.mkQ ∘ₗ D.subtype).ker = Submodule.comap D.subtype C

The kernel of the canonical map from D to L/C is the intrinsic pullback to D of the ambient intersection with C.

theorem MagnitudeConjecture.RightModule.moduleTops_nonisomorphic_of_coordinateThin_of_crossKernel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type u_1} [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (L : FinitelyGeneratedCategory A) (hL : IsCoordinateThin e L) (C D : Submodule Aᵐᵒᵖ ↑L) (hCtop : IsSimpleModule Aᵐᵒᵖ (↑(submoduleFGObj L C) ⧸ Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L C))) (hker : (C.mkQ ∘ₗ D.subtype).ker = Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L D)) : ¬Nonempty ((↑(submoduleFGObj L C) ⧸ Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L C)) ≃ₗ[Aᵐᵒᵖ] ↑(submoduleFGObj L D) ⧸ Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L D))

The simple tops of two submodules of a coordinate-thin ambient module cannot coincide when the second branch maps into the quotient by the first with precisely its radical as kernel.

theorem MagnitudeConjecture.RightModule.isIndecomposableModule_diagonalCommonRadicalCokernel {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (E C D : FinitelyGeneratedCategory A) (iC : ↑E →ₗ[Aᵐᵒᵖ] ↑C) (iD : ↑E →ₗ[Aᵐᵒᵖ] ↑D) (hiC : Function.Injective ⇑iC) (hiD : Function.Injective ⇑iD) (hiCrange : iC.range = Module.jacobson Aᵐᵒᵖ ↑C) (hiDrange : iD.range = Module.jacobson Aᵐᵒᵖ ↑D) (hEtop : IsSimpleModule Aᵐᵒᵖ (↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)) (hCtop : IsSimpleModule Aᵐᵒᵖ (↑C ⧸ Module.jacobson Aᵐᵒᵖ ↑C)) (hDtop : IsSimpleModule Aᵐᵒᵖ (↑D ⧸ Module.jacobson Aᵐᵒᵖ ↑D)) (hCtopDtop : ¬Nonempty ((↑C ⧸ Module.jacobson Aᵐᵒᵖ ↑C) ≃ₗ[Aᵐᵒᵖ] ↑D ⧸ Module.jacobson Aᵐᵒᵖ ↑D)) (hCtopEtop : ¬Nonempty ((↑C ⧸ Module.jacobson Aᵐᵒᵖ ↑C) ≃ₗ[Aᵐᵒᵖ] ↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)) (hDtopEtop : ¬Nonempty ((↑D ⧸ Module.jacobson Aᵐᵒᵖ ↑D) ≃ₗ[Aᵐᵒᵖ] ↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)) [Nontrivial ↥(Module.jacobson Aᵐᵒᵖ ↑E)] : let K := Module.jacobson Aᵐᵒᵖ ↑E; have sC := iC ∘ₗ K.subtype; have sD := iD ∘ₗ K.subtype; have h := sC.prod sD; QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(cokernelFGObj (submoduleFGObj E K) (prodFGObj C D) h)

Two local modules with a common radical yield an indecomposable diagonal cokernel after gluing the radical of that common radical.

theorem MagnitudeConjecture.RightModule.isIndecomposableModule_diagonalCommonRadicalCokernel_of_coordinateThin {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type u_1} [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (E C D : FinitelyGeneratedCategory A) (iC : ↑E →ₗ[Aᵐᵒᵖ] ↑C) (iD : ↑E →ₗ[Aᵐᵒᵖ] ↑D) (hiC : Function.Injective ⇑iC) (hiD : Function.Injective ⇑iD) (hiCrange : iC.range = Module.jacobson Aᵐᵒᵖ ↑C) (hiDrange : iD.range = Module.jacobson Aᵐᵒᵖ ↑D) (hCthin : IsCoordinateThin e C) (hDthin : IsCoordinateThin e D) (hEtop : IsSimpleModule Aᵐᵒᵖ (↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)) (hCtop : IsSimpleModule Aᵐᵒᵖ (↑C ⧸ Module.jacobson Aᵐᵒᵖ ↑C)) (hDtop : IsSimpleModule Aᵐᵒᵖ (↑D ⧸ Module.jacobson Aᵐᵒᵖ ↑D)) (hCtopDtop : ¬Nonempty ((↑C ⧸ Module.jacobson Aᵐᵒᵖ ↑C) ≃ₗ[Aᵐᵒᵖ] ↑D ⧸ Module.jacobson Aᵐᵒᵖ ↑D)) [Nontrivial ↥(Module.jacobson Aᵐᵒᵖ ↑E)] : let K := Module.jacobson Aᵐᵒᵖ ↑E; have sC := iC ∘ₗ K.subtype; have sD := iD ∘ₗ K.subtype; have h := sC.prod sD; QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(cokernelFGObj (submoduleFGObj E K) (prodFGObj C D) h)

For coordinate-thin common-radical extensions, separation of the two outer tops is the only nonisomorphism hypothesis needed by the diagonal cokernel criterion.

theorem MagnitudeConjecture.RightModule.isIndecomposableModule_diagonalCommonRadicalCokernel_of_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {ι : Type u_1} [Fintype ι] (e : ι → A) (hall : CompleteOrthogonalIdempotents e) (L : FinitelyGeneratedCategory A) (hL : IsCoordinateThin e L) (C D : Submodule Aᵐᵒᵖ ↑L) (E : FinitelyGeneratedCategory A) (iC : ↑E →ₗ[Aᵐᵒᵖ] ↑(submoduleFGObj L C)) (iD : ↑E →ₗ[Aᵐᵒᵖ] ↑(submoduleFGObj L D)) (hiC : Function.Injective ⇑iC) (hiD : Function.Injective ⇑iD) (hiCrange : iC.range = Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L C)) (hiDrange : iD.range = Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L D)) (hcrossKer : (C.mkQ ∘ₗ D.subtype).ker = Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L D)) (hEtop : IsSimpleModule Aᵐᵒᵖ (↑E ⧸ Module.jacobson Aᵐᵒᵖ ↑E)) (hCtop : IsSimpleModule Aᵐᵒᵖ (↑(submoduleFGObj L C) ⧸ Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L C))) (hDtop : IsSimpleModule Aᵐᵒᵖ (↑(submoduleFGObj L D) ⧸ Module.jacobson Aᵐᵒᵖ ↑(submoduleFGObj L D))) [Nontrivial ↥(Module.jacobson Aᵐᵒᵖ ↑E)] : let K := Module.jacobson Aᵐᵒᵖ ↑E; have sC := iC ∘ₗ K.subtype; have sD := iD ∘ₗ K.subtype; have h := sC.prod sD; QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(cokernelFGObj (submoduleFGObj E K) (prodFGObj (submoduleFGObj L C) (submoduleFGObj L D)) h)

Ambient coordinate thinness discharges every separation hypothesis for two submodules whose common-radical structure is compatible with the cross projection to L/C.