Quotient branches in the biserial fiber-kernel obstruction

The first Pogorzały--Skowroński obstruction starts with two disjoint simple submodules S,T ⊆ X, forms the branches X/S and X/T, and maps both to a common quotient X/J. This file identifies their first two socle layers and packages the resulting fiber kernel without adding abstract branch data.

theorem MagnitudeConjecture.RightModule.isSimpleModule_map_quotientMk_of_inf_eq_bot {A : Type u} [Ring A] (X : FinitelyGeneratedCategory A) (S T : Submodule Aᵐᵒᵖ ↑X) (hinf : S ⊓ T = ⊥) (hT : IsSimpleModule Aᵐᵒᵖ ↥T) : IsSimpleModule Aᵐᵒᵖ ↥(Submodule.map S.mkQ T)

A simple submodule disjoint from the denominator remains simple in the quotient.

theorem MagnitudeConjecture.RightModule.moduleSocle_quotient_eq_sup_map {A : Type u} [Ring A] (X : FinitelyGeneratedCategory A) (S T : Submodule Aᵐᵒᵖ ↑X) (hinf : S ⊓ T = ⊥) (hT : IsSimpleModule Aᵐᵒᵖ ↥T) (hquot : IsUniserialModule Aᵐᵒᵖ ↑(quotientFGObj X S)) : moduleSocle Aᵐᵒᵖ ↑(quotientFGObj X S) = Submodule.map S.mkQ (S ⊔ T)

In a uniserial quotient X/S, the image of a disjoint simple submodule T is the whole socle.

noncomputable def MagnitudeConjecture.RightModule.quotientBranchSocleLinearEquiv {A : Type u} [Ring A] (X : FinitelyGeneratedCategory A) (S T : Submodule Aᵐᵒᵖ ↑X) (hinf : S ⊓ T = ⊥) (hT : IsSimpleModule Aᵐᵒᵖ ↥T) (hquot : IsUniserialModule Aᵐᵒᵖ ↑(quotientFGObj X S)) : ↥T ≃ₗ[Aᵐᵒᵖ] ↥(moduleSocle Aᵐᵒᵖ ↑(quotientFGObj X S))

The disjoint simple submodule is canonically equivalent to the socle of the corresponding uniserial quotient branch.

def MagnitudeConjecture.RightModule.nestedQuotientBySocleLinearEquiv {A : Type u} [Ring A] (X : FinitelyGeneratedCategory A) (S R : Submodule Aᵐᵒᵖ ↑X) (hSR : S ≤ R) (hsocle : moduleSocle Aᵐᵒᵖ ↑(quotientFGObj X S) = Submodule.map S.mkQ R) : ↑(quotientFGObj (quotientFGObj X S) (moduleSocle Aᵐᵒᵖ ↑(quotientFGObj X S))) ≃ₗ[Aᵐᵒᵖ] ↑(quotientFGObj X R)

Quotienting X/S by the image of a larger layer R is canonically equivalent to X/R.

def MagnitudeConjecture.RightModule.quotientBranchCommonNextSocleFGObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) (R : Submodule Aᵐᵒᵖ ↑X) : FinitelyGeneratedCategory A

The common middle layer of the two quotient branches.

def MagnitudeConjecture.RightModule.quotientBranchNextSocleLinearEquiv {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) (S R : Submodule Aᵐᵒᵖ ↑X) (hSR : S ≤ R) (hsocle : moduleSocle Aᵐᵒᵖ ↑(quotientFGObj X S) = Submodule.map S.mkQ R) : ↥(moduleSocle Aᵐᵒᵖ ↑(quotientFGObj (quotientFGObj X S) (moduleSocle Aᵐᵒᵖ ↑(quotientFGObj X S)))) ≃ₗ[Aᵐᵒᵖ] ↑(quotientBranchCommonNextSocleFGObj X R)

The next socle layer of X/S is canonically the socle of X/R when the first socle of X/S is the image of R.

def MagnitudeConjecture.RightModule.quotientBranchFiberKernelFGObj {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) (S T J : Submodule Aᵐᵒᵖ ↑X) (hSTJ : S ⊔ T ≤ J) : FinitelyGeneratedCategory A

The literal fiber-kernel module on the two quotient branches X/S and X/T over X/J.

def MagnitudeConjecture.RightModule.quotientBranchFiberKernelRadicalPreimage {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (X : FinitelyGeneratedCategory A) (S T J : Submodule Aᵐᵒᵖ ↑X) (hSTJ : S ⊔ T ≤ J) : Submodule Aᵐᵒᵖ ↑(quotientBranchFiberKernelFGObj X S T J hSTJ)

The preimage of the product of the two branch radicals in the literal quotient-branch fiber kernel.