Diagonal cokernels from biserial branch intersections

A coordinate-thin ambient module has no nonzero map from a simple-top submodule to its complementary ambient quotient. Applied to two branches with a semisimple length-two intersection, this forces the cross-Hom vanishing needed to prove the diagonal-summand cokernel indecomposable.

theorem MagnitudeConjecture.RightModule.linearMap_submodule_to_quotient_eq_zero_of_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) (L : FinitelyGeneratedCategory A) (hL : IsCoordinateThin e L) (P : Submodule Aᵐᵒᵖ ↑L) (hPtop : IsSimpleModule Aᵐᵒᵖ (↥P ⧸ Module.jacobson Aᵐᵒᵖ ↥P)) (f : ↑(submoduleFGObj L P) →ₗ[Aᵐᵒᵖ] ↑(quotientFGObj L P)) : f = 0

In a coordinate-thin module, every map from a simple-top submodule to the quotient by that same submodule is zero.

theorem MagnitudeConjecture.RightModule.linearMap_to_crossBranch_eq_zero_of_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) (L : FinitelyGeneratedCategory A) (hL : IsCoordinateThin e L) (P : Submodule Aᵐᵒᵖ ↑L) (hPtop : IsSimpleModule Aᵐᵒᵖ (↥P ⧸ Module.jacobson Aᵐᵒᵖ ↥P)) (N : FinitelyGeneratedCategory A) (g : ↑N →ₗ[Aᵐᵒᵖ] ↑(quotientFGObj L P)) (hkerSimple : IsSimpleModule Aᵐᵒᵖ ↥g.ker) (hnoniso : ¬Nonempty ((↥P ⧸ Module.jacobson Aᵐᵒᵖ ↥P) ≃ₗ[Aᵐᵒᵖ] ↥g.ker)) (f : ↑(submoduleFGObj L P) →ₗ[Aᵐᵒᵖ] ↑N) : f = 0

A cross map out of a simple-top branch vanishes when projection to the ambient branch quotient has a simple kernel different from the source top.

def MagnitudeConjecture.RightModule.infToLeftLinearMap {A : Type u} [Ring A] {L : FinitelyGeneratedCategory A} (P Q : Submodule Aᵐᵒᵖ ↑L) : ↥(P ⊓ Q) →ₗ[Aᵐᵒᵖ] ↥P

The intersection of two submodules maps canonically to the left one.

def MagnitudeConjecture.RightModule.infToRightLinearMap {A : Type u} [Ring A] {L : FinitelyGeneratedCategory A} (P Q : Submodule Aᵐᵒᵖ ↑L) : ↥(P ⊓ Q) →ₗ[Aᵐᵒᵖ] ↥Q

The intersection of two submodules maps canonically to the right one.

theorem MagnitudeConjecture.RightModule.infToLeftLinearMap_injective {A : Type u} [Ring A] {L : FinitelyGeneratedCategory A} (P Q : Submodule Aᵐᵒᵖ ↑L) : Function.Injective ⇑(infToLeftLinearMap P Q)

theorem MagnitudeConjecture.RightModule.infToRightLinearMap_injective {A : Type u} [Ring A] {L : FinitelyGeneratedCategory A} (P Q : Submodule Aᵐᵒᵖ ↑L) : Function.Injective ⇑(infToRightLinearMap P Q)

def MagnitudeConjecture.RightModule.infSubmoduleToRightLinearMap {A : Type u} [Ring A] {L : FinitelyGeneratedCategory A} (P Q : Submodule Aᵐᵒᵖ ↑L) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) : ↥K →ₗ[Aᵐᵒᵖ] ↥Q

A chosen submodule of an intersection maps into the right branch.

def MagnitudeConjecture.RightModule.infSubmoduleToLeftLinearMap {A : Type u} [Ring A] {L : FinitelyGeneratedCategory A} (P Q : Submodule Aᵐᵒᵖ ↑L) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) : ↥K →ₗ[Aᵐᵒᵖ] ↥P

A chosen submodule of an intersection maps into the left branch.

def MagnitudeConjecture.RightModule.crossBranchQuotientProjection {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (L : FinitelyGeneratedCategory A) (P Q : Submodule Aᵐᵒᵖ ↑L) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) : ↑(quotientFGObj (submoduleFGObj L Q) (infSubmoduleToRightLinearMap P Q K).range) →ₗ[Aᵐᵒᵖ] ↑(quotientFGObj L P)

The right branch modulo a chosen intersection submodule projects to the ambient quotient by the left branch.

def MagnitudeConjecture.RightModule.crossBranchLeftQuotientProjection {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (L : FinitelyGeneratedCategory A) (P Q : Submodule Aᵐᵒᵖ ↑L) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) : ↑(quotientFGObj (submoduleFGObj L P) (infSubmoduleToLeftLinearMap P Q K).range) →ₗ[Aᵐᵒᵖ] ↑(quotientFGObj L Q)

The left branch modulo a chosen intersection submodule projects to the ambient quotient by the right branch.

noncomputable def MagnitudeConjecture.RightModule.crossBranchQuotientProjectionKernelLinearEquiv {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (L : FinitelyGeneratedCategory A) (P Q : Submodule Aᵐᵒᵖ ↑L) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) : (↥(P ⊓ Q) ⧸ K) ≃ₗ[Aᵐᵒᵖ] ↥(crossBranchQuotientProjection L P Q K).ker

The kernel of the projection from the right branch modulo a chosen intersection submodule is the corresponding quotient of the whole intersection.

noncomputable def MagnitudeConjecture.RightModule.crossBranchLeftQuotientProjectionKernelLinearEquiv {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (L : FinitelyGeneratedCategory A) (P Q : Submodule Aᵐᵒᵖ ↑L) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) : (↥(P ⊓ Q) ⧸ K) ≃ₗ[Aᵐᵒᵖ] ↥(crossBranchLeftQuotientProjection L P Q K).ker

Left-hand version of crossBranchQuotientProjectionKernelLinearEquiv.

theorem MagnitudeConjecture.RightModule.linearMap_to_crossBranchQuotient_eq_zero_of_coordinateThin_of_inf_left_le_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) (L : FinitelyGeneratedCategory A) (hL : IsCoordinateThin e L) (P Q : Submodule Aᵐᵒᵖ ↑L) (hPtop : IsSimpleModule Aᵐᵒᵖ (↥P ⧸ Module.jacobson Aᵐᵒᵖ ↥P)) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) (hInfJ : (infToLeftLinearMap P Q).range ≤ Module.jacobson Aᵐᵒᵖ ↥P) (f : ↑(submoduleFGObj L P) →ₗ[Aᵐᵒᵖ] ↑(quotientFGObj (submoduleFGObj L Q) (infSubmoduleToRightLinearMap P Q K).range)) : f = 0

If the whole branch intersection maps into the left branch radical, every map from the left branch to the right branch modulo an intersection submodule is zero. Projection to the ambient quotient kills the map first; its remaining image is a subquotient of the source radical, which coordinate thinness also kills.

theorem MagnitudeConjecture.RightModule.linearMap_to_crossBranchLeftQuotient_eq_zero_of_coordinateThin_of_inf_right_le_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) (L : FinitelyGeneratedCategory A) (hL : IsCoordinateThin e L) (P Q : Submodule Aᵐᵒᵖ ↑L) (hQtop : IsSimpleModule Aᵐᵒᵖ (↥Q ⧸ Module.jacobson Aᵐᵒᵖ ↥Q)) (K : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) (hInfJ : (infToRightLinearMap P Q).range ≤ Module.jacobson Aᵐᵒᵖ ↥Q) (f : ↑(submoduleFGObj L Q) →ₗ[Aᵐᵒᵖ] ↑(quotientFGObj (submoduleFGObj L P) (infSubmoduleToLeftLinearMap P Q K).range)) : f = 0

Right-hand version of linearMap_to_crossBranchQuotient_eq_zero_of_coordinateThin_of_inf_left_le_jacobson.

theorem MagnitudeConjecture.RightModule.crossBranchQuotientProjection_simple_kernel {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (L : FinitelyGeneratedCategory A) (P Q : Submodule Aᵐᵒᵖ ↑L) (K T : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) (hTsimple : IsSimpleModule Aᵐᵒᵖ ↥T) (hcompl : IsCompl K T) : IsSimpleModule Aᵐᵒᵖ ↥(crossBranchQuotientProjection L P Q K).ker ∧ Nonempty (↥(crossBranchQuotientProjection L P Q K).ker ≃ₗ[Aᵐᵒᵖ] ↥T)

Projection from the right branch modulo a chosen intersection summand to the ambient quotient by the left branch has kernel the complementary intersection summand.

theorem MagnitudeConjecture.RightModule.crossBranchLeftQuotientProjection_simple_kernel {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (L : FinitelyGeneratedCategory A) (P Q : Submodule Aᵐᵒᵖ ↑L) (K T : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) (hTsimple : IsSimpleModule Aᵐᵒᵖ ↥T) (hcompl : IsCompl K T) : IsSimpleModule Aᵐᵒᵖ ↥(crossBranchLeftQuotientProjection L P Q K).ker ∧ Nonempty (↥(crossBranchLeftQuotientProjection L P Q K).ker ≃ₗ[Aᵐᵒᵖ] ↥T)

The left-hand version of crossBranchQuotientProjection_simple_kernel.

theorem MagnitudeConjecture.RightModule.isIndecomposableModule_diagonalInfSummandCokernel_of_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) (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)) (K T : Submodule Aᵐᵒᵖ ↥(P ⊓ Q)) (hKsimple : IsSimpleModule Aᵐᵒᵖ ↥K) (hTsimple : IsSimpleModule Aᵐᵒᵖ ↥T) (hcompl : IsCompl K T) (hTopPTP : ¬Nonempty ((↥P ⧸ Module.jacobson Aᵐᵒᵖ ↥P) ≃ₗ[Aᵐᵒᵖ] ↥(Submodule.map (infToLeftLinearMap P Q) T))) (hTopQTQ : ¬Nonempty ((↥Q ⧸ Module.jacobson Aᵐᵒᵖ ↥Q) ≃ₗ[Aᵐᵒᵖ] ↥(Submodule.map (infToRightLinearMap P Q) T))) : let I := submoduleFGObj L (P ⊓ Q); let S := submoduleFGObj I K; let C := submoduleFGObj L P; let D := submoduleFGObj L Q; have sC := infToLeftLinearMap P Q ∘ₗ K.subtype; have sD := infToRightLinearMap P Q ∘ₗ K.subtype; have h := sC.prod sD; QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule Aᵐᵒᵖ ↑(cokernelFGObj S (prodFGObj C D) h)

Gluing one simple summand of a length-two branch intersection gives an indecomposable cokernel. Coordinate thinness of the ambient local module replaces the source's unnecessary branch-length-three reduction.